vert_inv — Mathlib

English

If a commutative square is given with isomorphisms on the vertical edges, then the square formed by taking the inverses of those isomorphisms also commutes.

Русский

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

LaTeX

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

Lean4

theorem vert_inv {g : W ≅ Y} {h : X ≅ Z} (p : CommSq f g.hom h.hom i) : CommSq i g.inv h.inv f :=
  ⟨by rw [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, p.w]⟩

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