English
Let hX be HasBasis for nhds within a set S. Then EquicontinuousWithinAt F S x0 is equivalent to: for every left-basis index, near x0 within S, for all i, (F i x0, F i x) ∈ s k.
Русский
Пусть hX задаёт базис для neighbourhoods внутри S. Тогда EquicontinuousWithinAt F S x0 эквивалентно: существуют индексы базиса, такие что при приближении в пределах S, для всех i выполняется (F i x0, F i x) ∈ s_k.
LaTeX
$$$\\text{If } h_X: (\\mathcal{N}[S] x_0) \\text{ HasBasis } p s, \\ EquicontinuousWithinAt F S x_0 \\iff \\forall k, p k \\to \\exists, \\forall x \\in s_k, \\forall i, (F_i x_0, F_i x) \\in U.$$$
Lean4
theorem equicontinuousWithinAt_iff_right {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → X → α} {S : Set X} {x₀ : X}
(hα : (𝓤 α).HasBasis p s) :
EquicontinuousWithinAt F S x₀ ↔ ∀ k, p k → ∀ᶠ x in 𝓝[S] x₀, ∀ i, (F i x₀, F i x) ∈ s k :=
by
rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
(UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]
rfl
