English
Let A ⊆ Y and S ⊆ X be given, with u: Y → X → α. If the family (u ∘ ↑) is equicontinuous on S for all points of A and the restriction of u to S is continuous, then equicontinuity holds on S for the closure of A.
Русский
Пусть A ⊆ Y и S ⊆ X заданы, пусть u: Y → X → α. Если семейство (u ∘ ↑) экконтинуально на S для всех точек A и ограничение u на S непрерывно, то экконтинуальность сохраняется для closure(A) на S.
LaTeX
$$$\forall A\subseteq Y\; \forall S\subseteq X\; (\operatorname{EquicontinuousOn}(u \circ (\uparrow): A \to X \to \alpha)\ S) \land \operatorname{Continuous}(S\text{-restrict} \circ u) \Rightarrow \operatorname{EquicontinuousOn}(u \circ (\uparrow): \overline{A} \to X \to \alpha)\; S$$$
Lean4
/-- If a set of functions is equicontinuous on a set `S`, the same is true for its closure in *any*
topology for which evaluation at any `x ∈ S` 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.EquicontinuousOn.closure` for a more familiar
(but weaker) statement. -/
theorem closure' {A : Set Y} {u : Y → X → α} {S : Set X} (hA : EquicontinuousOn (u ∘ (↑) : A → X → α) S)
(hu : Continuous (S.restrict ∘ u)) : EquicontinuousOn (u ∘ (↑) : closure A → X → α) S := fun x hx ↦
(hA x hx).closure' hu <| by exact continuous_apply ⟨x, hx⟩ |>.comp hu
