rightZigzagIso_symm — Mathlib

English

The right zigzag iso is symmetric to the left zigzag iso under inversion: rightZigzagIso η ε = (leftZigzagIso ε.symm η.symm)^{-1}.

Русский

Правый зигзаг-изоморфизм симметричен левому зигзаг-изоморфизмu при взятии обратного: rightZigzagIso η ε = (leftZigzagIso ε.symm η.symm)^{-1}.

LaTeX

$$$$ \text{rightZigzagIso } \eta \varepsilon = \big( \text{leftZigzagIso } \varepsilon^{\mathrm{symm}} \eta^{\mathrm{symm}} \big)^{-1}, $$$$

Lean4

@[simp]
theorem rightZigzagIso_symm : (rightZigzagIso η ε).symm = leftZigzagIso ε.symm η.symm :=
  Iso.ext (rightZigzagIso_inv η ε)

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