isTerminalEquivUnique — Mathlib

English

There exists a canonical equivalence between IsTerminal X and Unique X.

Русский

Существует каноническое эквивалентность между IsTerminal X и Unique X.

LaTeX

$$$$ IsTerminal X \\simeq Unique X $$$$

Lean4

/-- A type is terminal if and only if it contains exactly one element. -/
noncomputable def isTerminalEquivUnique (X : Type u) : IsTerminal X ≃ Unique X :=
  equivOfSubsingletonOfSubsingleton (fun h => ((Iso.toEquiv (terminalIsoIsTerminal h).symm).unique))
    (fun _ => IsTerminal.ofIso terminalIsTerminal (Equiv.toIso (Equiv.ofUnique _ _)))

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