csSup_le

Mathlib.Order.ConditionallyCompleteLattice.Basic

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

English

If s is nonempty and every b ∈ s satisfies b ≤ a, then sSup s ≤ a.

Русский

Если s ненулево и для каждого b ∈ s выполняется b ≤ a, то sSup s ≤ a.

LaTeX

$$$$ \text{If } s \neq \emptyset, \ \forall b \in s:\, b \le a \ \Rightarrow \ sSup s \le a. $$$$

Lean4

theorem csSup_le (h₁ : s.Nonempty) (h₂ : ∀ b ∈ s, b ≤ a) : sSup s ≤ a :=
  ConditionallyCompleteLattice.csSup_le s a h₁ h₂

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

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

Разделы

Аффилиация

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