le_csInf_iff''

Mathlib.Order.ConditionallyCompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#le_csInf_iff''

English

If s is nonempty, a ≤ sInf s iff ∀ b ∈ s, a ≤ b.

Русский

Если s непусто, тогда a ≤ sInf s эквивалентно ∀ b ∈ s, a ≤ b.

LaTeX

$$$\text{Nonempty}(s) \Rightarrow \bigl(a \le sInf(s) \iff \forall b, b \in s \rightarrow a \le b\bigr)$$$

Lean4

theorem le_csInf_iff'' {s : Set α} {a : α} (ne : s.Nonempty) : a ≤ sInf s ↔ ∀ b : α, b ∈ s → a ≤ b :=
  le_csInf_iff (OrderBot.bddBelow _) ne

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

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

Разделы

Аффилиация

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