sup_inf_inf_compl

Mathlib.Order.BooleanAlgebra.Basic

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

English

In a Boolean algebra, (x ∧ y) ∨ (x ∧ y^c) = x.

Русский

В булевой алгебре (x ∧ y) ∨ (x ∧ y^c) = x.

LaTeX

$$$(x \wedge y) \vee (x \wedge y^{c}) = x$$$

Lean4

@[simp]
theorem sup_inf_inf_compl : x ⊓ y ⊔ x ⊓ yᶜ = x := by rw [← sdiff_eq, sup_inf_sdiff _ _]

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

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

Разделы

Аффилиация

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