cancel_unit_right_assoc' — Mathlib

English

General cancellation rule for sequences with a unit inserted on the far right; equality of two composites implies equality after removing the final unit.

Русский

Обобщённое правило отмены для цепочек с единицей на конце; равенство двух композиции эквивалентно равенству без последней единицы.

LaTeX

$$$\forall {W,X,X',Y} (f: W\to X)(g: X\to Y)(f': W\to X')(g': X'\to Y),\; f \cdot g \cdot u_Y = f' \cdot g' \cdot u_Y \iff f \cdot g = f' \cdot g'$$$

Lean4

@[simp]
theorem cancel_unit_right_assoc' {W X X' Y Y' Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) (f' : W ⟶ X') (g' : X' ⟶ Y')
    (h' : Y' ⟶ Z) : f ≫ g ≫ h ≫ e.unit.app Z = f' ≫ g' ≫ h' ≫ e.unit.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h' := by
  simp only [← Category.assoc, cancel_mono]

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