English
If a set A is equicontinuous within S at x0, then its closure inside Set X also remains equicontinuous within S at x0.
Русский
Если A экквинтоентно внутри S в x0, то его замыкание внутри множества X сохраняет экквинтоентность внутри S в x0.
LaTeX
$$$\\text{A EquicontinuousWithinAt } S x_0 \\Rightarrow \\overline{A} \\ EquicontinuousWithinAt S x_0.$$$
Lean4
/-- If a set of functions is equicontinuous at some `x₀` within a set `S`, its closure for the
product topology is also equicontinuous at `x₀` within `S`. This would also be true for the coarser
topology of pointwise convergence on `S ∪ {x₀}`, see `Set.EquicontinuousWithinAt.closure'`. -/
protected theorem closure {A : Set (X → α)} {S : Set X} {x₀ : X} (hA : A.EquicontinuousWithinAt S x₀) :
(closure A).EquicontinuousWithinAt S x₀ :=
hA.closure' (u := id) (Pi.continuous_restrict _) (continuous_apply _)
