topCatAdjunctionCounit_bijective — Mathlib

English

For any TopCat X, the counit of the adjunction is bijective; more precisely, the map topCatAdjunctionCounit X is a bijection.

Русский

Для любого TopCat X сопутствующий counit биективен; точнее, отображение topCatAdjunctionCounit X является биекцией.

LaTeX

$$$\mathrm{topCatAdjunctionCounit}\,X\;\text{ is bijective}$$$

Lean4

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

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