subsingleton_of_isTerminal — Mathlib

English

If X is a terminal object in CommRingCat, then X.carrier is a subsingleton (i.e., has exactly one element).

Русский

Если X является терминальным объектом в CommRingCat, то его множество носит свойство subsingleton.

LaTeX

$$$\forall X\; (hX: IsTerminal X)\; \Rightarrow\; Subsingleton X.carrier$$

Lean4

theorem subsingleton_of_isTerminal {X : CommRingCat} (hX : IsTerminal X) : Subsingleton X :=
  (hX.uniqueUpToIso punitIsTerminal).commRingCatIsoToRingEquiv.toEquiv.subsingleton_congr.mpr
    (show Subsingleton PUnit by infer_instance)

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