sInf_eq_top

Mathlib.Order.CompleteLattice.Basic

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

English

Let α be a complete lattice. The infimum of s is ⊤ iff every a ∈ s equals ⊤.

Русский

Пусть α — полная решётка. Тогда sInf s = ⊤ эквивалентно тому, что каждый элемент s равен ⊤.

LaTeX

$$$$ \operatorname{sInf} s = \top \iff \forall a \in s, a = \top $$$$

Lean4

@[simp]
theorem sInf_eq_top : sInf s = ⊤ ↔ ∀ a ∈ s, a = ⊤ :=
  @sSup_eq_bot αᵒᵈ _ _

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

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

Разделы

Аффилиация

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