instIsMultiplicativeW — Mathlib

English

The class W is stable under composition and contains identities; thus W is multiplicative on the source category.

Русский

Класс W стабилен при композиции и содержит тождественные стрелки; следовательно, W мультипликативен на исходной категории.

LaTeX

$$$(W P).IsMultiplicative$$$

Lean4

instance : (W P).IsMultiplicative
    where
  id_mem X Z _ := by simpa [id_comp] using Function.bijective_id
  comp_mem f g hf hg Z hZ := by simpa using Function.Bijective.comp (hf Z hZ) (hg Z hZ)

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