instIsMultiplicativeSchemeOfIsStableUnderBaseChange

English

If W is multiplicative, P is stable under base-change and multiplicative, then the source-local-closure (W, P) is multiplicative.

Русский

Если W мультипликативно, P стабильно по базовому изменению и мультипликативно, то sourceLocalClosure(W, P) мультипликативно.

LaTeX

$$$ W.IsMultiplicative \land P.IsStableUnderBaseChange \land P.IsMultiplicative \Rightarrow (sourceLocalClosure\ W\ P).IsMultiplicative $$$

Lean4

instance [W.IsMultiplicative] [P.IsStableUnderBaseChange] [P.IsMultiplicative] :
    (sourceLocalClosure W P).IsMultiplicative where

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