English
If a uniformly convergent-on-filter sequence on a set and a target L with eventual convergence and the limit of L, then the limit of f follows in the target topology.
Русский
Если функция сходится равномерно по фильтру на множестве и есть предельное поведение L с предельной близостью, тогда f сходится к пределу ℓ во всём заданном топологическом пространстве.
LaTeX
$$$h1 : TendstoUniformlyOnFilter F f p p' \\Rightarrow (h2 : ∀ᶠ i in p, Tendsto (F i) p' (\\mathcal{Nhds} (L i))) \\land (h3 : Tendsto L p (\\mathcal{Nhds} \\ell)) \\Rightarrow \\ Tendsto f p' (\\mathcal{Nhds} \\ell)$$$
Lean4
theorem tendsto_of_eventually_tendsto (h1 : TendstoUniformlyOnFilter F f p p')
(h2 : ∀ᶠ i in p, Tendsto (F i) p' (𝓝 (L i))) (h3 : Tendsto L p (𝓝 ℓ)) : Tendsto f p' (𝓝 ℓ) :=
by
rw [tendsto_nhds_left]
intro s hs
rw [mem_map, Set.preimage, ← eventually_iff]
obtain ⟨t, ht, hts⟩ := comp3_mem_uniformity hs
have p1 : ∀ᶠ i in p, (L i, ℓ) ∈ t := tendsto_nhds_left.mp h3 ht
have p2 : ∀ᶠ i in p, ∀ᶠ x in p', (F i x, L i) ∈ t := by filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht
have p3 : ∀ᶠ i in p, ∀ᶠ x in p', (f x, F i x) ∈ t := (h1 t ht).curry
obtain ⟨i, p4, p5, p6⟩ := (p1.and (p2.and p3)).exists
filter_upwards [p5, p6] with x p5 p6 using hts ⟨F i x, p6, L i, p5, p4⟩
