initial_iff_empty — Mathlib

English

A type X is initial if and only if it is empty.

Русский

Тип X является начальным тогда и только тогда, когда он пуст.

LaTeX

$$$$ Nonempty(IsInitial X) \\iff IsEmpty X $$$$

Lean4

/-- An object in `Type u` is initial if and only if it is empty. -/
theorem initial_iff_empty (X : Type u) : Nonempty (IsInitial X) ↔ IsEmpty X :=
  by
  constructor
  · intro ⟨h⟩
    exact Function.isEmpty (IsInitial.to h PEmpty)
  · intro h
    exact ⟨IsInitial.ofIso Types.isInitialPunit <| Equiv.toIso <| Equiv.equivOfIsEmpty PEmpty X⟩

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