unitInv_app_inverse — Mathlib

English

Relates unitInv to the counit via the inverse functor.

Русский

Соединяет unitInv с counit через обратный функтор.

LaTeX

$$$e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y)$$$

Lean4

theorem unitInv_app_inverse (e : C ≌ D) (Y : D) : e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y) :=
  by
  rw [← Iso.app_inv, ← Iso.app_hom, ← mapIso_hom, Eq.comm, ← Iso.hom_eq_inv]
  simpa using unit_app_inverse e Y

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