English
If two uniform convergences are eventually equal (pointwise equality eventually), they induce the same TendstoUniformlyOnFilter.
Русский
Если две равномерные последовательности сходятся и совпадают почти в пределе, они порождают одинаковый TendstoUniformlyOnFilter.
LaTeX
$$$$\\text{TendstoUniformlyOnFilter}(F,f,p,p')\\land\\forall^\\infty n\\in p×ˢ p', F(n)=F'(n)\\Rightarrow \\text{TendstoUniformlyOnFilter}(F',f,p,p').$$$$
Lean4
/-- A sequence of functions `Fₙ` converges uniformly on a set `s` to a limiting function `f` w.r.t.
filter `p` iff the function `(n, x) ↦ (f x, Fₙ x)` converges along `p ×ˢ 𝓟 s` to the uniformity.
In other words: one knows nothing about the behavior of `x` in this limit besides it being in `s`.
-/
theorem tendstoUniformlyOn_iff_tendsto :
TendstoUniformlyOn F f p s ↔ Tendsto (fun q : ι × α => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β) := by
simp [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto]
