decide_iff

Mathlib.Data.Bool.Basic

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

English

For any proposition p, decide p equals true if and only if p holds, given a decision procedure.

Русский

Для любой пропозиции p, decide p равно true тогда и только тогда, когда p истинно, при наличии решения.

LaTeX

$$$$ \decide p = \mathrm{true} \iff p. $$$$

Lean4

theorem decide_iff (p : Prop) [d : Decidable p] : decide p = true ↔ p := by simp

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

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

Разделы

Аффилиация

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