English
TendstoLocallyUniformlyOn_iff provides a criterion for TendstoLocallyUniformlyOn with a set s: uniform convergence relative to s holds pointwise with neighborhoods in the s-filter.
Русский
Критерий локальной равномерности по множеству s: равномерное сходство относительно s сохраняется в локальных окрестностях внутри s.
LaTeX
$$$\text{TendstoLocallyUniformlyOn } F f p s \iff \forall (u \in 𝓝(1))\, \forall x \in s,\; \exists t \in 𝓝[s] x,\; \forallᶠ i \in p, \forall a \in t, F_i(a)/f(a) ∈ u.$$$
Lean4
@[to_additive]
theorem tendstoLocallyUniformlyOn_iff [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α)
(hu : IsTopologicalGroup.toUniformSpace G = u) :
TendstoLocallyUniformlyOn F f p s ↔ ∀ u ∈ 𝓝 (1 : G), ∀ x ∈ s, ∃ t ∈ 𝓝[s] 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⟩
