instIsStableUnderRetractsTrivialFibrationsOfFibrationsOfWeakEquivalences

English

Analogous stability holds for trivial fibrations under retracts.

Русский

Аналогично тривиальные фибрации стабильны под retracts.

LaTeX

$$$\operatorname{IsStableUnderRetracts}\big(\operatorname{trivialFibrations}(C)\big)$$$

Lean4

instance [CategoryWithWeakEquivalences C] [CategoryWithFibrations C] [(fibrations C).IsStableUnderRetracts]
    [(weakEquivalences C).IsStableUnderRetracts] : (trivialFibrations C).IsStableUnderRetracts :=
  by
  dsimp [trivialFibrations]
  infer_instance

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