English
Reformulation of equicontinuity at a point: EquicontinuousAt F x0 is equivalent to the same pairwise U-condition but with nhds at x0 instead of nhdsWithin S.
Русский
Переформулировка эконтинуальности в точке: EquicontinuousAt F x0 эквивалентно тому же парному условию относительно окружностей, взятых в окрестности x0 без ограничения S.
LaTeX
$$$\text{EquicontinuousAt}(F,x_0) \iff \forall U \in \mathcal{U}(\alpha),\; \exists V \in \mathcal{N}(x_0),\; \forall x,y \in V,\; \forall i,(F(i,x),F(i,y))\in U$$$
Lean4
/-- Reformulation of equicontinuity at `x₀` comparing two variables near `x₀` instead of comparing
only one with `x₀`. -/
theorem equicontinuousAt_iff_pair {F : ι → X → α} {x₀ : X} :
EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ i, (F i x, F i y) ∈ U := by
simp_rw [← equicontinuousWithinAt_univ, equicontinuousWithinAt_iff_pair (mem_univ x₀), nhdsWithin_univ]
