English
Definition: A family F: ι → X → α is equicontinuous at x0 if, for every entourage U of α, there exists a neighborhood V of x0 such that for all x in V and all i, (F_i(x0), F_i(x)) ∈ U.
Русский
Определение: семейство F: ι → X → α эквиконтинуально в точке x0, если для каждого окружения U пространства α найдется окрестность V точки x0 такая, что для всех x∈V и всех i выполняется (F_i(x0), F_i(x)) ∈ U.
LaTeX
$$$\forall U \in 𝓤(α), \forall^{\.} x \in 𝓝(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`* if, for all entourages `U ∈ 𝓤 α`, there is a neighborhood `V` of `x₀`
such that, for all `x ∈ V` and for all `i : ι`, `F i x` is `U`-close to `F i x₀`. -/
def EquicontinuousAt (F : ι → X → α) (x₀ : X) : Prop :=
∀ U ∈ 𝓤 α, ∀ᶠ x in 𝓝 x₀, ∀ i, (F i x₀, F i x) ∈ U
