English
Let (𝓝 x0).HasBasis p s be a basis for the neighborhoods of x0. Then EquicontinuousAt F x0 is equivalent to: for every basis index k with p k, there exists k with p k and for all x in s k and all indices i, (F i x0, F i x) belongs to every neighborhood in the basis.
Русский
Пусть (𝓝 x0).HasBasis p s является базисом окрестностей x0. Тогда EquicontinuousAt F x0 эквивалентно тому, что для каждого индекса k с p k существует k с p k и для всех x из s k и каждого i, пара (F i x0, F i x) принадлежит любому окрестному базиса.
LaTeX
$$$\\text{If } hX: (\\mathcal{N} x_0) \\text{ has basis } (p,s), \\; EquicontinuousAt F x_0 \\iff \\forall U \\in 𝓤 α, \\exists k, p k \\wedge \\forall x \\in s k, \\forall i, (F i x_0, F i x) \\in U.$$$
Lean4
theorem equicontinuousAt_iff_left {p : κ → Prop} {s : κ → Set X} {F : ι → X → α} {x₀ : X} (hX : (𝓝 x₀).HasBasis p s) :
EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ i, (F i x₀, F i x) ∈ U :=
by
rw [equicontinuousAt_iff_continuousAt, ContinuousAt, hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)]
rfl
