sSup — Mathlib

English

If a family {f_i} of functions f_i: α → β consists of monotone maps, then their pointwise supremum g(a) = sup_i f_i(a) is also monotone in a.

Русский

Если семейство функций {f_i} с отображениями f_i: α → β состоит только из монотонных отображений, то их точечный супремум g(a) = sup_i f_i(a) также монотонен по a.

LaTeX

$$If ∀ i, f_i is Monotone, then Monotone( iSup_i f_i ), i.e. ∀ a ≤ a', sup_i f_i(a) ≤ sup_i f_i(a').$$

Lean4

protected theorem sSup (hs : ∀ f ∈ s, Monotone f) : Monotone (sSup s) := fun _ _ h ↦ iSup_mono fun f ↦ hs f f.2 h

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