cancel_iso_hom_right — Mathlib

English

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

Русский

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

LaTeX

$$$f \\circ g.{\\mathrm{hom}} = f' \\circ g.{\\mathrm{hom}} \\iff f = f'$$$

Lean4

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

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