hnot_hnot_hnot

Mathlib.Order.Heyting.Basic

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

English

Triple negation collapses: ¬¬¬a = ¬a.

Русский

Тройное отрицание сводится к одному: ¬¬¬a = ¬a.

LaTeX

$$$$ \neg(\neg(\neg a)) = \neg a $$$$

Lean4

@[simp]
theorem hnot_hnot_hnot (a : α) : ￢￢￢a = ￢a :=
  hnot_hnot_le.antisymm <| hnot_anti hnot_hnot_le

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

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

Разделы

Аффилиация

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