isTerminalEquivIsoPUnit — Mathlib

English

A type X is terminal if and only if it is isomorphic to PUnit.

Русский

Тип X является терминальным тогда и только тогда, когда он изоморфен PUnit.

LaTeX

$$$$ IsTerminal X \\simeq (X \\cong PUnit) $$$$

Lean4

/-- A type is terminal if and only if it is isomorphic to `PUnit`. -/
noncomputable def isTerminalEquivIsoPUnit (X : Type u) : IsTerminal X ≃ (X ≅ PUnit) := by
  calc
    IsTerminal X ≃ Unique X := isTerminalEquivUnique _
    _ ≃ (X ≃ PUnit.{u + 1}) := (uniqueEquivEquivUnique _ _)
    _ ≃ (X ≅ PUnit) := equivEquivIso

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