right_triangle_hom — Mathlib

English

For an equivalence e, the right zigzag hom equals ρ_e.inv.hom ≫ λ_e.inv.

Русский

Для эквивалентности e правая зигзагообразная гом применяется к гомоморфизму правого унитора и левого, соответственно.

LaTeX

$$$\\mathrm{rightZigzag } e.unit.hom\\ e.counit.hom = (\\rho_{e.inv}).hom \\;\\circ\\; (\\lambda_{e.inv}).inv$$$

Lean4

theorem right_triangle_hom (e : a ≌ b) : rightZigzag e.unit.hom e.counit.hom = (ρ_ e.inv).hom ≫ (λ_ e.inv).inv :=
  congrArg Iso.hom e.right_triangle

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