English
A family F: ι → α → β converges locally uniformly to f on s if for every entourage u there is a small neighborhood t of each x ∈ s such that eventually (f y, F n y) ∈ u for all y ∈ t.
Русский
Семейство F локально равномерно сходится к f на s, если для любого окружения u найдётся окрестность t вокруг каждой точки x ∈ s, такая что для всех y ∈ t и больших n выполняется (f y, F n y) ∈ u.
LaTeX
$$$\\forall u \\in 𝓤(β), \\forall x ∈ s, \\exists t ∈ 𝓝[x] s, \\forall n, (f, F n) ∈ u \\text{ на } t$$$
Lean4
/-- A sequence of functions `Fₙ` converges locally uniformly on a set `s` to a limiting function
`f` with respect to a filter `p` if, for any entourage of the diagonal `u`, for any `x ∈ s`, one
has `p`-eventually `(f y, Fₙ y) ∈ u` for all `y` in a neighborhood of `x` in `s`. -/
def TendstoLocallyUniformlyOn (F : ι → α → β) (f : α → β) (p : Filter ι) (s : Set α) :=
∀ u ∈ 𝓤 β, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u
