English
Continuity of a bilinear composition in a fiber bundle with parameters m follows from the continuity of each part.
Русский
Непрерывность билинейного составления в расслоении с параметрами следует из непрерывности каждой части.
LaTeX
$$$\\text{ContinuousWithinAt}(\\lambda m,\\; TotalSpace.mk'(\\cdots))(F_3) s x \\Rightarrow \\cdots$$$
Lean4
/-- Consider `C^n` maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a basemap
`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
One can apply `ψ m` to `v m` and `w m`, and the resulting map is `C^n`. -/
theorem clm_bundle_apply₂
(hψ :
ContinuousWithinAt
(fun m ↦ TotalSpace.mk' (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (E := fun (x : B) ↦ (E₁ x →L[𝕜] E₂ x →L[𝕜] E₃ x)) (b m) (ψ m)) s
x)
(hv : ContinuousWithinAt (fun m ↦ TotalSpace.mk' F₁ (b m) (v m)) s x)
(hw : ContinuousWithinAt (fun m ↦ TotalSpace.mk' F₂ (b m) (w m)) s x) :
ContinuousWithinAt (fun m ↦ TotalSpace.mk' F₃ (b m) (ψ m (v m) (w m))) s x :=
(hψ.clm_bundle_apply hv).clm_bundle_apply hw
