equivEmptyEquiv — Mathlib

English

There is a canonical equivalence α ≃ Empty ≃ IsEmpty α; i.e., α is equivalent to Empty iff α is empty.

Русский

Существует каноническая эквивалентность α ≃ Empty ≃ IsEmpty α; то есть α эквивалентно Empty тогда и только тогда, когда α пуст.

LaTeX

$$$\alpha \simeq Empty \simeq IsEmpty(\alpha)$$$

Lean4

/-- `α` is equivalent to an empty type iff `α` is empty. -/
def equivEmptyEquiv (α : Sort u) : α ≃ Empty ≃ IsEmpty α :=
  ⟨fun e => Function.isEmpty e, @equivEmpty α, fun e => ext fun x => (e x).elim, fun _ => rfl⟩

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