propEquivPEmpty

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.propEquivPEmpty

← MathLib Explorer

English

The Sort of proofs of a false proposition is equivalent to PEmpty.

Русский

Тип доказательств ложного proposition эквивалентен PEmpty.

LaTeX

$$$p \simeq PEmpty \quad (p \text{ проп } , h : \neg p)$$$

Lean4

/-- The `Sort` of proofs of a false proposition is equivalent to `PEmpty`. -/
def propEquivPEmpty {p : Prop} (h : ¬p) : p ≃ PEmpty :=
  @equivPEmpty p <| IsEmpty.prop_iff.2 h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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