English
If A is uniformly equicontinuous on S, then the closure of A remains uniformly equicontinuous on S.
Русский
Если A равномерно эконтинуально на S, то замыкание A остаётся равномерно эконтинуальным на 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`, its closure for the product
topology is also uniformly equicontinuous. This would also be true for the coarser topology of
pointwise convergence on `S`, see `UniformEquicontinuousOn.closure'`. -/
protected theorem closure {A : Set <| β → α} {S : Set β} (hA : A.UniformEquicontinuousOn S) :
(closure A).UniformEquicontinuousOn S :=
UniformEquicontinuousOn.closure' (u := id) hA
(Pi.continuous_restrict _)
/-
Implementation note: The following lemma (as well as all the following variations) could
theoretically be deduced from the "closure" statements above. For example, we could do:
```lean
theorem Filter.Tendsto.continuousAt_of_equicontinuousAt {l : Filter ι} [l.NeBot] {F : ι → X → α}
{f : X → α} {x₀ : X} (h₁ : Tendsto F l (𝓝 f)) (h₂ : EquicontinuousAt F x₀) :
ContinuousAt f x₀ :=
(equicontinuousAt_iff_range.mp h₂).closure.continuousAt
⟨f, mem_closure_of_tendsto h₁ <| Eventually.of_forall mem_range_self⟩
theorem Filter.Tendsto.uniformContinuous_of_uniformEquicontinuous {l : Filter ι} [l.NeBot]
{F : ι → β → α} {f : β → α} (h₁ : Tendsto F l (𝓝 f)) (h₂ : UniformEquicontinuous F) :
UniformContinuous f :=
(uniformEquicontinuous_iff_range.mp h₂).closure.uniformContinuous
⟨f, mem_closure_of_tendsto h₁ <| Eventually.of_forall mem_range_self⟩
```
Unfortunately, the proofs get painful when dealing with the relative case as one needs to change
the ambient topology. So it turns out to be easier to re-do the proof by hand.
-/
