English
If a set A of functions is uniformly equicontinuous on a domain, its closure is uniformly equicontinuous on that domain.
Русский
Если множество функций экьютельно равномерно на области, то его замыкание на этой области тоже экьютельно.
LaTeX
$$$A\text{ UniformEquicontinuous} \Rightarrow \overline{A}\text{ UniformEquicontinuous}$$$
Lean4
/-- If `𝓕 : ι → β → α` tends to `f : β → α` *pointwise on `S : Set β`* along some nontrivial
filter, and if the family `𝓕` is uniformly equicontinuous on `S`, then the limit is uniformly
continuous on `S`. -/
theorem uniformContinuousOn_of_uniformEquicontinuousOn {l : Filter ι} [l.NeBot] {F : ι → β → α} {f : β → α} {S : Set β}
(h₁ : ∀ x ∈ S, Tendsto (F · x) l (𝓝 (f x))) (h₂ : UniformEquicontinuousOn F S) : UniformContinuousOn f S :=
by
intro U hU; rw [mem_map]
rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
filter_upwards [h₂ V hV, mem_inf_of_right (mem_principal_self _)]
rintro ⟨x, y⟩ hxy ⟨hxS, hyS⟩
exact hVU <| hVclosed.mem_of_tendsto ((h₁ x hxS).prodMk_nhds (h₁ y hyS)) <| Eventually.of_forall hxy
