English
If f is an isomorphism and the trivial cofibrations/fibrations coexist as a weak factorization system, then f is a cofibration.
Русский
Если f — изоморфизм и существует слабая факторизационная система тривиальных кофибраций и фибраций, то f — кофибрация.
LaTeX
$$$[IsWeakFactorizationSystem(\\mathrm{trivialCofibrations}(C)) (\\mathrm{fibrations}(C))] [IsIso(f)] : \\mathrm{Cofibration}(f).$$$
Lean4
instance [IsWeakFactorizationSystem (trivialCofibrations C) (fibrations C)] [IsIso f] : Cofibration f :=
by
have := (fibrations C).llp_of_isIso f
rw [fibrations_llp] at this
simpa only [cofibration_iff] using this.1
