English
Let X, Y be topological spaces and α a uniform space. For a map u: Y → (X → α) and a subset A ⊆ Y, if the family {u_y : X → α} (y ∈ A) is equicontinuous on X and u is continuous, then the enlarged family indexed by the closure cl(A) is equicontinuous on X as well.
Русский
Пусть X, Y — топологические пространства, α — равномерное пространство. Пусть u: Y → X → α и A ⊆ Y. Если семейство {u_y : X → α} для y ∈ A экконтинуально на X и функция u непрерывна, тогда расширенное семейство, индексируемое по closure(A), остаётся экконтинуальным на X.
LaTeX
$$$\forall A \subseteq Y\; \forall u: Y \to X \to \alpha\; (\operatorname{Equicontinuous}(u \circ (\uparrow): A \to X \to \alpha) \land \operatorname{Continuous}(u)) \Rightarrow \operatorname{Equicontinuous}(u \circ (\uparrow): \overline{A} \to X \to \alpha)$$$
Lean4
/-- If a set of functions is equicontinuous, the same is true for its closure in *any*
topology for which evaluation at any point is continuous. Since this will be applied to
`DFunLike` types, we state it for any topological space with a map to `X → α` satisfying the right
continuity conditions. See also `Set.Equicontinuous.closure` for a more familiar statement. -/
theorem closure' {A : Set Y} {u : Y → X → α} (hA : Equicontinuous (u ∘ (↑) : A → X → α)) (hu : Continuous u) :
Equicontinuous (u ∘ (↑) : closure A → X → α) := fun x ↦ (hA x).closure' hu
