out_proof

Mathlib.Data.Erased

URI: https://scilib.ai/kg/mathlib#Erased.out_proof

English

If a is an erased witness for a proposition p, then p holds.

Русский

Если a является стёртым свидетелем для утверждения p, то p истинно.

LaTeX

$$$p$$$

Lean4

/-- Extracts the erased value, if it is a proof. -/
theorem out_proof {p : Prop} (a : Erased p) : p :=
  out a

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

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

Разделы

Аффилиация

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