decide_false — Mathlib

English

For any decidable proposition p, if ¬p holds, then decide(p) = false.

Русский

Пусть p — произвольное высказывание с допустимым разрешением. Если p ложно, то значение decide(p) равно false.

LaTeX

$$$$ \forall p\, [\operatorname{Decidable}(p)]\rightarrow (\neg p\rightarrow \operatorname{decide}(p) = \mathrm{false}) $$$$

Lean4

theorem decide_false {p : Prop} [Decidable p] : ¬p → decide p = false :=
  (decide_false_iff p).2

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