dec_em' — Mathlib

English

Let p be a proposition with a decision procedure. Then either p or its negation holds.

Русский

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

LaTeX

$$$\forall p : \mathrm{Prop}, \mathrm{Decidable}(p) \Rightarrow p \lor \lnot p$$$

Lean4

theorem dec_em' (p : Prop) [Decidable p] : ¬p ∨ p :=
  (dec_em p).symm

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