English
Let ψ m, v m, w m be C^n-differentiable in a neighborhood, with ψ m a bilinear map E1(b(m)) × E2(b(m)) → E3(b(m)). Then the map m ↦ ψ(m)(v(m), w(m)) is C^n-differentiable on the set.
Русский
Пусть векторные отображения ψ m задают билинейное отображение, зависящее C^n гладко от m, а v(m), w(m) — C^n-функции. Тогда m ↦ ψ(m)(v(m), w(m)) дифференцируема на множестве в смысле C^n.
LaTeX
$$$$\text{ContMDiffWithinAt } IM (IB.\prod 𝓘(\mathbb{k}, F_1 \to_L F_2 \to_L F_3)) n (m \mapsto \mathrm{TotalSpace.mk}' F_1 \ldots) s x \rightarrow\; \text{...}$$$$
Lean4
/-- Consider `C^n` maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a base map
`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`.
We give here a version of this statement within a set at a point. -/
theorem clm_bundle_apply₂
(hψ :
ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂ →L[𝕜] F₃)) n
(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 : ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F₁)) n (fun m ↦ TotalSpace.mk' F₁ (b m) (v m)) s x)
(hw : ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F₂)) n (fun m ↦ TotalSpace.mk' F₂ (b m) (w m)) s x) :
ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F₃)) n (fun m ↦ TotalSpace.mk' F₃ (b m) (ψ m (v m) (w m))) s x :=
hψ.clm_bundle_apply hv |>.clm_bundle_apply hw
