continuous_of_equicontinuous — Mathlib

English

If F: ι → X → α tends to f pointwise along a nontrivial filter and the family is equicontinuous at x0, then f is continuous at x0.

Русский

Если F: ι → X → α сходится по точкам к f вдоль ненулевого фильтра и семейство эконтинуально в x0, то f непрерывна в x0.

LaTeX

$$$\text{Tendsto }F\ l\ (\mathcal{N} f) \land \text{EquicontinuousAt } F x_0 \Rightarrow \text{ContinuousAt } f x_0$$$

Lean4

/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise* along some nontrivial filter, and if the
family `𝓕` is equicontinuous, then the limit is continuous. -/
theorem continuous_of_equicontinuous {l : Filter ι} [l.NeBot] {F : ι → X → α} {f : X → α} (h₁ : Tendsto F l (𝓝 f))
    (h₂ : Equicontinuous F) : Continuous f :=
  continuous_iff_continuousAt.mpr fun x => h₁.continuousAt_of_equicontinuousAt (h₂ x)

Похожие утверждения