English
Let e1, e1' be linear trivializations of the bundle with fiber F1 over B, and e2, e2' be linear trivializations with fiber F2 over B. Then the product trivialization e1.prod e2 is linear with respect to 𝕜, provided e1 and e2 are linear for 𝕜.
Русский
Пусть e1, e1' — линейные тривиализации расслоения с волокном F1 над множеством B, а e2, e2' — линейные тривиализации с волокном F2 над B. Тогда произведённая тривиализация e1.prod e2 линейна по 𝕜, при условии линейности e1 и e2 по 𝕜.
LaTeX
$$$ (e_1 \text{ IsLinear } \\mathbb{K}) \\land (e_2 \\text{ IsLinear } \\mathbb{K}) \\Rightarrow (e_1 \\times e_2) \\text{ IsLinear } \\mathbb{K} $$$
Lean4
instance isLinear [e₁.IsLinear 𝕜] [e₂.IsLinear 𝕜] : (e₁.prod e₂).IsLinear 𝕜 where
linear := fun _ ⟨h₁, h₂⟩ => (((e₁.linear 𝕜 h₁).mk' _).prodMap ((e₂.linear 𝕜 h₂).mk' _)).isLinear
