continuous — Mathlib

English

A locally uniform limit of continuous functions is continuous.

Русский

Локальная равномерная предельная функция непрерывна.

LaTeX

$$$\text{TendstoLocallyUniformly.continuous}$$$

Lean4

/-- A locally uniform limit of continuous functions is continuous. -/
protected theorem continuous (h : TendstoLocallyUniformly F f p) (hc : ∀ᶠ n in p, Continuous (F n)) [NeBot p] :
    Continuous f :=
  continuousOn_univ.mp <| h.tendstoLocallyUniformlyOn.continuousOn <| hc.mono fun _n hn => hn.continuousOn

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