instIsVeryGoodOfFactorizationData

English

In a model category, the path object built from a factorization data data h is very good.

Русский

В модельной категории путь-объект, полученный из данных факторизации h, является очень хорошим.

LaTeX

$$$IsVeryGood( PathObject.ofFactorizationData\, h )$$$

Lean4

instance : (ofFactorizationData h).IsVeryGood
    where
  fibration_p := by simpa using inferInstanceAs (Fibration h.p)
  cofibration_ι := by dsimp; infer_instance

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