cancel_epi_assoc_iff — Mathlib

English

If f:X→Y is epi, then (f ≫ g) ≫ k = (f ≫ h) ≫ l if and only if g ≫ k = h ≫ l.

Русский

Если f:X→Y эпиморфизм, то ((f ≫ g) ≫ k) = ((f ≫ h) ≫ l) тогда эквивалентно (g ≫ k) = (h ≫ l).

LaTeX

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

Lean4

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

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