false_of_a_eq_not_a

Mathlib.Tactic.CC.Lemmas

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.false_of_a_eq_not_a

Lean4

theorem false_of_a_eq_not_a {a : Prop} (h : a = Not a) : False :=
  have : Not a := fun ha ↦ absurd ha (Eq.mp h ha)
  absurd (Eq.mpr h this) this

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

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

Разделы

Аффилиация

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