English
The forward mapping for the product trivialization is given by sending a point p to its base coordinate and the corresponding fiber coordinates from each factor.
Русский
Впередиcтующее отображение для тривиализации произведения отсылает точку p к её базовой координате и соответствующим координатам волокон из каждого множителя.
LaTeX
$$$\mathrm{Prod.toFun'}(e_1,e_2)(p) = \langle p.1, (e_1\langle p.1,p.2.1\rangle).2, (e_2\langle p.1,p.2.2\rangle).2\rangle$$$
Lean4
/-- Given trivializations `e₁`, `e₂` for fiber bundles `E₁`, `E₂` over a base `B`, the forward
function for the construction `Trivialization.prod`, the induced
trivialization for the fiberwise product of `E₁` and `E₂`. -/
def toFun' : TotalSpace (F₁ × F₂) (E₁ ×ᵇ E₂) → B × F₁ × F₂ := fun p ↦ ⟨p.1, (e₁ ⟨p.1, p.2.1⟩).2, (e₂ ⟨p.1, p.2.2⟩).2⟩
