isLUB_iSup — Mathlib

English

The supremum iSup f of a function f has the universal upper bound property for the range of f; equivalently, the range of f has iSup f as a least upper bound.

Русский

Предел наибольшей верхней границы iSup f является наименьшей верхней границей множества range f.

LaTeX

$$$$\\text{IsLUB}(\\operatorname{range}(f), \\iSup_j f(j)).$$$$

Lean4

theorem isLUB_iSup : IsLUB (range f) (⨆ j, f j) :=
  isLUB_sSup _

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