instIsMultiplicative — Mathlib

English

IsStableUnderTransfiniteComposition is extended with monoidal multiplicativity.

Русский

Устойчивость по трансфинитной композиции расширяется монодной мультпликативностью.

LaTeX

$$$W \\text{ IsStableUnderTransfiniteComposition}$$$

Lean4

instance : W.IsMultiplicative
    where
  id_mem X := transfiniteCompositionsOfShape_le _ _ _ (TransfiniteCompositionOfShape.id W X).mem
  comp_mem f g hf hg := transfiniteCompositionsOfShape_le _ _ _ (TransfiniteCompositionOfShape.ofComp f g hf hg).mem

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