isAtom_compl

Mathlib.Order.Atoms

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem isAtom_compl : IsAtom aᶜ ↔ IsCoatom a :=
  isCompl_compl.symm.isAtom_iff_isCoatom

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

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

Разделы

Аффилиация

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