English
If a family F: X → α converges to f pointwise on S and is equicontinuous at x0 within S, then f is continuous at x0 within S.
Русский
Если семейство F сходится по точкам к f на S и эконтинуально в точке x0 внутри S, то f непрерывна в x0 на S.
LaTeX
$$$(\forall x\in S,\ Tendsto (F·x)\ l\ (\mathcal{N}(f(x)))) \land Tendsto (F·x_0)\ l\ (\mathcal{N}(f(x_0))) \land EquicontinuousWithinAt F S x_0 \Rightarrow ContinuousWithinAt f S x_0$$$
Lean4
/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise on `S ∪ {x₀} : Set X`* along some nontrivial
filter, and if the family `𝓕` is equicontinuous at `x₀ : X` within `S`, then the limit is
continuous at `x₀` within `S`. -/
theorem continuousWithinAt_of_equicontinuousWithinAt {l : Filter ι} [l.NeBot] {F : ι → X → α} {f : X → α} {S : Set X}
{x₀ : X} (h₁ : ∀ x ∈ S, Tendsto (F · x) l (𝓝 (f x))) (h₂ : Tendsto (F · x₀) l (𝓝 (f x₀)))
(h₃ : EquicontinuousWithinAt F S x₀) : ContinuousWithinAt f S x₀ :=
by
intro U hU; rw [mem_map]
rcases UniformSpace.mem_nhds_iff.mp hU with ⟨V, hV, hVU⟩
rcases mem_uniformity_isClosed hV with ⟨W, hW, hWclosed, hWV⟩
filter_upwards [h₃ W hW, eventually_mem_nhdsWithin] with x hx hxS using
hVU <| ball_mono hWV (f x₀) <| hWclosed.mem_of_tendsto (h₂.prodMk_nhds (h₁ x hxS)) <| Eventually.of_forall hx
