English
If a set A is uniformly equicontinuous on S, then its closure is uniformly equicontinuous on S.
Русский
Если множество функций равномерно эконтинуально на S, то его замыкание на S также равномерно эконтинуально.
LaTeX
$$$A\text{ UniformEquicontinuousOn } S\Rightarrow \overline{A}\text{ UniformEquicontinuousOn } S$$$
Lean4
/-- If a set of functions is uniformly equicontinuous on a set `S`, the same is true for its
closure in *any* topology for which evaluation at any `x ∈ S` i 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.UniformEquicontinuousOn.closure` for a more familiar
(but weaker) statement. -/
theorem closure' {A : Set Y} {u : Y → β → α} {S : Set β} (hA : UniformEquicontinuousOn (u ∘ (↑) : A → β → α) S)
(hu : Continuous (S.restrict ∘ u)) : UniformEquicontinuousOn (u ∘ (↑) : closure A → β → α) S :=
by
intro U hU
rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
filter_upwards [hA V hV, mem_inf_of_right (mem_principal_self _)]
rintro ⟨x, y⟩ hxy ⟨hxS, hyS⟩
rw [SetCoe.forall] at *
change A ⊆ (fun f => (u f x, u f y)) ⁻¹' V at hxy
refine (closure_minimal hxy <| hVclosed.preimage <| .prodMk ?_ ?_).trans (preimage_mono hVU)
· exact (continuous_apply ⟨x, hxS⟩).comp hu
· exact (continuous_apply ⟨y, hyS⟩).comp hu
