α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ Measurable f ∧ IsSeparable (range f) → StronglyMeasurable f
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ StronglyMeasurable f ↔ Measurable f ∧ IsSeparable (range f)
refine' ⟨fun H => ⟨H.measurable, H.isSeparable_range⟩, _⟩
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
⊢ StronglyMeasurable f
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ Measurable f ∧ IsSeparable (range f) → StronglyMeasurable f
rintro ⟨H, H'⟩
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ StronglyMeasurable f
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
⊢ StronglyMeasurable f
letI := pseudoMetrizableSpacePseudoMetric β
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
⊢ StronglyMeasurable f
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ StronglyMeasurable f
let g := codRestrict f (closure (range f)) fun x => subset_closure (mem_range_self x)
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
⊢ StronglyMeasurable f
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
⊢ StronglyMeasurable f
have fg : f = ((↑) : closure (range f) → β) ∘ g := by
  ext x
  rfl
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
⊢ StronglyMeasurable f
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
⊢ StronglyMeasurable f
have T : MeasurableEmbedding ((↑) : closure (range f) → β) := by
  apply ClosedEmbedding.measurableEmbedding
  exact closedEmbedding_subtype_val isClosed_closure
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
g_meas : Measurable g
⊢ StronglyMeasurable f
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
⊢ StronglyMeasurable f
have g_meas : Measurable g := by
  rw [fg] at H
  exact T.measurable_comp_iff.1 H
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
g_meas : Measurable g
this : SecondCountableTopology ↑(closure (range f))
⊢ StronglyMeasurable f
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
g_meas : Measurable g
⊢ StronglyMeasurable f
have : SecondCountableTopology (closure (range f)) := by
  suffices SeparableSpace (closure (range f)) by
    exact UniformSpace.secondCountable_of_separable _
  exact (IsSeparable.closure H').separableSpace
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
g_meas : Measurable g
this : SecondCountableTopology ↑(closure (range f))
g_smeas : StronglyMeasurable g
⊢ StronglyMeasurable f
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
g_meas : Measurable g
this : SecondCountableTopology ↑(closure (range f))
⊢ StronglyMeasurable f
have g_smeas : StronglyMeasurable g := Measurable.stronglyMeasurable g_meas
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
g_meas : Measurable g
this : SecondCountableTopology ↑(closure (range f))
g_smeas : StronglyMeasurable g
⊢ StronglyMeasurable (Subtype.val ∘ g)
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
g_meas : Measurable g
this : SecondCountableTopology ↑(closure (range f))
g_smeas : StronglyMeasurable g
⊢ StronglyMeasurable f
rw [fg]
no goals
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
g_meas : Measurable g
this : SecondCountableTopology ↑(closure (range f))
g_smeas : StronglyMeasurable g
⊢ StronglyMeasurable (Subtype.val ∘ g)
exact continuous_subtype_val.comp_stronglyMeasurable g_smeas
case h
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
x : α
⊢ f x = (Subtype.val ∘ g) x
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
⊢ f = Subtype.val ∘ g
ext x
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
x : α
⊢ f x = (Subtype.val ∘ g) x
rfl
case h
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
⊢ ClosedEmbedding Subtype.val
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
⊢ MeasurableEmbedding Subtype.val
apply ClosedEmbedding.measurableEmbedding
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
⊢ ClosedEmbedding Subtype.val
exact closedEmbedding_subtype_val isClosed_closure
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
H : Measurable (Subtype.val ∘ g)
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
⊢ Measurable g
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
⊢ Measurable g
rw [fg] at H
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
H : Measurable (Subtype.val ∘ g)
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
⊢ Measurable g
exact T.measurable_comp_iff.1 H
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
g_meas : Measurable g
⊢ SeparableSpace ↑(closure (range f))
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
g_meas : Measurable g
⊢ SecondCountableTopology ↑(closure (range f))
suffices SeparableSpace (closure (range f)) by
  exact UniformSpace.secondCountable_of_separable _
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
g_meas : Measurable g
⊢ SeparableSpace ↑(closure (range f))
exact (IsSeparable.closure H').separableSpace
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.136321
ι : Type ?u.136324
inst✝⁴ : Countable ι
f g✝ : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : Measurable f
H' : IsSeparable (range f)
this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
g : α → ↑(closure (range f)) := codRestrict f (closure (range f)) (_ : ∀ (x : α), f x ∈ closure (range f))
fg : f = Subtype.val ∘ g
T : MeasurableEmbedding Subtype.val
g_meas : Measurable g
this : SeparableSpace ↑(closure (range f))
⊢ SecondCountableTopology ↑(closure (range f))
exact UniformSpace.secondCountable_of_separable _