isAtomic_of_isCoatomic_of_complementedLattice_of_isModular

English

If a lattice is Coatomic and complemented modular, then IsAtomic is equivalent to IsCoAtomic.

Русский

Если решетка коатомична и дополнена модульная, то атомность эквивалентна коатомности.

LaTeX

$$$ \\text{IsCoatomic}(\\alpha) \\iff \\text{IsAtomic}(\\alpha) $$$

Lean4

theorem isAtomic_of_isCoatomic_of_complementedLattice_of_isModular [IsCoatomic α] : IsAtomic α :=
  isCoatomic_dual_iff_isAtomic.1 isCoatomic_of_isAtomic_of_complementedLattice_of_isModular

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