isStableUnderProductsOfShape_fibrations

English

Let C be as above. For any index set J and any family f_i: X_i → Y_i (i ∈ J) of fibrations, the product map ∏_{i∈J} f_i: ∏ X_i → ∏ Y_i is a fibration.

Русский

Пусть C образует аналогичную систему. Для любой семьи фибраций f_i: X_i → Y_i индексируемой по J произведение маппирования ∏_{i∈J} f_i: ∏ X_i → ∏ Y_i является фибрацией.

LaTeX

$$$\\forall (f_i)_{i\\in J},\\ \\left(\\forall i\\in J,\\ f_i \\in \\mathrm{fibrations}(C)\\right) \\Rightarrow \\left(\\prod_{i\\in J} f_i \\in \\mathrm{fibrations}(C)\\right).$$$

Lean4

instance isStableUnderProductsOfShape_fibrations : (fibrations C).IsStableUnderProductsOfShape J :=
  by
  rw [← trivialCofibrations_rlp]
  apply MorphismProperty.rlp_isStableUnderProductsOfShape

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