Equivalence of smoothness with the basic definition for functions between vector spaces

• contMDiff_iff_contDiff: for functions between vector spaces, manifold-smoothness is equivalent to usual smoothness.
• ContinuousLinearMap.contMDiff: continuous linear maps between normed spaces are smooth
• smooth_smul: multiplication by scalars is a smooth operation

theorem contMDiffWithinAt_iff_contDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} {f : E → E'} {s : Set E} {x : E} : ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x

theorem ContMDiffWithinAt.contDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} {f : E → E'} {s : Set E} {x : E} : ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s x → ContDiffWithinAt 𝕜 n f s x

Alias of the forward direction of contMDiffWithinAt_iff_contDiffWithinAt.

theorem ContDiffWithinAt.contMDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} {f : E → E'} {s : Set E} {x : E} : ContDiffWithinAt 𝕜 n f s x → ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s x

Alias of the reverse direction of contMDiffWithinAt_iff_contDiffWithinAt.

theorem contMDiffAt_iff_contDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} {f : E → E'} {x : E} : ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f x ↔ ContDiffAt 𝕜 n f x

theorem ContMDiffAt.contDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} {f : E → E'} {x : E} : ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f x → ContDiffAt 𝕜 n f x

Alias of the forward direction of contMDiffAt_iff_contDiffAt.

theorem ContDiffAt.contMDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} {f : E → E'} {x : E} : ContDiffAt 𝕜 n f x → ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f x

Alias of the reverse direction of contMDiffAt_iff_contDiffAt.

theorem contMDiffOn_iff_contDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} {f : E → E'} {s : Set E} : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s ↔ ContDiffOn 𝕜 n f s

theorem ContMDiffOn.contDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} {f : E → E'} {s : Set E} : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s → ContDiffOn 𝕜 n f s

Alias of the forward direction of contMDiffOn_iff_contDiffOn.

theorem ContDiffOn.contMDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} {f : E → E'} {s : Set E} : ContDiffOn 𝕜 n f s → ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s

Alias of the reverse direction of contMDiffOn_iff_contDiffOn.

theorem contMDiff_iff_contDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} {f : E → E'} : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f ↔ ContDiff 𝕜 n f

theorem ContDiff.contMDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} {f : E → E'} : ContDiff 𝕜 n f → ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f

Alias of the reverse direction of contMDiff_iff_contDiff.

theorem ContMDiff.contDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} {f : E → E'} : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f → ContDiff 𝕜 n f

Alias of the forward direction of contMDiff_iff_contDiff.

theorem ContDiffWithinAt.comp_contMDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_7} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {n : WithTop ℕ∞} {g : F → F'} {f : M → F} {s : Set M} {t : Set F} {x : M} (hg : ContDiffWithinAt 𝕜 n g t (f x)) (hf : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F) n f s x) (h : s ⊆ f ⁻¹' t) : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F') n (g ∘ f) s x

theorem ContDiffAt.comp_contMDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_7} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {n : WithTop ℕ∞} {g : F → F'} {f : M → F} {s : Set M} {x : M} (hg : ContDiffAt 𝕜 n g (f x)) (hf : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F) n f s x) : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F') n (g ∘ f) s x

theorem ContDiffAt.comp_contMDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_7} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {n : WithTop ℕ∞} {g : F → F'} {f : M → F} {x : M} (hg : ContDiffAt 𝕜 n g (f x)) (hf : ContMDiffAt I (modelWithCornersSelf 𝕜 F) n f x) : ContMDiffAt I (modelWithCornersSelf 𝕜 F') n (g ∘ f) x

theorem ContDiff.comp_contMDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_7} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {n : WithTop ℕ∞} {g : F → F'} {f : M → F} {s : Set M} {x : M} (hg : ContDiff 𝕜 n g) (hf : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F) n f s x) : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F') n (g ∘ f) s x

theorem ContDiff.comp_contMDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_7} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {n : WithTop ℕ∞} {g : F → F'} {f : M → F} {x : M} (hg : ContDiff 𝕜 n g) (hf : ContMDiffAt I (modelWithCornersSelf 𝕜 F) n f x) : ContMDiffAt I (modelWithCornersSelf 𝕜 F') n (g ∘ f) x

theorem ContDiff.comp_contMDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_7} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {n : WithTop ℕ∞} {g : F → F'} {f : M → F} (hg : ContDiff 𝕜 n g) (hf : ContMDiff I (modelWithCornersSelf 𝕜 F) n f) : ContMDiff I (modelWithCornersSelf 𝕜 F') n (g ∘ f)

