mul_mem_cancel_right — Mathlib

English

If hg ∈ S.arrows d e, then f ≫ g ∈ S.arrows c e iff f ∈ S.arrows c d.

Русский

Если hg ∈ S.arrows d e, то f ≫ g ∈ S.arrows c e тогда и только тогда, когда f ∈ S.arrows c d.

LaTeX

$$$(f \\;\\circ\\; g) \\in S.arrows\\ c e \\iff f \\in S.arrows\\ c d$ given hg ∈ S.arrows d e$$

Lean4

theorem mul_mem_cancel_right {c d e : C} {f : c ⟶ d} {g : d ⟶ e} (hg : g ∈ S.arrows d e) :
    f ≫ g ∈ S.arrows c e ↔ f ∈ S.arrows c d := by
  constructor
  · rintro h
    suffices (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d by
      simpa only [inv_eq_inv, IsIso.hom_inv_id, Category.comp_id, Category.assoc] using this
    apply S.mul h (S.inv hg)
  · exact fun hf => S.mul hf hg

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