hnot_sup_self

Mathlib.Order.Heyting.Basic

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

English

For all a, ¬a ∨ a = ⊤.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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