Linear maps between normed spaces are smooth

theorem ContinuousLinearMap.contMDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (L : E →L[𝕜] F) : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n ⇑L

theorem ContinuousLinearMap.contMDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (L : E →L[𝕜] F) {x : E} : ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n (⇑L) x

theorem ContinuousLinearMap.contMDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (L : E →L[𝕜] F) {s : Set E} {x : E} : ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n (⇑L) s x

theorem ContinuousLinearMap.contMDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (L : E →L[𝕜] F) {s : Set E} : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n (⇑L) s

theorem ContMDiffWithinAt.clm_precomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {f : M → F₁ →L[𝕜] F₂} {s : Set M} {x : M} (hf : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n f s x) : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 ((F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃)) n (fun (y : M) => ContinuousLinearMap.precomp F₃ (f y)) s x

theorem ContMDiffAt.clm_precomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {f : M → F₁ →L[𝕜] F₂} {x : M} (hf : ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n f x) : ContMDiffAt I (modelWithCornersSelf 𝕜 ((F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃)) n (fun (y : M) => ContinuousLinearMap.precomp F₃ (f y)) x

theorem ContMDiffOn.clm_precomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {f : M → F₁ →L[𝕜] F₂} {s : Set M} (hf : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n f s) : ContMDiffOn I (modelWithCornersSelf 𝕜 ((F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃)) n (fun (y : M) => ContinuousLinearMap.precomp F₃ (f y)) s

theorem ContMDiff.clm_precomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {f : M → F₁ →L[𝕜] F₂} (hf : ContMDiff I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n f) : ContMDiff I (modelWithCornersSelf 𝕜 ((F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃)) n fun (y : M) => ContinuousLinearMap.precomp F₃ (f y)

theorem ContMDiffWithinAt.clm_postcomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {f : M → F₂ →L[𝕜] F₃} {s : Set M} {x : M} (hf : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n f s x) : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃)) n (fun (y : M) => ContinuousLinearMap.postcomp F₁ (f y)) s x

theorem ContMDiffAt.clm_postcomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {f : M → F₂ →L[𝕜] F₃} {x : M} (hf : ContMDiffAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n f x) : ContMDiffAt I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃)) n (fun (y : M) => ContinuousLinearMap.postcomp F₁ (f y)) x

theorem ContMDiffOn.clm_postcomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {f : M → F₂ →L[𝕜] F₃} {s : Set M} (hf : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n f s) : ContMDiffOn I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃)) n (fun (y : M) => ContinuousLinearMap.postcomp F₁ (f y)) s

theorem ContMDiff.clm_postcomp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {f : M → F₂ →L[𝕜] F₃} (hf : ContMDiff I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n f) : ContMDiff I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃)) n fun (y : M) => ContinuousLinearMap.postcomp F₁ (f y)

theorem ContMDiffWithinAt.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M} {x : M} (hg : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g s x) (hf : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n f s x) : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n (fun (x : M) => (g x).comp (f x)) s x

theorem ContMDiffAt.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {x : M} (hg : ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g x) (hf : ContMDiffAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n f x) : ContMDiffAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n (fun (x : M) => (g x).comp (f x)) x

theorem ContMDiffOn.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M} (hg : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g s) (hf : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n f s) : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n (fun (x : M) => (g x).comp (f x)) s

theorem ContMDiff.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} (hg : ContMDiff I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g) (hf : ContMDiff I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n f) : ContMDiff I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n fun (x : M) => (g x).comp (f x)

theorem ContMDiffWithinAt.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} {x : M} (hg : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n g s x) (hf : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F₁) n f s x) : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F₂) n (fun (x : M) => (g x) (f x)) s x

Applying a linear map to a vector is smooth within a set. Version in vector spaces. For versions in nontrivial vector bundles, see ContMDiffWithinAt.clm_apply_of_inCoordinates and ContMDiffWithinAt.clm_bundle_apply.

theorem ContMDiffAt.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {x : M} (hg : ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n g x) (hf : ContMDiffAt I (modelWithCornersSelf 𝕜 F₁) n f x) : ContMDiffAt I (modelWithCornersSelf 𝕜 F₂) n (fun (x : M) => (g x) (f x)) x

Applying a linear map to a vector is smooth. Version in vector spaces. For versions in nontrivial vector bundles, see ContMDiffAt.clm_apply_of_inCoordinates and ContMDiffAt.clm_bundle_apply.

theorem ContMDiffOn.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} (hg : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n g s) (hf : ContMDiffOn I (modelWithCornersSelf 𝕜 F₁) n f s) : ContMDiffOn I (modelWithCornersSelf 𝕜 F₂) n (fun (x : M) => (g x) (f x)) s

