instIsCofibrantPOfFactorizationDataOfIsStableUnderCompositionCofibrations

English

Under suitable hypotheses, the factorization data yields a PathObject whose P component is cofibrant.

Русский

При некоторых условиях факторизационные данные дают PathObject, у которого компонент P кофибриван.

LaTeX

$$$IsCofibrant\,( PathObject.ofFactorizationData\, h ).P$$$

Lean4

instance [HasInitial C] [IsCofibrant A] [(cofibrations C).IsStableUnderComposition] :
    IsCofibrant (ofFactorizationData h).P :=
  isCofibrant_of_cofibration (ofFactorizationData h).ι

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