sSup_le_iff

Mathlib.Order.CompleteLattice.Defs

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

English

For any s ⊆ α and a, sSup s ≤ a if and only if ∀ b ∈ s, b ≤ a.

Русский

Для любого s ⊆ α и a, sSup s ≤ a тогда и только тогда, когда ∀ b ∈ s, b ≤ a.

LaTeX

$$$ sSup\ s ≤ a \iff \forall b \in s, b \le a $$$

Lean4

@[simp]
theorem sSup_le_iff : sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a :=
  isLUB_le_iff (isLUB_sSup s)

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

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

Разделы

Аффилиация

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