complementedLattice_of_isAtomistic

English

If α is atomistic in addition to being modular and compactly generated, then α is complemented.

Русский

Если α атомистична, модульна и компактно порождаема, тогда α — комплементированная.

LaTeX

$$$ \text{ComplementedLattice}(\alpha) $ given IsAtomistic(α)$$

Lean4

/-- See [Theorem 6.6][calugareanu]. -/
theorem complementedLattice_of_isAtomistic [IsAtomistic α] : ComplementedLattice α :=
  complementedLattice_of_sSup_atoms_eq_top sSup_atoms_eq_top

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