cancel_natIso_inv_right — Mathlib

English

Cancellation on the right for a natural iso: if f ∘ α.hom.app Y = f' ∘ α.hom.app Y then f=f'.

Русский

Сокращение справа для натурального изоморфизма: если 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_inv_right {X : D} {Y : C} (f f' : X ⟶ G.obj Y) : f ≫ α.inv.app Y = f' ≫ α.inv.app Y ↔ f = f' := by
  simp only [cancel_mono, refl]

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