English
Let F: ι → α → G and f: α → G. Then TendstoUniformly F f p is equivalent to uniform closeness to f across all a ∈ α: for every neighborhood of the identity, eventually all points satisfy F_i(a) / f(a) ∈ U.
Русский
Пусть F: ι → α → G и f: α → G. Тогда устойчивое сходство по Ф фильтру p эквивалентно тому, что для любого окрестности единицы почти все индексы i удовлетворяют F_i(a) / f(a) ∈ U одновременно для всех a.
LaTeX
$$$\text{TendstoUniformly } F f p \iff \forall U \in \mathcal{N}(1),\; \forall a, F_i(a) / f(a) \in U \text{ для i sufficiently large.}$$$
Lean4
@[to_additive]
theorem tendstoUniformly_iff (F : ι → α → G) (f : α → G) (p : Filter ι) (hu : IsTopologicalGroup.toUniformSpace G = u) :
TendstoUniformly F f p ↔ ∀ u ∈ 𝓝 (1 : G), ∀ᶠ i in p, ∀ a, 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 => hv (hi a)⟩
