isStableUnderCoproductsOfShape_cofibrations

English

Coproducts of cofibrations are cofibrations; i.e., taking coprod maps componentwise preserves cofibrations.

Русский

Копробрации кофибраций — кофибрации; копродуктовые отображения сохраняют кофибрации.

LaTeX

$$$\\forall f_i:\\ X_i\\to Y_i\\ (i\\in J),\\ \\big(\\forall i\\in J,\\ f_i\\in \\mathrm{cofibrations}(C)\\big)\\Rightarrow (\\coprod_{i\\in J} f_i)\\in \\mathrm{cofibrations}(C).$$$

Lean4

instance isStableUnderCoproductsOfShape_cofibrations : (cofibrations C).IsStableUnderCoproductsOfShape J :=
  by
  rw [← trivialFibrations_llp]
  apply MorphismProperty.llp_isStableUnderCoproductsOfShape

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