isCompl_bot_top — Mathlib

English

In any lattice with a bottom and a top, the bottom and the top are complements.

Русский

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

LaTeX

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

Lean4

theorem isCompl_bot_top : IsCompl (⊥ : α) ⊤ :=
  IsCompl.of_eq (bot_inf_eq _) (sup_top_eq _)

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