instComplementedLattice — Mathlib

English

In a subsingleton lattice, the lattice is complemented.

Русский

В одноэлементной решётке всякая связность комплементирована.

LaTeX

$$$[Subsingleton\ α] \\Rightarrow ComplementedLattice(\\alpha)$$$

Lean4

theorem instComplementedLattice [Lattice α] [BoundedOrder α] [Subsingleton α] : ComplementedLattice α :=
  by
  refine ⟨fun a ↦ ⟨⊥, disjoint_bot_right, ?_⟩⟩
  rw [Subsingleton.elim ⊥ ⊤]
  exact codisjoint_top_right

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