inv_counit_map — Mathlib

English

Same content as inv_counit_map, simplified for use with simp.

Русский

То же самое, что и inv_counit_map, упрощённо для использования simp.

LaTeX

$$inv (R.map (h.counit.app X)) = h.unit.app (R.obj X)$$

Lean4

/-- If the counit of an adjunction is an isomorphism, then its inverse on the image of R is given
by R whiskered with the unit. -/
@[simp]
theorem inv_counit_map {X : D} [IsIso (h.counit.app X)] : inv (R.map (h.counit.app X)) = h.unit.app (R.obj X) :=
  IsIso.inv_eq_of_inv_hom_id (h.right_triangle_components X)

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