isStableUnderProductsOfShape_trivialFibrations

English

Products of trivial fibrations are trivial fibrations.

Русский

Произведения тривиальных фибраций остаются тривиальными фибрациями.

LaTeX

$$$\\prod_{i\\in J}(\\mathrm{trivialFibrations}(C))\\ni\\mathrm{trivialFibrations}(C).$$$

Lean4

instance isStableUnderProductsOfShape_trivialFibrations : (trivialFibrations C).IsStableUnderProductsOfShape J :=
  by
  rw [← cofibrations_rlp]
  apply MorphismProperty.rlp_isStableUnderProductsOfShape

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