English
For any type X with a TopologicalSpace structure and a DeltaGeneratedSpace X, there is an object of the DeltaGenerated category obtained by the constructor, whose underlying topological space is X.
Русский
Для любого типа X с топологическим пространством и структурой DeltaGeneratedSpace существует объект в категории DeltaGenerated, получаемый конструктором, чья связанная с ним топологическая структура равна X.
LaTeX
$$$\\operatorname{of}(X) \\in \\mathrm{Obj}(\\DeltaGenerated)\\text{ with } \\operatorname{toTop}(\\operatorname{of}(X)) = \\mathrm{TopCat.of}(X)\\ \\text{and}\\ \\operatorname{deltaGenerated}(\\operatorname{of}(X)) = \\text{(the given } \\DeltaGeneratedSpace X).$$$
Lean4
/-- Constructor for objects of the category `DeltaGenerated` -/
abbrev of (X : Type u) [TopologicalSpace X] [DeltaGeneratedSpace X] : DeltaGenerated.{u}
where
toTop := TopCat.of X
deltaGenerated := ‹_›
