of — Mathlib · SciLib

English

Given a property P and a type X with the compact Hausdorff topology, the constructor CompHausLike.of produces an object in CompHausLike P.

Русский

Дано свойство P и тип X с компактно-хаусдорфовой топологией, конструктор CompHausLike.of порождает объект в CompHausLike P.

LaTeX

$$$\mathrm{CompHausLike.of}(P,X) \in \mathrm{CompHausLike}(P)$$$

Lean4

/-- A constructor for objects of the category `CompHausLike P`,
taking a type, and bundling the compact Hausdorff topology
found by typeclass inference. -/
abbrev of : CompHausLike P where
  toTop := TopCat.of X
  is_compact := ‹_›
  is_hausdorff := ‹_›
  prop := HasProp.hasProp

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