English
The product of two trivializations induces a mem-atlas structure for the product trivialization.
Русский
Произведение двух тривиализаций порождает структуру MemTrivializationAtlas для произведения тривиализаций.
LaTeX
$$$\mathrm{MemTrivializationAtlas}(e_1\,\mathrm{.prod}\, e_2)$$$
Lean4
/-- The product of two fiber bundles is a fiber bundle. -/
@[simps]
noncomputable instance prod : FiberBundle (F₁ × F₂) (E₁ ×ᵇ E₂)
where
totalSpaceMk_isInducing'
b := by
rw [← (Prod.isInducing_diag F₁ E₁ F₂ E₂).of_comp_iff]
exact (totalSpaceMk_isInducing F₁ E₁ b).prodMap (totalSpaceMk_isInducing F₂ E₂ b)
trivializationAtlas' :=
{e |
∃ (e₁ : Trivialization F₁ (π F₁ E₁)) (e₂ : Trivialization F₂ (π F₂ E₂)) (_ : MemTrivializationAtlas e₁) (_ :
MemTrivializationAtlas e₂), e = Trivialization.prod e₁ e₂}
trivializationAt' b := (trivializationAt F₁ E₁ b).prod (trivializationAt F₂ E₂ b)
mem_baseSet_trivializationAt' b := ⟨mem_baseSet_trivializationAt F₁ E₁ b, mem_baseSet_trivializationAt F₂ E₂ b⟩
trivialization_mem_atlas' b := ⟨trivializationAt F₁ E₁ b, trivializationAt F₂ E₂ b, inferInstance, inferInstance, rfl⟩
