elim

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#Fact.elim

English

From a proof of p packaged as a Fact, deduce p.

Русский

Из доказательства p, упакованного как факт, следует p.

LaTeX

$$$\\mathrm{Fact}(p) \\Rightarrow p.$$$

Lean4

theorem elim {p : Prop} (h : Fact p) : p :=
  h.1

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

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

Разделы

Аффилиация

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