continuous — Mathlib

English

A uniform limit of continuous functions is continuous.

Русский

Единственный предел непрерывных функций в локальном равномерном смысле сохраняет непрерывность.

LaTeX

$$$TendstoLocallyUniformly.continuous$$$

Lean4

/-- A uniform limit of continuous functions is continuous. -/
protected theorem continuous (h : TendstoUniformly F f p) (hc : ∀ᶠ n in p, Continuous (F n)) [NeBot p] : Continuous f :=
  h.tendstoLocallyUniformly.continuous hc

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