rightZigzagIso_inv — Mathlib

English

Similarly, the inverse of the right zigzag equals the left zigzag with inverted components: rightZigzagIso η ε .inv = leftZigzag ε.inv η.inv.

Русский

Аналогично, обратный правого зигзага равен левому зигзагу с инвертированными компонентами.

LaTeX

$$$$ (rightZigzagIso \eta \epsilon).inv = leftZigzag (\epsilon^{-1}) (\eta^{-1}). $$$$

Lean4

@[simp]
theorem rightZigzagIso_inv : (rightZigzagIso η ε).inv = leftZigzag ε.inv η.inv := by
  simp [bicategoricalComp, bicategoricalIsoComp]

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