instIsMultiplicativeCofibrations — Mathlib

English

Cofibrations are closed under finite products; in particular, the product of two cofibrations is a cofibration.

Русский

Кофибрации замкнуты по отношению к конечным произведениям; в частности, произведение двух кофибраций является кофибрацией.

LaTeX

$$$\\mathrm{Cofibrations}(C)^{\\mathrm{IsMultiplicative}}.$$$

Lean4

instance : (cofibrations C).IsMultiplicative :=
  by
  rw [← trivialFibrations_llp]
  infer_instance

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