compl_sup_compl_le

Mathlib.Order.Heyting.Basic

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

English

aᶜ ⊔ bᶜ ≤ (a ⊓ b)ᶜ.

Русский

aᶜ ⊔ bᶜ ≤ (a ⊓ b)ᶜ.

LaTeX

$$$a^{\complement} \sqcup b^{\complement} \le (a \land b)^{\complement}$$$

Lean4

theorem compl_sup_compl_le : aᶜ ⊔ bᶜ ≤ (a ⊓ b)ᶜ :=
  sup_le (compl_anti inf_le_left) <| compl_anti inf_le_right

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

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

Разделы

Аффилиация

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