English
Let nhds x0 and uniformity on α have HasBasis structures compatible with families F. Then EquicontinuousAt F x0 holds iff there exists a basis index for the left side such that F remains uniformly close for all x near x0 and all i.
Русский
Пусть пространства имеют совместимые базы для окрестностей и равномерности; тогда EquicontinuousAt F x0 эквивалентно существованию индекса базы, при котором F сохраняет равномерную близость для ближайших точек и для всех i.
LaTeX
$$$\\text{If } hX: (\\mathcal{N} x_0)\\HasBasis p_1 s_1 \\text{ and } hα: (\\mathcal{U} α)\\HasBasis p_2 s_2, \\\\ EquicontinuousAt F x_0 \\iff \\forall k_2, p_2 k_2 \\to \\exists k_1, p_1 k_1 \\,\\wedge \\, \\forall x \\in s_1 k_1, \\forall i, (F i x_0, F i x) \\in s_2 k_2.$$
Lean4
theorem equicontinuousAt_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set X} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)}
{F : ι → X → α} {x₀ : X} (hX : (𝓝 x₀).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) :
EquicontinuousAt F x₀ ↔ ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ i, (F i x₀, F i x) ∈ s₂ k₂ :=
by
rw [equicontinuousAt_iff_continuousAt, ContinuousAt, hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]
rfl
