English
If IsWeakFactorizationSystem(cofibrations, trivialFibrations) and all f_i are weak equivalences, then Limits.Sigma.map f is a weak equivalence.
Русский
Если имеется слабая факторизационная система кофибраций и тривиальная факторизационная система, и все f_i — слабые эквивалентности, то Limits.Sigma.map f — слабая эквивалентность.
LaTeX
$$$[IsWeakFactorizationSystem(\\mathrm{cofibrations}(C)) (\\mathrm{trivialFibrations}(C))] [\\forall i, \\mathrm{WeakEquivalence}(f_i)] : \\mathrm{WeakEquivalence}(\\mathrm{Limits}.\\Sigma.map\ n f).$$$
Lean4
instance [IsWeakFactorizationSystem (trivialCofibrations C) (fibrations C)] [∀ i, WeakEquivalence (f i)] :
WeakEquivalence (Limits.Sigma.map f) := by
rw [weakEquivalence_iff]
exact (MorphismProperty.colimMap (W := (trivialCofibrations C)) _ (fun ⟨i⟩ ↦ mem_trivialCofibrations (f i))).2
