English
IsTopologicalGroup.tendstoLocallyUniformlyOn_iff gives the criterion for TendstoLocallyUniformlyOn with a domain subset s: convergence is locally uniform around each point of s.
Русский
Критерий локальной равномерности на подмножество: сходимость локально-односна по каждому точке из s.
LaTeX
$$$\text{TendstoLocallyUniformlyOn } F f p s \iff \forall u \in 𝓝(1), \forall x \in s, \exists t \in 𝓝[x] , \forallᶠ i \in p, \forall a \in t, F_i(a)/f(a) ∈ u.$$$
Lean4
@[to_additive]
theorem tendstoLocallyUniformly_iff [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι)
(hu : IsTopologicalGroup.toUniformSpace G = u) :
TendstoLocallyUniformly F f p ↔ ∀ u ∈ 𝓝 (1 : G), ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ i in p, ∀ a ∈ t, F i a / f a ∈ u :=
hu ▸
⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ x =>
Exists.imp (fun _ ⟨h, hp⟩ => ⟨h, mem_of_superset hp fun _ hi a ha => hv (hi a ha)⟩) (h u hu x)⟩
