English
A sequence F_n converges uniformly to f if every entourage u in the uniformity, the pairs (f(x), F_n(x)) lie in u for all x, eventually in n.
Русский
Последовательность F_n сходится равномерно к f, если для каждого окружности u в равномерности пары (f(x), F_n(x)) принадлежат u для всех x, когда n достаточно велик.
LaTeX
$$$$\\forall u\\in 𝓤(\\beta),\\ \\forall^\\infty n\\in \\mathbb{N},\\ \\forall x:\\ (f(x),F_n(x))\\in u.$$$$
Lean4
/-- A sequence of functions `Fₙ` converges uniformly to a limiting function `f` with respect to a
filter `p` if, for any entourage of the diagonal `u`, one has `p`-eventually
`(f x, Fₙ x) ∈ u` for all `x`. -/
def TendstoUniformly (F : ι → α → β) (f : α → β) (p : Filter ι) :=
∀ u ∈ 𝓤 β, ∀ᶠ n in p, ∀ x : α, (f x, F n x) ∈ u
