of_decide_false

Mathlib.Data.Bool.Basic

URI: https://scilib.ai/kg/mathlib#Bool.of_decide_false

English

If p is decidable and decide(p) = false, then ¬p.

Русский

Если p разрешимо и decide(p) = false, тогда ¬p.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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