instMemTrivializationAtlasProdProd

English

The product of two fiber bundles is itself a fiber bundle with the product base and fiber data.

Русский

Произведение двух фибраций образует новое фибровое расслоение с базой и фиброй как произведение.

LaTeX

$$$\mathrm{FiberBundle}(F_1\times F_2, E_1\times^b E_2)$$$

Lean4

instance {e₁ : Trivialization F₁ (π F₁ E₁)} {e₂ : Trivialization F₂ (π F₂ E₂)} [MemTrivializationAtlas e₁]
    [MemTrivializationAtlas e₂] : MemTrivializationAtlas (e₁.prod e₂ : Trivialization (F₁ × F₂) (π (F₁ × F₂)(E₁ ×ᵇ E₂)))
    where out := ⟨e₁, e₂, inferInstance, inferInstance, rfl⟩

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