α : Type u_1
β : Type u_2
γ : Type ?u.132725
ι : Type ?u.132728
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)))
⊢ IsSeparable (range f)
α : Type u_1
β : Type u_2
γ : Type ?u.132725
ι : Type ?u.132728
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
⊢ IsSeparable (range f)
have : IsSeparable (closure (⋃ n, range (hf.approx n))) :=
  (isSeparable_iUnion fun n => (SimpleFunc.finite_range (hf.approx n)).isSeparable).closure
α : Type u_1
β : Type u_2
γ : Type ?u.132725
ι : Type ?u.132728
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)))
⊢ range f ⊆ closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n))
α : Type u_1
β : Type u_2
γ : Type ?u.132725
ι : Type ?u.132728
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)))
⊢ IsSeparable (range f)
apply this.mono
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.132725
ι : Type ?u.132728
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)))
x : α
⊢ f x ∈ closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n))
α : Type u_1
β : Type u_2
γ : Type ?u.132725
ι : Type ?u.132728
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)))
⊢ range f ⊆ closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n))
rintro _ ⟨x, rfl⟩
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.132725
ι : Type ?u.132728
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)))
x : α
⊢ ∀ᶠ (x_1 : ℕ) in atTop, ↑(StronglyMeasurable.approx hf x_1) x ∈ ⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.132725
ι : Type ?u.132728
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)))
x : α
⊢ f x ∈ closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n))
apply mem_closure_of_tendsto (hf.tendsto_approx x)
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.132725
ι : Type ?u.132728
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)))
x : α
n : ℕ
⊢ ↑(StronglyMeasurable.approx hf n) x ∈ ⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.132725
ι : Type ?u.132728
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)))
x : α
⊢ ∀ᶠ (x_1 : ℕ) in atTop, ↑(StronglyMeasurable.approx hf x_1) x ∈ ⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)
refine eventually_of_forall fun n => ?_
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.132725
ι : Type ?u.132728
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)))
x : α
n : ℕ
⊢ ↑(StronglyMeasurable.approx hf n) x ∈ range ↑(StronglyMeasurable.approx hf n)
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.132725
ι : Type ?u.132728
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)))
x : α
n : ℕ
⊢ ↑(StronglyMeasurable.approx hf n) x ∈ ⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)
apply mem_iUnion_of_mem n
no goals
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.132725
ι : Type ?u.132728
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ (n : ℕ), range ↑(StronglyMeasurable.approx hf n)))
x : α
n : ℕ
⊢ ↑(StronglyMeasurable.approx hf n) x ∈ range ↑(StronglyMeasurable.approx hf n)
exact mem_range_self _