theorem ContMDiff.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} (hg : ContMDiff I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n g) (hf : ContMDiff I (modelWithCornersSelf 𝕜 F₁) n f) : ContMDiff I (modelWithCornersSelf 𝕜 F₂) n fun (x : M) => (g x) (f x)

theorem ContMDiffWithinAt.cle_arrowCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_11} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄} {s : Set M} {x : M} (hf : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n (fun (x : M) => ↑(f x).symm) s x) (hg : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₃ →L[𝕜] F₄)) n (fun (x : M) => ↑(g x)) s x) : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) n (fun (y : M) => ↑((f y).arrowCongr (g y))) s x

theorem ContMDiffAt.cle_arrowCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_11} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄} {x : M} (hf : ContMDiffAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n (fun (x : M) => ↑(f x).symm) x) (hg : ContMDiffAt I (modelWithCornersSelf 𝕜 (F₃ →L[𝕜] F₄)) n (fun (x : M) => ↑(g x)) x) : ContMDiffAt I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) n (fun (y : M) => ↑((f y).arrowCongr (g y))) x

theorem ContMDiffOn.cle_arrowCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_11} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄} {s : Set M} (hf : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n (fun (x : M) => ↑(f x).symm) s) (hg : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₃ →L[𝕜] F₄)) n (fun (x : M) => ↑(g x)) s) : ContMDiffOn I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) n (fun (y : M) => ↑((f y).arrowCongr (g y))) s

theorem ContMDiff.cle_arrowCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_11} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄} (hf : ContMDiff I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n fun (x : M) => ↑(f x).symm) (hg : ContMDiff I (modelWithCornersSelf 𝕜 (F₃ →L[𝕜] F₄)) n fun (x : M) => ↑(g x)) : ContMDiff I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) n fun (y : M) => ↑((f y).arrowCongr (g y))

theorem ContMDiffWithinAt.clm_prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_11} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {s : Set M} {x : M} (hg : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g s x) (hf : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₄)) n f s x) : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) n (fun (x : M) => (g x).prodMap (f x)) s x

theorem ContMDiffAt.clm_prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_11} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {x : M} (hg : ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g x) (hf : ContMDiffAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₄)) n f x) : ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) n (fun (x : M) => (g x).prodMap (f x)) x

theorem ContMDiffOn.clm_prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_11} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {s : Set M} (hg : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g s) (hf : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₄)) n f s) : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) n (fun (x : M) => (g x).prodMap (f x)) s

theorem ContMDiff.clm_prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_8} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_9} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_10} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_11} [NormedAddCommGroup F₄] [NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} (hg : ContMDiff I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g) (hf : ContMDiff I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₄)) n f) : ContMDiff I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) n fun (x : M) => (g x).prodMap (f x)

Smoothness of scalar multiplication

theorem contMDiff_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_12} [NormedAddCommGroup V] [NormedSpace 𝕜 V] : ContMDiff ((modelWithCornersSelf 𝕜 𝕜).prod (modelWithCornersSelf 𝕜 V)) (modelWithCornersSelf 𝕜 V) ⊤ fun (p : 𝕜 × V) => p.1 • p.2

On any vector space, multiplication by a scalar is a smooth operation.

theorem ContMDiffWithinAt.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {n : WithTop ℕ∞} {V : Type u_12} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 𝕜) n f s x) (hg : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 V) n g s x) : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 V) n (fun (p : M) => f p • g p) s x

theorem ContMDiffAt.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} {n : WithTop ℕ∞} {V : Type u_12} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : ContMDiffAt I (modelWithCornersSelf 𝕜 𝕜) n f x) (hg : ContMDiffAt I (modelWithCornersSelf 𝕜 V) n g x) : ContMDiffAt I (modelWithCornersSelf 𝕜 V) n (fun (p : M) => f p • g p) x

theorem ContMDiffOn.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {n : WithTop ℕ∞} {V : Type u_12} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) n f s) (hg : ContMDiffOn I (modelWithCornersSelf 𝕜 V) n g s) : ContMDiffOn I (modelWithCornersSelf 𝕜 V) n (fun (p : M) => f p • g p) s

theorem ContMDiff.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {V : Type u_12} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : ContMDiff I (modelWithCornersSelf 𝕜 𝕜) n f) (hg : ContMDiff I (modelWithCornersSelf 𝕜 V) n g) : ContMDiff I (modelWithCornersSelf 𝕜 V) n fun (p : M) => f p • g p