English
If IsWeakFactorizationSystem(cofibrations, trivialFibrations) holds and each f_i is a cofibration, then coprod.map f1 f2 is a cofibration.
Русский
Если выполняется слабая факторизационная система кофибраций и каждый f_i — кофибрация, то coprod.map f1 f2 — кофибрация.
LaTeX
$$$[IsWeakFactorizationSystem(\\mathrm{cofibrations}(C)) (\\mathrm{trivialFibrations}(C))] [h_1:\\mathrm{Cofibration}(f_1)] [h_2:\\mathrm{Cofibration}(f_2)] : \\mathrm{Cofibration}(\\mathrm{coprod.map}\\ f_1\\ f_2).$$$
Lean4
instance [IsWeakFactorizationSystem (cofibrations C) (trivialFibrations C)] : Cofibration (Limits.Sigma.map f) :=
by
simp only [cofibration_iff] at h ⊢
exact MorphismProperty.colimMap _ (fun ⟨i⟩ ↦ h i)
