English
There is a canonical way to regard any type X equipped with a topology that is compact and Hausdorff as an object of the category of compact Hausdorff spaces.
Русский
Существует канонический способ рассматривать любой тип X, оснащенный топологией, которая образует компактное и хаусдорфово пространство, как объект в категории компактных хаусдорфовых пространств.
LaTeX
$$$(X,\tau)$ with \tau \text{ compact and Hausdorff} \Rightarrow X \text{ is an object of } \mathbf{CompHaus}.$$
Lean4
/-- A constructor for objects of the category `CompHaus`,
taking a type, and bundling the compact Hausdorff topology
found by typeclass inference. -/
abbrev of : CompHaus :=
CompHausLike.of _ X
