English
Let F be the functor from Compactum to CompHaus. Then F is essentially surjective: for every object Y of CompHaus there exists an object X of Compactum and an isomorphism F(X) ≅ Y.
Русский
Пусть F —функтор из категории Compactum в категорию CompHaus. Тогда F является эссенциально сюръективным: для каждого объекта Y в CompHaus существует объект X в Compactum и изоморфизм F(X) ≅ Y.
LaTeX
$$$\\forall Y \\in \\mathrm{Obj}(\\mathbf{CompHaus}),\\ \\exists X \\in \\mathrm{Obj}(\\mathbf{Compactum}), (\\mathrm{compactumToCompHaus})(X) \\cong Y.$$$
Lean4
/-- The functor `compactumToCompHaus` is essentially surjective. -/
instance essSurj : compactumToCompHaus.EssSurj :=
{ mem_essImage := fun X => ⟨Compactum.ofTopologicalSpace X, ⟨isoOfTopologicalSpace⟩⟩ }
