multiplicativeClosure' — Mathlib

Lean4

/-- A variant of `multiplicativeClosure` in which compositions are taken on the left rather than
on the right. It is not intended to be used directly, and one should rather access this via
`multiplicativeClosure_eq_multiplicativeClosure'` in cases where the inductive principle of this
variant is needed. -/
inductive multiplicativeClosure' (W : MorphismProperty C) : MorphismProperty C
  | of {x y : C} (f : x ⟶ y) (hf : W f) : multiplicativeClosure' W f
  | id (x : C) : multiplicativeClosure' W (𝟙 x)
  |
  of_comp {x y z : C} (f : x ⟶ y) (g : y ⟶ z) (hf : W f) (hg : multiplicativeClosure' W g) :
    multiplicativeClosure' W (f ≫ g)

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