instEpiTopCatAppCounitTopCatAdjunction

English

For every TopCat X, the counit map topCatAdjunction.counit.app X is surjective (epi) in TopCat.

Русский

Для каждого X в TopCat отображение topCatAdjunction.counit.app X сюръективно (эпиморфно) в TopCat.

LaTeX

$$$\operatorname{Surjective}\bigl(\operatorname{topCatAdjunctionCounit}\,X\bigr).$$$

Lean4

instance (X : TopCat) : Epi (topCatAdjunction.counit.app X) :=
  by
  rw [TopCat.epi_iff_surjective]
  exact (topCatAdjunctionCounit_bijective _).2

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