English
Let l be a nontrivial filter, F: X→α, f: X→α, S⊆X and x0∈X. If F→f pointwise at x0 within S and F is equicontinuous within S at x0, then f is continuous at x0 within S.
Русский
Пусть l — ненулевой фильтр, F: X→α, f: X→α, S⊆X и x0∈X. Если F сходится по точкам к f в x0 внутри S и F эконтинуально внутри S в x0, то f непрерывна в x0 внутри S.
LaTeX
$$$\text{ContinuousWithinAt}(f,S,x_0)$ при условиях EquicontinuousWithinAt и Tendsto внутри nhdsWithin.$$
Lean4
/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise* along some nontrivial filter, and if the
family `𝓕` is equicontinuous at some `x₀ : X`, then the limit is continuous at `x₀`. -/
theorem 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₀ :=
by
rw [← continuousWithinAt_univ, ← equicontinuousWithinAt_univ, tendsto_pi_nhds] at *
exact continuousWithinAt_of_equicontinuousWithinAt (fun x _ ↦ h₁ x) (h₁ x₀) h₂
