square_from_iso_invert — Mathlib

English

Given i : X ≅ Y, p : Arrow T, and sq : Arrow.mk i.hom ⟶ p, we have i.inv ≫ sq.left ≫ p.hom = sq.right.

Русский

Пусть i: X ≅ Y, p: Arrow T, sq: Arrow.mk i.hom ⟶ p; тогда i.inv ≫ sq.left ≫ p.hom = sq.right.

LaTeX

$$$i.inv \circ sq.left \circ p.hom = sq.right$$$

Lean4

/-- Given a square from an isomorphism `i` to an arrow `p`, express the target part of `sq`
in terms of the inverse of `i`. -/
theorem square_from_iso_invert {X Y : T} (i : X ≅ Y) (p : Arrow T) (sq : Arrow.mk i.hom ⟶ p) :
    i.inv ≫ sq.left ≫ p.hom = sq.right := by simp only [Iso.inv_hom_id_assoc, Arrow.w, Arrow.mk_hom]

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