isCompl_top_bot

Mathlib.Order.Disjoint

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

English

In any bounded lattice, the top and bottom are complements.

Русский

В любой ограниченной решётке верхний элемент ⊤ и нижний элемент ⊥ образуют пару комплементов.

LaTeX

$$$\\forall \\alpha\\ [Lattice \\alpha]\\ [BoundedOrder \\alpha], IsCompl(\\top : \\alpha) \\bot$$$

Lean4

theorem isCompl_top_bot : IsCompl (⊤ : α) ⊥ :=
  IsCompl.of_eq (inf_bot_eq _) (top_sup_eq _)

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

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

Разделы

Аффилиация

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