cancel_mono_assoc_iff — Mathlib

English

If k ≫ (g ≫ f) = l ≫ (h ≫ f) with f mono, then k ≫ g = l ≫ h.

Русский

Пусть f моно и k ≫ (g ≫ f) = l ≫ (h ≫ f). Тогда k ≫ g = l ≫ h.

LaTeX

$$$ k \\circ (g \\circ f) = l \\circ (h \\circ f) \\iff k \\circ g = l \\circ h $$$

Lean4

theorem cancel_mono_assoc_iff (f : X ⟶ Y) [Mono f] {g h : Z ⟶ X} {W : C} {k l : W ⟶ Z} :
    k ≫ (g ≫ f) = l ≫ (h ≫ f) ↔ k ≫ g = l ≫ h :=
  ⟨fun p => (cancel_mono f).1 <| by simpa using p, fun p => by simp only [← Category.assoc, p]⟩

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