sInf_eq_bot

Mathlib.Order.CompleteLattice.Defs

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

English

Dually, sInf s equals bottom iff for all b > bottom there exists a ∈ s with a < b.

Русский

Дуал: sInf s = ⊥ тогда, когда для каждого b > ⊥ существует a ∈ s с a < b.

LaTeX

$$$sInf s = \bot \;\iff\; \forall b > \bot,\; \exists a \in s,\; a < b$$$

Lean4

theorem sInf_eq_bot : sInf s = ⊥ ↔ ∀ b > ⊥, ∃ a ∈ s, a < b :=
  @sSup_eq_top αᵒᵈ _ _

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

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

Разделы

Аффилиация

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