horiz_inv — Mathlib

English

If a commutative square consists of isomorphisms on the horizontal edges, then the square formed by taking the inverses on the corresponding edges also commutes.

Русский

Если в коммутативном квадрате вершины соединены изоморфизмами по горизонтали, то квадрат, образованный их обратными стрелками, также коммутирует.

LaTeX

$$$CommSq f.hom g h i.hom \rightarrow CommSq f.inv h g i.inv$$$

Lean4

theorem horiz_inv {f : W ≅ X} {i : Y ≅ Z} (p : CommSq f.hom g h i.hom) : CommSq f.inv h g i.inv :=
  flip (vert_inv (flip p))

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