@@ -360,7 +360,7 @@ section TwoVariables
360360variable [∀ x, IsTopologicalAddGroup (E₃ x)] [∀ x, ContinuousSMul 𝕜 (E₃ x)]
361361 {ψ : ∀ x, (E₁ (b x) →L[𝕜] E₂ (b x) →L[𝕜] E₃ (b x))} {w : ∀ x, E₂ (b x)}
362362
363- /-- Consider `C^n` maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a base map
363+ /-- Consider `C^n` maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
364364`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
365365One can apply `ψ m` to `v m` and `w m`, and the resulting map is `C^n`.
366366
@@ -373,7 +373,7 @@ lemma ContMDiffWithinAt.clm_bundle_apply₂
373373 CMDiffAt[s] n (fun m ↦ TotalSpace.mk' F₃ (b m) (ψ m (v m) (w m))) x :=
374374 hψ.clm_bundle_apply hv |>.clm_bundle_apply hw
375375
376- /-- Consider `C^n` maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a base map
376+ /-- Consider `C^n` maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
377377`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
378378One can apply `ψ m` to `v m` and `w m`, and the resulting map is `C^n`.
379379
@@ -386,7 +386,7 @@ lemma ContMDiffAt.clm_bundle_apply₂
386386 CMDiffAt n (fun m ↦ TotalSpace.mk' F₃ (b m) (ψ m (v m) (w m))) x :=
387387 ContMDiffWithinAt.clm_bundle_apply₂ hψ hv hw
388388
389- /-- Consider `C^n` maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a base map
389+ /-- Consider `C^n` maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
390390`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
391391One can apply `ψ m` to `v m` and `w m`, and the resulting map is `C^n`.
392392
@@ -399,7 +399,7 @@ lemma ContMDiffOn.clm_bundle_apply₂
399399 CMDiff[s] n (fun m ↦ TotalSpace.mk' F₃ (b m) (ψ m (v m) (w m))) :=
400400 fun x hx ↦ (hψ x hx).clm_bundle_apply₂ (hv x hx) (hw x hx)
401401
402- /-- Consider `C^n` maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a base map
402+ /-- Consider `C^n` maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
403403`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
404404One can apply `ψ m` to `v m` and `w m`, and the resulting map is `C^n`. -/
405405lemma ContMDiff.clm_bundle_apply₂
@@ -417,7 +417,7 @@ section TwoVariables'
417417variable [∀ x, IsTopologicalAddGroup (E₃ x)] [∀ x, ContinuousSMul 𝕜 (E₃ x)]
418418 {ψ : ∀ x, (E₁ (b x) →L[𝕜] E₂ (b x) →L[𝕜] E₃ (b x))} {w : ∀ x, E₂ (b x)}
419419
420- /-- Consider differentiable maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a base map
420+ /-- Consider differentiable maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
421421`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
422422One can apply `ψ m` to `v m` and `w m`, and the resulting map is differentiable.
423423
@@ -430,7 +430,7 @@ lemma MDifferentiableWithinAt.clm_bundle_apply₂
430430 MDiffAt[s] (fun m ↦ TotalSpace.mk' F₃ (b m) (ψ m (v m) (w m))) x :=
431431 hψ.clm_bundle_apply hv |>.clm_bundle_apply hw
432432
433- /-- Consider differentiable maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a base map
433+ /-- Consider differentiable maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
434434`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
435435One can apply `ψ m` to `v m` and `w m`, and the resulting map is differentiable.
436436
@@ -443,7 +443,7 @@ lemma MDifferentiableAt.clm_bundle_apply₂
443443 MDiffAt (fun m ↦ TotalSpace.mk' F₃ (b m) (ψ m (v m) (w m))) x :=
444444 MDifferentiableWithinAt.clm_bundle_apply₂ hψ hv hw
445445
446- /-- Consider differentiable maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a base map
446+ /-- Consider differentiable maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
447447`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
448448One can apply `ψ m` to `v m` and `w m`, and the resulting map is differentiable.
449449
@@ -456,7 +456,7 @@ lemma MDifferentiableOn.clm_bundle_apply₂
456456 MDiff[s] (fun m ↦ TotalSpace.mk' F₃ (b m) (ψ m (v m) (w m))) :=
457457 fun x hx ↦ (hψ x hx).clm_bundle_apply₂ (hv x hx) (hw x hx)
458458
459- /-- Consider differentiable maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a base map
459+ /-- Consider differentiable maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
460460`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
461461One can apply `ψ m` to `v m` and `w m`, and the resulting map is differentiable. -/
462462lemma MDifferentiable.clm_bundle_apply₂
0 commit comments