English
A family F_n tends uniformly to f on a filter p' if for every entourage u, eventually (f y, F_n y) ∈ u holds for all y in α simultaneously with respect to p'.
Русский
Семейство F_n сходится равномерно к f на фильтре p' если для каждого окружности u выполняется, что для всех y последовательность F_n(y) близка к f(y) по u почти всюду относительно p'.
LaTeX
$$$$\\text{TendstoUniformlyOnFilter}(F,f,p,p') \\equiv \\forall u\\in 𝓤(\\beta),\\ ∀^\\infty (n,y)\\in p×\\! p',\\ (f(y),F(n,y))\\in u.$$$$
Lean4
/-- A sequence of functions `Fₙ` converges uniformly on a filter `p'` to a limiting function `f`
with respect to the filter `p` if, for any entourage of the diagonal `u`, one has
`p ×ˢ p'`-eventually `(f x, Fₙ x) ∈ u`. -/
def TendstoUniformlyOnFilter (F : ι → α → β) (f : α → β) (p : Filter ι) (p' : Filter α) :=
∀ u ∈ 𝓤 β, ∀ᶠ n : ι × α in p ×ˢ p', (f n.snd, F n.fst n.snd) ∈ u
