instNonemptyOfIsCofibrant — Mathlib

English

If X and Y are cofibrant, then there exists a CofibrantBrownFactorization f.

Русский

Если X и Y являются cofibrant, то существует CofibrantBrownFactorization f.

LaTeX

$$$[\text{IsCofibrant } X] [\text{IsCofibrant } Y] \Rightarrow \text{Nonempty } (\text{CofibrantBrownFactorization } f)$$$

Lean4

instance [IsCofibrant X] [IsCofibrant Y] : Nonempty (CofibrantBrownFactorization f) :=
  ⟨.mk' f (MorphismProperty.factorizationData _ _ _)⟩

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