English
Reformulation of equicontinuity at x0 within a set S: EquicontinuousWithinAt F S x0 is equivalent to saying that for every entourage U of α, there exists a neighborhood V of x0 within S such that for all x,y in V and all i, (F(i,x), F(i,y)) ∈ U.
Русский
Переформулировка эконтинуальности в точке x0 внутри множества S: EquicontinuousWithinAt F S x0 эквивалентно тому, что для каждого окружения U в α существует окрестность V в nhdsWithin x0 S такая, что для всех x,y ∈ V и для всех i выполняется (F(i,x), F(i,y)) ∈ U.
LaTeX
$$$\text{EquicontinuousWithinAt}(F,S,x_0) \iff \forall U \in \mathcal{U}(\alpha),\; \exists V \in \mathcal{N}_S(x_0),\; \forall x,y \in V,\; \forall i, (F(i,x),F(i,y)) \in U$$$
Lean4
/-- Reformulation of equicontinuity at `x₀` within a set `S`, comparing two variables near `x₀`
instead of comparing only one with `x₀`. -/
theorem equicontinuousWithinAt_iff_pair {F : ι → X → α} {S : Set X} {x₀ : X} (hx₀ : x₀ ∈ S) :
EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ i, (F i x, F i y) ∈ U :=
by
constructor <;> intro H U hU
· rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩
refine ⟨_, H V hV, fun x hx y hy i => hVU (prodMk_mem_compRel ?_ (hy i))⟩
exact hVsymm.mk_mem_comm.mp (hx i)
· rcases H U hU with ⟨V, hV, hVU⟩
filter_upwards [hV] using fun x hx i => hVU x₀ (mem_of_mem_nhdsWithin hx₀ hV) x hx i
