isTerminalPUnit — Mathlib

English

The one-element space is terminal in Profinite; i.e., there is a unique map from any profinite space to PUnit.

Русский

Одномерное пространство является терминальным в Profinite; то есть из любого профинидального пространства существует единственный отображение в PUnit.

LaTeX

$$$\\forall X \\;\\exists ! f:X\\to \\mathrm{PUnit}$$$

Lean4

/-- A one-element space is terminal in `Profinite` -/
abbrev isTerminalPUnit : IsTerminal (Profinite.of PUnit.{u + 1}) :=
  CompHausLike.isTerminalPUnit

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