complementedLattice_iff_isAtomistic

English

In a suitable lattice, complementedness is equivalent to atomisticity. Specifically, ComplementedLattice α iff IsAtomistic α.

Русский

В подходящей решётке комплементированность эквивалентна атомистичности: ComplementedLattice α ⇔ IsAtomistic α.

LaTeX

$$$ \text{ComplementedLattice}(\alpha) \iff \text{IsAtomistic}(\alpha) $$$

Lean4

theorem complementedLattice_iff_isAtomistic : ComplementedLattice α ↔ IsAtomistic α :=
  by
  constructor <;> intros
  · exact isAtomistic_of_complementedLattice
  · exact complementedLattice_of_isAtomistic

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