English
Let hα be a HasBasis for the uniformity on α. Then EquicontinuousAt F x0 is equivalent to: for each basis index k with p k, eventually near x0, for all i, (F i x0, F i x) ∈ s k.
Русский
Пусть hα — база для равномерности на α. Тогда EquicontinuousAt F x0 эквивалентно: для каждого индекса k с p k пределы у x0 для всех i удовлетворяют (F i x0, F i x) ∈ s k.
LaTeX
$$$\\text{If } h_\\alpha: (\\mathcal{U} \\alpha) \\text{ has basis } p s, \\ EquicontinuousAt F x_0 \\iff \\forall k, p k \\to \\forallᶠ x \\in \\mathcal{N} x_0, \\forall i, (F i x_0, F i x) \\in s_k.$$$
Lean4
theorem equicontinuousAt_iff_right {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → X → α} {x₀ : X}
(hα : (𝓤 α).HasBasis p s) : EquicontinuousAt F x₀ ↔ ∀ k, p k → ∀ᶠ x in 𝓝 x₀, ∀ i, (F i x₀, F i x) ∈ s k :=
by
rw [equicontinuousAt_iff_continuousAt, ContinuousAt, (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]
rfl
