English
If x ∈ B is a base point, and v1 ∈ E1 x, v2 ∈ E2 x, then the product trivialization applied to ⟨x, (v1, v2)⟩ yields ⟨x, e1.continuousLinearEquivAt x v1, e2.continuousLinearEquivAt x v2⟩.
Русский
Пусть x ∈ B, и v1 ∈ E1 x, v2 ∈ E2 x. Применение произведённой тривиализации к ⟨x, (v1, v2)⟩ даёт ⟨x, e1.continuousLinearEquivAt x v1, e2.continuousLinearEquivAt x v2⟩.
LaTeX
$$$ \\text{prod } e_1 e_2 \\langle x, (v_1, v_2) \\rangle = \\langle x, e_1.continuousLinearEquivAt 𝕜 x \\flat v_1, e_2.continuousLinearEquivAt 𝕜 x \\flat v_2 \\rangle $$$
Lean4
theorem prod_apply' [e₁.IsLinear 𝕜] [e₂.IsLinear 𝕜] {x : B} (hx₁ : x ∈ e₁.baseSet) (hx₂ : x ∈ e₂.baseSet) (v₁ : E₁ x)
(v₂ : E₂ x) :
prod e₁ e₂ ⟨x, (v₁, v₂)⟩ = ⟨x, e₁.continuousLinearEquivAt 𝕜 x hx₁ v₁, e₂.continuousLinearEquivAt 𝕜 x hx₂ v₂⟩ :=
rfl
