iSup — Mathlib

English

If a family {f_i} of functions f_i: α → β is monotone, then the indexed supremum iSup_i f_i is monotone.

Русский

Если семейство функций {f_i} с отображениями f_i: α → β монотонно, то индексируемый супремум iSup_i f_i монотонен.

LaTeX

$$For a family f: i → α → β with ∀ i, Monotone(f_i), then Monotone(iSup_i f_i).$$

Lean4

protected theorem iSup (hf : ∀ i, Monotone (f i)) : Monotone (⨆ i, f i) :=
  Monotone.sSup (by simpa)

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