isCoatom_iff_isAtom — Mathlib

English

In a complemented modular lattice, if a and b are complements, then a is a coatom if and only if b is an atom.

Русский

В дополненной модульной решетке, если элементы a и b являются комплементарными, то a является коатомом тогда, когда b является атомом.

LaTeX

$$$ \\text{IsCoatom}(a) \\iff \\text{IsAtom}(b) \\quad \\text{given } \\text{IsCompl}(a,b)$$$

Lean4

theorem isCoatom_iff_isAtom : IsCoatom a ↔ IsAtom b :=
  hc.symm.isAtom_iff_isCoatom.symm

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