cancel_natIso_hom_right_assoc — Mathlib

English

Cancellation on the right for α.hom.app Y: f ∘ α.hom.app Y = f' ∘ α.hom.app Y implies f=f'.

Русский

Сокращение справа для α.hom.app Y: f ∘ α.hom.app Y = f' ∘ α.hom.app Y значит f=f'.

LaTeX

$$$ f \circ α.hom.app Y = f' \circ α.hom.app Y \Rightarrow f=f' $$$

Lean4

@[simp]
theorem cancel_natIso_hom_right_assoc {W X X' : D} {Y : C} (f : W ⟶ X) (g : X ⟶ F.obj Y) (f' : W ⟶ X')
    (g' : X' ⟶ F.obj Y) : f ≫ g ≫ α.hom.app Y = f' ≫ g' ≫ α.hom.app Y ↔ f ≫ g = f' ≫ g' := by
  simp only [← Category.assoc, cancel_mono, refl]

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