cancel_iso_inv_left — Mathlib

English

Let f: Y ≅ X be an isomorphism in a category, and g, g': Y → Z be morphisms. Then f.inv ≫ g = f.inv ≫ g' if and only if g = g'.

Русский

Пусть f: Y ≅ X — изоморфизм в категории, и g, g': Y → Z — морфизмы. Тогда f.inv ≫ g = f.inv ≫ g' тогда и только тогда, когда g = g'.

LaTeX

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

Lean4

@[simp]
theorem cancel_iso_inv_left {X Y Z : C} (f : Y ≅ X) (g g' : Y ⟶ Z) : f.inv ≫ g = f.inv ≫ g' ↔ g = g' := by
  simp only [cancel_epi]

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