topCatAdjunctionCounitEquiv — Mathlib

English

The counit of the adjunction between lightCondSet and TopCat is bijective, realized by an equivalence topCatAdjunctionCounitEquiv.

Русский

Коунит адъюнкции между lightCondSet и TopCat является биекцией, реализованной эквивалентностью topCatAdjunctionCounitEquiv.

LaTeX

$$$ X.toLightCondSet.toTopCat \simeq X $$$

Lean4

/-- The counit of the adjunction `lightCondSetToTopCat ⊣ topCatToLightCondSet` is always bijective,
but not an isomorphism in general (the inverse isn't continuous unless `X` is sequential).
-/
noncomputable def topCatAdjunctionCounitEquiv (X : TopCat.{u}) : X.toLightCondSet.toTopCat ≃ X
    where
  toFun := topCatAdjunctionCounit X
  invFun x := ContinuousMap.const _ x

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