isCoatom_compl

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#isCoatom_compl

English

In a Boolean algebra, the complement of a coatom is an atom.

Русский

В буловой алгебре комплемент коатомы является атомом.

LaTeX

$$$ IsCoatom(a^{c}) \iff IsAtom(a) $$$

Lean4

@[simp]
theorem isCoatom_compl : IsCoatom aᶜ ↔ IsAtom a :=
  isCompl_compl.symm.isCoatom_iff_isAtom

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru