topIsoZero — Mathlib

English

There is an isomorphism between the terminal object in SimplexCategory and ⟦0⟧.

Русский

Существует изоморфизм между терминальным объектом в SimplexCategory и ⟦0⟧.

LaTeX

$$$\\top_{\\mathrm{SimplexCategory}} \\cong \\langle 0 \\rangle.$$$

Lean4

/-- The isomorphism between the terminal object in `SimplexCategory` and `⦋0⦌`. -/
noncomputable def topIsoZero : ⊤_ SimplexCategory ≅ ⦋0⦌ :=
  terminalIsoIsTerminal isTerminalZero

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