English
If a family is equicontinuous at x0 within S, then its closure in a topology making evaluation continuous on S preserves equicontinuity at x0.
Русский
Если семейство экквинтоентно в x0 внутри S, то его замыкание в любой топологии, где отображение в точке фиксирует непрерывность на S, сохраняет экквинтоентность в x0.
LaTeX
$$$\\text{EquicontinuousWithinAt}(F,S,x_0) \\Rightarrow \\text{EquicontinuousWithinAt} (u \\circ (↑) : \\mathrm{closure} A\\to X\\to \\alpha) x_0$ (для подходящих u и условий непрерывности).$$
Lean4
/-- If a set of functions is equicontinuous at some `x₀` within a set `S`, the same is true for its
closure in *any* topology for which evaluation at any `x ∈ S ∪ {x₀}` 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.EquicontinuousWithinAt.closure`
for a more familiar (but weaker) statement.
Note: This could *technically* be called `EquicontinuousWithinAt.closure` without name clashes
with `Set.EquicontinuousWithinAt.closure`, but we don't do it because, even with a `protected`
marker, it would introduce ambiguities while working in namespace `Set` (e.g, in the proof of
any theorem called `Set.something`). -/
theorem closure' {A : Set Y} {u : Y → X → α} {S : Set X} {x₀ : X}
(hA : EquicontinuousWithinAt (u ∘ (↑) : A → X → α) S x₀) (hu₁ : Continuous (S.restrict ∘ u))
(hu₂ : Continuous (eval x₀ ∘ u)) : EquicontinuousWithinAt (u ∘ (↑) : closure A → X → α) S x₀ :=
by
intro U hU
rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
filter_upwards [hA V hV, eventually_mem_nhdsWithin] with x hx hxS
rw [SetCoe.forall] at *
change A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V at hx
refine (closure_minimal hx <| hVclosed.preimage <| hu₂.prodMk ?_).trans (preimage_mono hVU)
exact (continuous_apply ⟨x, hxS⟩).comp hu₁
