complementedLattice_iff — Mathlib

English

A lattice with bounds is complemented iff every element has a complement.

Русский

Каждая ограниченная решётка является комплементированной тогда и только тогда, когда каждый элемент имеет комплемент.

LaTeX

$$$ComplementedLattice(\\alpha) \\Leftrightarrow \\forall a:\\alpha, \\exists b:\\alpha, IsCompl(a,b)$$$

Lean4

theorem complementedLattice_iff (α) [Lattice α] [BoundedOrder α] :
    ComplementedLattice α ↔ ∀ a : α, ∃ b : α, IsCompl a b :=
  ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

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