instEpiTopCatAppCounitTopCatAdjunction

English

For every TopCat X, the map topCatAdjunction.counit.app X is an epimorphism (in fact bijective).

Русский

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

LaTeX

$$$\mathrm{epi}(\mathrm{topCatAdjunctionCounit}_X)$$$

Lean4

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

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