sup_hnot_self

Mathlib.Order.Heyting.Basic

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

English

For all a, a ∨ ¬a = ⊤.

Русский

Для всякого a: a ∨ ¬a = ⊤.

LaTeX

$$$$ a \lor \neg a = \top $$$$

Lean4

@[simp]
theorem sup_hnot_self (a : α) : a ⊔ ￢a = ⊤ :=
  Codisjoint.eq_top codisjoint_hnot_right

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

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

Разделы

Аффилиация

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