Mathlib.Geometry.Manifold.ContMDiff.NormedSpace

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 : ℕ∞} {f : E → E'} {s : Set E} {x : E} :

ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s x ↔ ContDiffWithinAt 𝕜 (↑n) f s x

source

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.

source

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.

source

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

source

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.

source

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.

source

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

source

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.

source

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.

source

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

source

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.

source

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.

source

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

source

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

source

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

source

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

source

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

source

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 #

source

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

source

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

source

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

source

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

source

@[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.

source

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

source

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

source

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

source

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)

source

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

source

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

source

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

source

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)

source

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

source

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

source

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

source

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)

source

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.

source

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.

source

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

source

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)

source

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

source

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

source

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

source

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))

source

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

source

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

source

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

source

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 #

source

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.

source

@[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.

source

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

source

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

source

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

source

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

source

@[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.

source

@[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.

source

@[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.

source

@[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.