inf_compl_eq_bot'

Mathlib.Order.BooleanAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#inf_compl_eq_bot'

English

In a Boolean algebra, x ∧ xᶜ = ⊥.

Русский

В булевой алгебре $x \wedge x^{c} = 0$.

LaTeX

$$$x \\land x^{c} = \\bot$$$

Lean4

theorem inf_compl_eq_bot' : x ⊓ xᶜ = ⊥ :=
  bot_unique <| BooleanAlgebra.inf_compl_le_bot x

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

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

Разделы

Аффилиация

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