em'

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#em'

English

Let p be a proposition. Then p or not p holds.

Русский

Пусть p — высказывание. Тогда либо p истинно, либо его отрицание истинно.

LaTeX

$$$p \lor \lnot p$$$

Lean4

theorem em' (p : Prop) : ¬p ∨ p :=
  (em p).symm

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

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

Разделы

Аффилиация

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