decide_true

Mathlib.Data.Bool.Basic

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

English

If p holds, then decide p holds as true.

Русский

Если p истинно, то decide p истинно.

LaTeX

$$$$ p \rightarrow \decide p. $$$$

Lean4

theorem decide_true {p : Prop} [Decidable p] : p → decide p :=
  (decide_iff p).2

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

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

Разделы

Аффилиация

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