English
If a family F: X → α is uniformly equicontinuous as a function-valued set, then its closure in the space of functions is uniformly equicontinuous.
Русский
Если семейство функций равномерно эконтинуально, то его замыкание в пространстве функций также равномерно эконтинуально.
LaTeX
$$$A\,\text{UniformEquicontinuous} \Rightarrow \overline{A}\,\text{UniformEquicontinuous}$$$
Lean4
/-- If a set of functions is uniformly 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 `β → α` satisfying the right
continuity conditions. See also `Set.UniformEquicontinuous.closure` for a more familiar statement.
-/
theorem closure' {A : Set Y} {u : Y → β → α} (hA : UniformEquicontinuous (u ∘ (↑) : A → β → α)) (hu : Continuous u) :
UniformEquicontinuous (u ∘ (↑) : closure A → β → α) :=
by
rw [← uniformEquicontinuousOn_univ] at hA ⊢
exact hA.closure' (Pi.continuous_restrict _ |>.comp hu)
