terminalIsoPUnit — Mathlib

English

There exists a canonical isomorphism between the terminal object and the one-point compact Hausdorff space.

Русский

Существует каноническое изоморфие между терминальным объектом и одноточечным компактно-хаусдорфовым пространством.

LaTeX

$$$\top_{\mathrm{CompHaus}} \cong \mathrm{CompHaus.of}(\mathrm{PUnit})$$$

Lean4

/-- The isomorphism from an arbitrary terminal object of `CompHaus` to a one-element space. -/
noncomputable def terminalIsoPUnit : ⊤_ CompHaus.{u} ≅ CompHaus.of PUnit :=
  terminalIsTerminal.uniqueUpToIso CompHaus.isTerminalPUnit

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