English
Definition: F is equicontinuous at x0 within a subset S if, for every entourage U, there exists a neighborhood V of x0 inside S such that for all x ∈ V ∩ S and all i, (F_i(x0), F_i(x)) ∈ U.
Русский
Определение: F эквиконтинуально в точке x0 внутри подмножества S, если для каждого окружения U существует окрестность V точки x0, лежащая в S, такая, что для всех x ∈ V ∩ S и всех i выполняется (F_i(x0), F_i(x)) ∈ U.
LaTeX
$$$EquicontinuousWithinAt(F,S,x_0) = \forall U \in 𝓤(α), \forall^{\.} x in 𝓝[S] x_0, \forall i, (F_i(x_0), F_i(x)) \in U$$$
Lean4
/-- A family `F : ι → X → α` of functions from a topological space to a uniform space is
*equicontinuous at `x₀ : X` within `S : Set X`* if, for all entourages `U ∈ 𝓤 α`, there is a
neighborhood `V` of `x₀` within `S` such that, for all `x ∈ V` and for all `i : ι`, `F i x` is
`U`-close to `F i x₀`. -/
def EquicontinuousWithinAt (F : ι → X → α) (S : Set X) (x₀ : X) : Prop :=
∀ U ∈ 𝓤 α, ∀ᶠ x in 𝓝[S] x₀, ∀ i, (F i x₀, F i x) ∈ U
