csSup_eq

Mathlib.Order.ConditionallyCompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#IsGreatest.csSup_eq

English

If IsGreatest s a holds, then sSup s = a.

Русский

Если элемент a является наибольшим элементом множества s, то супремум множества s равен a.

LaTeX

$$$IsGreatest(s, a) \rightarrow \mathrm{sSup}(s) = a$$$

Lean4

/-- A greatest element of a set is the supremum of this set. -/
theorem csSup_eq (H : IsGreatest s a) : sSup s = a :=
  H.isLUB.csSup_eq H.nonempty

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

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

Разделы

Аффилиация

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