instIsMultiplicativeTrivialCofibrations

English

Another instance asserting the stability under base change for fibrations in the presence of a weak factorization system.

Русский

Еще одно утверждение о стабильности под base change для фибраций в присутствии слабой факторизационной системы.

LaTeX

$$$\operatorname{IsStableUnderBaseChange}\big(\operatorname{fibrations}C\big)$$$

Lean4

instance : (trivialCofibrations C).IsMultiplicative :=
  by
  rw [← fibrations_llp]
  infer_instance

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