case intro.intro.intro
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
⊢ ∃ t', t' ≤ t ∧ Continuous f ∧ PolishSpace α
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
⊢ ∃ t', t' ≤ t ∧ Continuous f ∧ PolishSpace α
obtain ⟨b, b_count, -, hb⟩ : ∃ b : Set (Set β), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b :=
  exists_countable_basis β
case intro.intro.intro
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
⊢ ∃ t', t' ≤ t ∧ Continuous f ∧ PolishSpace α
case intro.intro.intro
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
⊢ ∃ t', t' ≤ t ∧ Continuous f ∧ PolishSpace α
haveI : Encodable b := b_count.toEncodable
case intro.intro.intro
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this✝ : Encodable ↑b
this : ∀ (s : ↑b), IsClopenable (f ⁻¹' ↑s)
⊢ ∃ t', t' ≤ t ∧ Continuous f ∧ PolishSpace α
case intro.intro.intro
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
⊢ ∃ t', t' ≤ t ∧ Continuous f ∧ PolishSpace α
have : ∀ s : b, IsClopenable (f ⁻¹' s) := by
  intro s
  apply MeasurableSet.isClopenable
  exact hf (hb.isOpen s.2).measurableSet
case intro.intro.intro
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
T : ↑b → TopologicalSpace α
Tt : ∀ (s : ↑b), T s ≤ t
Tpolish : ∀ (s : ↑b), PolishSpace α
h✝ : ∀ (s : ↑b), IsClosed (f ⁻¹' ↑s)
Topen : ∀ (s : ↑b), IsOpen (f ⁻¹' ↑s)
⊢ ∃ t', t' ≤ t ∧ Continuous f ∧ PolishSpace α
case intro.intro.intro
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this✝ : Encodable ↑b
this : ∀ (s : ↑b), IsClopenable (f ⁻¹' ↑s)
⊢ ∃ t', t' ≤ t ∧ Continuous f ∧ PolishSpace α
choose T Tt Tpolish _ Topen using this
case intro.intro.intro.intro.intro.intro
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
T : ↑b → TopologicalSpace α
Tt : ∀ (s : ↑b), T s ≤ t
Tpolish : ∀ (s : ↑b), PolishSpace α
h✝ : ∀ (s : ↑b), IsClosed (f ⁻¹' ↑s)
Topen : ∀ (s : ↑b), IsOpen (f ⁻¹' ↑s)
t' : TopologicalSpace α
t'T : ∀ (i : ↑b), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
⊢ ∃ t', t' ≤ t ∧ Continuous f ∧ PolishSpace α
case intro.intro.intro
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
T : ↑b → TopologicalSpace α
Tt : ∀ (s : ↑b), T s ≤ t
Tpolish : ∀ (s : ↑b), PolishSpace α
h✝ : ∀ (s : ↑b), IsClosed (f ⁻¹' ↑s)
Topen : ∀ (s : ↑b), IsOpen (f ⁻¹' ↑s)
⊢ ∃ t', t' ≤ t ∧ Continuous f ∧ PolishSpace α
obtain ⟨t', t'T, t't, t'_polish⟩ :
  ∃ t' : TopologicalSpace α, (∀ i, t' ≤ T i) ∧ t' ≤ t ∧ @PolishSpace α t' :=
  exists_polishSpace_forall_le T Tt Tpolish
case intro.intro.intro.intro.intro.intro
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
T : ↑b → TopologicalSpace α
Tt : ∀ (s : ↑b), T s ≤ t
Tpolish : ∀ (s : ↑b), PolishSpace α
h✝ : ∀ (s : ↑b), IsClosed (f ⁻¹' ↑s)
Topen : ∀ (s : ↑b), IsOpen (f ⁻¹' ↑s)
t' : TopologicalSpace α
t'T : ∀ (i : ↑b), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
⊢ Continuous f
case intro.intro.intro.intro.intro.intro
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
T : ↑b → TopologicalSpace α
Tt : ∀ (s : ↑b), T s ≤ t
Tpolish : ∀ (s : ↑b), PolishSpace α
h✝ : ∀ (s : ↑b), IsClosed (f ⁻¹' ↑s)
Topen : ∀ (s : ↑b), IsOpen (f ⁻¹' ↑s)
t' : TopologicalSpace α
t'T : ∀ (i : ↑b), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
⊢ ∃ t', t' ≤ t ∧ Continuous f ∧ PolishSpace α
refine' ⟨t', t't, _, t'_polish⟩
case intro.intro.intro.intro.intro.intro
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
T : ↑b → TopologicalSpace α
Tt : ∀ (s : ↑b), T s ≤ t
Tpolish : ∀ (s : ↑b), PolishSpace α
h✝ : ∀ (s : ↑b), IsClosed (f ⁻¹' ↑s)
Topen : ∀ (s : ↑b), IsOpen (f ⁻¹' ↑s)
t' : TopologicalSpace α
t'T : ∀ (i : ↑b), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
s : Set β
hs : s ∈ b
⊢ IsOpen (f ⁻¹' s)
case intro.intro.intro.intro.intro.intro
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
T : ↑b → TopologicalSpace α
Tt : ∀ (s : ↑b), T s ≤ t
Tpolish : ∀ (s : ↑b), PolishSpace α
h✝ : ∀ (s : ↑b), IsClosed (f ⁻¹' ↑s)
Topen : ∀ (s : ↑b), IsOpen (f ⁻¹' ↑s)
t' : TopologicalSpace α
t'T : ∀ (i : ↑b), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
⊢ Continuous f
refine hb.continuous _ fun s hs => ?_
no goals
case intro.intro.intro.intro.intro.intro
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
T : ↑b → TopologicalSpace α
Tt : ∀ (s : ↑b), T s ≤ t
Tpolish : ∀ (s : ↑b), PolishSpace α
h✝ : ∀ (s : ↑b), IsClosed (f ⁻¹' ↑s)
Topen : ∀ (s : ↑b), IsOpen (f ⁻¹' ↑s)
t' : TopologicalSpace α
t'T : ∀ (i : ↑b), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
s : Set β
hs : s ∈ b
⊢ IsOpen (f ⁻¹' s)
exact t'T ⟨s, hs⟩ _ (Topen ⟨s, hs⟩)
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
s : ↑b
⊢ IsClopenable (f ⁻¹' ↑s)
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
⊢ ∀ (s : ↑b), IsClopenable (f ⁻¹' ↑s)
intro s
case hs
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
s : ↑b
⊢ MeasurableSet (f ⁻¹' ↑s)
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
s : ↑b
⊢ IsClopenable (f ⁻¹' ↑s)
apply MeasurableSet.isClopenable
no goals
case hs
α✝ : Type ?u.65771
inst✝⁶ : TopologicalSpace α✝
ι : Type ?u.65777
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : α → β
hf : Measurable f
b : Set (Set β)
b_count : Set.Countable b
hb : IsTopologicalBasis b
this : Encodable ↑b
s : ↑b
⊢ MeasurableSet (f ⁻¹' ↑s)
exact hf (hb.isOpen s.2).measurableSet