topCatAdjunctionCounit_bijective — Mathlib

English

For every X in TopCat, the counit component topCatAdjunction.counit.app X is bijective (surjective and injective).

Русский

Для каждого X в TopCat компонентa коунита topCatAdjunction.counit.app X биективна (существует биекция на носителе пространства).

LaTeX

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

Lean4

theorem topCatAdjunctionCounit_bijective (X : TopCat.{u}) : Function.Bijective (topCatAdjunctionCounit X) :=
  (topCatAdjunctionCounitEquiv X).bijective

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