α : Type u_1
β✝ : Type ?u.138812
γ : Type ?u.138815
ι : Type ?u.138818
inst✝⁵ : Countable ι
f✝ g : α → β✝
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ StronglyMeasurable f
α : Type u_1
β✝ : Type ?u.138812
γ : Type ?u.138815
ι : Type ?u.138818
inst✝⁵ : Countable ι
f✝ g : α → β✝
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous f
⊢ StronglyMeasurable f
borelize β
case inl
α : Type u_1
β✝ : Type ?u.138812
γ : Type ?u.138815
ι : Type ?u.138818
inst✝⁵ : Countable ι
f✝ g : α → β✝
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
⊢ StronglyMeasurable f

case inr
α : Type u_1
β✝ : Type ?u.138812
γ : Type ?u.138815
ι : Type ?u.138818
inst✝⁵ : Countable ι
f✝ g : α → β✝
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology β
⊢ StronglyMeasurable f
α : Type u_1
β✝ : Type ?u.138812
γ : Type ?u.138815
ι : Type ?u.138818
inst✝⁵ : Countable ι
f✝ g : α → β✝
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ StronglyMeasurable f
cases h.out
case inl
α : Type u_1
β✝ : Type ?u.138812
γ : Type ?u.138815
ι : Type ?u.138818
inst✝⁵ : Countable ι
f✝ g : α → β✝
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
⊢ Measurable f ∧ IsSeparable (range f)
case inl
α : Type u_1
β✝ : Type ?u.138812
γ : Type ?u.138815
ι : Type ?u.138818
inst✝⁵ : Countable ι
f✝ g : α → β✝
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
⊢ StronglyMeasurable f
rw [stronglyMeasurable_iff_measurable_separable]
case inl
α : Type u_1
β✝ : Type ?u.138812
γ : Type ?u.138815
ι : Type ?u.138818
inst✝⁵ : Countable ι
f✝ g : α → β✝
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
⊢ IsSeparable (range f)
case inl
α : Type u_1
β✝ : Type ?u.138812
γ : Type ?u.138815
ι : Type ?u.138818
inst✝⁵ : Countable ι
f✝ g : α → β✝
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
⊢ Measurable f ∧ IsSeparable (range f)
refine' ⟨hf.measurable, _⟩
case inl
α : Type u_1
β✝ : Type ?u.138812
γ : Type ?u.138815
ι : Type ?u.138818
inst✝⁵ : Countable ι
f✝ g : α → β✝
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
⊢ IsSeparable (f '' univ)
case inl
α : Type u_1
β✝ : Type ?u.138812
γ : Type ?u.138815
ι : Type ?u.138818
inst✝⁵ : Countable ι
f✝ g : α → β✝
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
⊢ IsSeparable (range f)
rw [← image_univ]
no goals
case inl
α : Type u_1
β✝ : Type ?u.138812
γ : Type ?u.138815
ι : Type ?u.138818
inst✝⁵ : Countable ι
f✝ g : α → β✝
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
⊢ IsSeparable (f '' univ)
exact (isSeparable_of_separableSpace univ).image hf
no goals
case inr
α : Type u_1
β✝ : Type ?u.138812
γ : Type ?u.138815
ι : Type ?u.138818
inst✝⁵ : Countable ι
f✝ g : α → β✝
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology β
⊢ StronglyMeasurable f
exact hf.measurable.stronglyMeasurable