flip — Mathlib

English

The commutative square in the opposite category associated to a commutative square is again a commutative square, obtained by reversing arrows.

Русский

Коммутативный квадрат в противоположной категории, связанный с коммутативным квадратом, снова является коммутативным квадратом, полученным путём обращения стрелок.

LaTeX

$$$\text{flip} : CommSq f g h i \mapsto CommSq i^{op} h^{op} g^{op} f^{op}.$$$

Lean4

theorem flip (p : CommSq f g h i) : CommSq g f i h :=
  ⟨p.w.symm⟩

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