continuous — Mathlib

English

Let F be a family of functions F_i: X → α that is equicontinuous. Then every member F_i is a continuous function.

Русский

Пусть F — семейство функций F_i: X → α, индексируемое ι, равноконтинуально. Тогда для каждого i ∈ ι функция F_i непрерывна.

LaTeX

$$$\\forall i : ι,\\ F_i \\in C(X, \\alpha)$$$

Lean4

/-- Each function of an equicontinuous family is continuous. -/
theorem continuous {F : ι → X → α} (h : Equicontinuous F) (i : ι) : Continuous (F i) :=
  continuous_iff_continuousAt.mpr fun x => (h x).continuousAt i

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