English
Same as 213104, with simp simplification, giving equality of coordinate changes for product and components.
Русский
См. 213104 с упрощением simp: равенство координатных изменений для произведения и каждого компонента.
LaTeX
$$$ ((e_1' \\times e_2').coordChangeL 𝕜 (e_1 \\times e_2) b) = (e_1.coordChangeL 𝕜 e_1' b) .prodMap (e_2.coordChangeL 𝕜 e_2' b) $$$
Lean4
/-- The product of two vector bundles is a vector bundle. -/
instance prod [VectorBundle 𝕜 F₁ E₁] [VectorBundle 𝕜 F₂ E₂] : VectorBundle 𝕜 (F₁ × F₂) (E₁ ×ᵇ E₂)
where
trivialization_linear' := by
rintro _ ⟨e₁, e₂, he₁, he₂, rfl⟩
infer_instance
continuousOn_coordChange' :=
by
rintro _ _ ⟨e₁, e₂, he₁, he₂, rfl⟩ ⟨e₁', e₂', he₁', he₂', rfl⟩
refine
(((continuousOn_coordChange 𝕜 e₁ e₁').mono ?_).prod_mapL 𝕜 ((continuousOn_coordChange 𝕜 e₂ e₂').mono ?_)).congr
?_ <;>
dsimp only [prod_baseSet, mfld_simps]
· mfld_set_tac
· mfld_set_tac
· rintro b hb
rw [ContinuousLinearMap.ext_iff]
rintro ⟨v₁, v₂⟩
change
(e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b (v₁, v₂) = (e₁.coordChangeL 𝕜 e₁' b v₁, e₂.coordChangeL 𝕜 e₂' b v₂)
rw [e₁.coordChangeL_apply e₁', e₂.coordChangeL_apply e₂', (e₁.prod e₂).coordChangeL_apply']
exacts [rfl, hb, ⟨hb.1.2, hb.2.2⟩, ⟨hb.1.1, hb.2.1⟩]
