iSup_eq

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#IsLUB.iSup_eq

English

If a is an upper bound and IsLUB(range f) a holds, then the supremum of f equals a.

Русский

Если a является верхней границей и выполняется IsLUB(range f, a), то iSup f = a.

LaTeX

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

Lean4

theorem iSup_eq (h : IsLUB (range f) a) : ⨆ j, f j = a :=
  h.sSup_eq

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru