instCofibrationCompOfIsStableUnderCompositionCofibrations

English

If f: X → Y and g: Y → Z are cofibrations and cofibrations are stable under composition, then f ≫ g is a cofibration.

Русский

Если f: X → Y и g: Y → Z являются кофибрациями, и кофибрации устойчивы при композиции, то f ≫ g — кофибрация.

LaTeX

$$$\operatorname{Cofibration}(f\circ g)$$$

Lean4

instance [CategoryWithCofibrations C] [(cofibrations C).IsStableUnderComposition] [hf : Cofibration f]
    [hg : Cofibration g] : Cofibration (f ≫ g) :=
  (cofibration_iff _).2 ((cofibrations C).comp_mem _ _ hf.mem hg.mem)

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