isCompl_compl

Mathlib.Order.BooleanAlgebra.Basic

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

English

IsCompl x xᶜ; i.e., x and its complement form a complement pair.

Русский

IsCompl(x, xᶜ); то есть x и его комплемент образуют пару дополнений.

LaTeX

$$$\\text{IsCompl}(x, x^{c})$$$

Lean4

theorem isCompl_compl : IsCompl x xᶜ :=
  IsCompl.of_eq inf_compl_eq_bot' sup_compl_eq_top

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

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

Разделы

Аффилиация

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