cancel_iso_inv_right_assoc — Mathlib

English

Let f, f' : X → Y and g : Z ≅ Y. Then f ≫ g.inv = f' ≫ g.inv iff f = f'.

Русский

Пусть f, f' : X → Y и g : Z ≅ Y. Тогда f ≫ g.inv = f' ≫ g.inv тогда и только тогда, когда f = f'.

LaTeX

$$$f \\circ g^{-1} = f' \\circ g^{-1} \\iff f = f'$$$

Lean4

@[simp]
theorem cancel_iso_inv_right_assoc {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) (h : Z ≅ Y) :
    f ≫ g ≫ h.inv = f' ≫ g' ≫ h.inv ↔ f ≫ g = f' ≫ g' := by simp only [← Category.assoc, cancel_mono]

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