right_triangle — Mathlib

English

For an equivalence e, the right zigzag is equal to the composition of the right and left unitor inverses up to iso.

Русский

Для эквивалентности e правая зигзагообразная конструкция равна композиции обратных правого и левого униторов (с учетом изоморфности).

LaTeX

$$$\\mathrm{rightZigzagIso}(e.unit, e.counit) = (\\rho_{e.inv}).trans (\\lambda_{e.inv}).symm$$$

Lean4

theorem right_triangle (e : a ≌ b) : rightZigzagIso e.unit e.counit = ρ_ e.inv ≪≫ (λ_ e.inv).symm :=
  Iso.ext (right_triangle_of_left_triangle e.unit e.counit e.left_triangle_hom)

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