English
TendstoLocallyUniformly F f p is characterized by: for every neighborhood of 1 and every x, there exists a neighborhood t of x such that for i large, F_i(a)/f(a) ∈ U for all a ∈ t.
Русский
Сходимость локальная равномерна: для каждого окрестности единицы и каждой точки x существует окрестность t(x), внутри которой для больших i выполняется F_i(a)/f(a) ∈ U для всех a в t.
LaTeX
$$$\text{TendstoLocallyUniformly } F f p \iff \forall u \in 𝓝(1), \forall x, \exists t \in 𝓝(x), \forallᶠ i \in p, \forall a \in t, F_i(a)/f(a) ∈ u.$$$
Lean4
@[to_additive]
theorem tendstoUniformlyOn_iff (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α)
(hu : IsTopologicalGroup.toUniformSpace G = u) :
TendstoUniformlyOn F f p s ↔ ∀ u ∈ 𝓝 (1 : G), ∀ᶠ i in p, ∀ a ∈ s, F i a / f a ∈ u :=
hu ▸
⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ =>
mem_of_superset (h u hu) fun _ hi a ha => hv (hi a ha)⟩
