α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ StronglyMeasurable g
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
⊢ StronglyMeasurable g
borelize β
case refine'_1
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ Measurable g

case refine'_2
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (range g)
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ StronglyMeasurable g
refine' stronglyMeasurable_iff_measurable_separable.2 ⟨_, _⟩
no goals
case refine'_1
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ Measurable g
exact measurable_of_tendsto_metrizable' u (fun i => (hf i).measurable) lim
case refine'_2.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
⊢ IsSeparable (range g)
case refine'_2
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (range g)
rcases u.exists_seq_tendsto with ⟨v, hv⟩
case refine'_2.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure (⋃ (i : ℕ), range (f (v i))))
⊢ IsSeparable (range g)
case refine'_2.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
⊢ IsSeparable (range g)
have : IsSeparable (closure (⋃ i, range (f (v i)))) :=
  (isSeparable_iUnion fun i => (hf (v i)).isSeparable_range).closure
case refine'_2.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure (⋃ (i : ℕ), range (f (v i))))
⊢ range g ⊆ closure (⋃ (i : ℕ), range (f (v i)))
case refine'_2.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure (⋃ (i : ℕ), range (f (v i))))
⊢ IsSeparable (range g)
apply this.mono
case refine'_2.intro.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure (⋃ (i : ℕ), range (f (v i))))
x : α
⊢ g x ∈ closure (⋃ (i : ℕ), range (f (v i)))
case refine'_2.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure (⋃ (i : ℕ), range (f (v i))))
⊢ range g ⊆ closure (⋃ (i : ℕ), range (f (v i)))
rintro _ ⟨x, rfl⟩
case refine'_2.intro.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure (⋃ (i : ℕ), range (f (v i))))
x : α
⊢ g x ∈ closure (⋃ (i : ℕ), range (f (v i)))
case refine'_2.intro.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure (⋃ (i : ℕ), range (f (v i))))
x : α
⊢ g x ∈ closure (⋃ (i : ℕ), range (f (v i)))
rw [tendsto_pi_nhds] at lim
case refine'_2.intro.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure (⋃ (i : ℕ), range (f (v i))))
x : α
⊢ ∀ᶠ (x_1 : ℕ) in atTop, ((fun i => f i x) ∘ v) x_1 ∈ ⋃ (i : ℕ), range (f (v i))
case refine'_2.intro.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure (⋃ (i : ℕ), range (f (v i))))
x : α
⊢ g x ∈ closure (⋃ (i : ℕ), range (f (v i)))
apply mem_closure_of_tendsto ((lim x).comp hv)
case refine'_2.intro.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure (⋃ (i : ℕ), range (f (v i))))
x : α
n : ℕ
⊢ ((fun i => f i x) ∘ v) n ∈ ⋃ (i : ℕ), range (f (v i))
case refine'_2.intro.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure (⋃ (i : ℕ), range (f (v i))))
x : α
⊢ ∀ᶠ (x_1 : ℕ) in atTop, ((fun i => f i x) ∘ v) x_1 ∈ ⋃ (i : ℕ), range (f (v i))
refine eventually_of_forall fun n => ?_
case refine'_2.intro.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure (⋃ (i : ℕ), range (f (v i))))
x : α
n : ℕ
⊢ ((fun i => f i x) ∘ v) n ∈ range (f (v n))
case refine'_2.intro.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure (⋃ (i : ℕ), range (f (v i))))
x : α
n : ℕ
⊢ ((fun i => f i x) ∘ v) n ∈ ⋃ (i : ℕ), range (f (v i))
apply mem_iUnion_of_mem n
no goals
case refine'_2.intro.intro
α : Type u_2
β : Type u_3
γ : Type ?u.191542
ι✝ : Type ?u.191545
inst✝⁴ : Countable ι✝
f✝ g✝ : α → β
ι : Type u_1
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure (⋃ (i : ℕ), range (f (v i))))
x : α
n : ℕ
⊢ ((fun i => f i x) ∘ v) n ∈ range (f (v n))
exact mem_range_self _