mul_mem_cancel_left — Mathlib

English

If hf ∈ S.arrows c d and f ≫ g ∈ S.arrows c e, then g ∈ S.arrows d e, equivalently f ≫ g ∈ S.arrows c e iff g ∈ S.arrows d e.

Русский

Пусть hf ∈ S.arrows c d. если f ≫ g ∈ S.arrows c e, то g ∈ S.arrows d e; эквивалентно f ≫ g ∈ S.arrows c e тогда g ∈ S.arrows d e.

LaTeX

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

Lean4

theorem mul_mem_cancel_left {c d e : C} {f : c ⟶ d} {g : d ⟶ e} (hf : f ∈ S.arrows c d) :
    f ≫ g ∈ S.arrows c e ↔ g ∈ S.arrows d e := by
  constructor
  · rintro h
    suffices Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e by simpa only [inv_eq_inv, IsIso.inv_hom_id_assoc] using this
    apply S.mul (S.inv hf) h
  · apply S.mul hf

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