le_sSup_iff

Mathlib.Order.CompleteLattice.Defs

URI: https://scilib.ai/kg/mathlib#le_sSup_iff

English

IsLUB s a if and only if a is the least upper bound of s.

Русский

IsLUB s a эквивалентно тому, что a является наименьшей верхней границей множества s.

LaTeX

$$$ IsLUB\, s\ a \iff a = sSup\, s $$$

Lean4

theorem le_sSup_iff : a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b :=
  ⟨fun h _ hb => le_trans h (sSup_le hb), fun hb => hb _ fun _ => le_sSup⟩

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

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

Разделы

Аффилиация

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