sSup — Mathlib

English

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

Русский

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

LaTeX

$$If ∀ i, f_i is Antitone, then Antitone( iSup_i f_i ).$$

Lean4

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

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