of — Mathlib · SciLib

English

Given a type X with a topology, TopCat.of X is the corresponding object of TopCat. It is the canonical way to regard X as a TopCat object, whose carrier is X.

Русский

Пусть X — тип с топологией. Тогда TopCat.of X есть соответствующий объект в TopCat; это канонический способ рассмотреть X как объект TopCat с носителем X.

LaTeX

$$$\\mathrm{TopCat.of}(X) \\text{ is the object with carrier } X$$$

Lean4

/-- The object in `TopCat` associated to a type equipped with the appropriate
typeclasses. This is the preferred way to construct a term of `TopCat`. -/
abbrev of (X : Type u) [TopologicalSpace X] : TopCat :=
  ⟨X⟩

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