instIsIsoFunctorSequentialCounitSequentialAdjunction

English

The counit of the sequential adjunction is an isomorphism; i.e., for each X, the morphism sequentialAdjunctionCounit X is an isomorphism.

Русский

Коунит последовательного сопряжения является изоморфизмом; то есть для каждого X отображение sequentialAdjunctionCounit X — изоморфизм.

LaTeX

$$$\text{IsIso}\bigl(\text{sequentialAdjunctionCounit}_{X}\bigr)$$$

Lean4

instance : IsIso sequentialAdjunction.{0}.counit :=
  by
  rw [NatTrans.isIso_iff_isIso_app]
  intro X
  exact inferInstanceAs (IsIso (sequentialAdjunctionCounitIso X).hom)

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