English
If a family is equicontinuous within a set S at x0, then the closure of that family in an appropriate topology remains equicontinuous at x0.
Русский
Если семейство экквинтоентно внутри S в x0, то замыкание этого множества сохраняет экквинтоентность в x0.
LaTeX
$$$\\text{EquicontinuousWithinAt}(F,S,x_0) \\Rightarrow \\text{EquicontinuousWithinAt}(\\overline{F},S,x_0).$$$
Lean4
/-- If a set of functions is equicontinuous at some `x₀`, 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.EquicontinuousAt.closure` for a more familiar statement. -/
theorem closure' {A : Set Y} {u : Y → X → α} {x₀ : X} (hA : EquicontinuousAt (u ∘ (↑) : A → X → α) x₀)
(hu : Continuous u) : EquicontinuousAt (u ∘ (↑) : closure A → X → α) x₀ :=
by
rw [← equicontinuousWithinAt_univ] at hA ⊢
exact hA.closure' (Pi.continuous_restrict _ |>.comp hu) (continuous_apply x₀ |>.comp hu)
