isAtom_iff_isCoatom — Mathlib

English

In a modular lattice, if a and b are complementary (IsCompl a b), then a is an atom iff b is a coatom.

Русский

В модульной решетке, если a и b комплементарны (IsCompl a b), тогда a — атом, тогда b — коатом.

LaTeX

$$$ IsCompl\ a\ b \Rightarrow (IsAtom\ a \iff IsCoatom\ b)$$$

Lean4

theorem isAtom_iff_isCoatom : IsAtom a ↔ IsCoatom b :=
  Set.isSimpleOrder_Iic_iff_isAtom.symm.trans <|
    hc.IicOrderIsoIci.isSimpleOrder_iff.trans Set.isSimpleOrder_Ici_iff_isCoatom

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