decide_false_iff

Mathlib.Data.Bool.Basic

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

English

The proposition decide p equals false if and only if p is false.

Русский

proposition decide p равно false тогда и только тогда, когда p ложно.

LaTeX

$$$$ \decide p = \mathrm{false} \iff \neg p. $$$$

Lean4

theorem decide_false_iff (p : Prop) {_ : Decidable p} : decide p = false ↔ ¬p :=
  bool_iff_false.symm.trans (not_congr (decide_iff _))

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

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

Разделы

Аффилиация

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