EquicontinuousOn — Mathlib

English

We say that a set H of functions is equicontinuous on a subset S if the lifted map is equicontinuous on S.

Русский

Говорят, что множество функций эквиконтинуально на подмножестве S, если соответствующее отображение эквиконтинуально на S.

LaTeX

$$EquicontinuousOn(F,S) := EquicontinuousWithinAt( (↑) : H → X → α ) S x0$$

Lean4

/-- A family `F : ι → X → α` of functions from a topological space to a uniform space is
*equicontinuous on `S : Set X`* if it is equicontinuous *within `S`* at each point of `S`. -/
def EquicontinuousOn (F : ι → X → α) (S : Set X) : Prop :=
  ∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀

Похожие утверждения