Documentation

Mathlib.Geometry.Manifold.ContMDiff.NormedSpace

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

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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} (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 : ℕ∞} (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 : ℕ∞} (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 : ℕ∞} (L : E →L[𝕜] F) {s : Set E} :
ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n (⇑L) s
@[deprecated ContinuousLinearMap.contMDiff]
theorem ContinuousLinearMap.smooth {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} (L : E →L[𝕜] F) :
ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n ⇑L

Alias of ContinuousLinearMap.contMDiff.

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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 a version in nontrivial vector bundles, see ContMDiffWithinAt.clm_apply_of_inCoordinates.

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 : ℕ∞} {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 a version in nontrivial vector bundles, see ContMDiffAt.clm_apply_of_inCoordinates.

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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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.

@[deprecated contMDiff_smul]
theorem smooth_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

Alias of contMDiff_smul.


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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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
@[deprecated ContMDiffWithinAt.smul]
theorem SmoothWithinAt.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 : ℕ∞} {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

Alias of ContMDiffWithinAt.smul.

@[deprecated ContMDiffAt.smul]
theorem SmoothAt.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 : ℕ∞} {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

Alias of ContMDiffAt.smul.

@[deprecated ContMDiffOn.smul]
theorem SmoothOn.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 : ℕ∞} {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

Alias of ContMDiffOn.smul.

@[deprecated ContMDiff.smul]
theorem Smooth.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 : ℕ∞} {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

Alias of ContMDiff.smul.