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_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_11} [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_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_11} [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_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_11} [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_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_11} [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_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_11} [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_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_11} [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_8} [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_8} [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_8} [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_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} (L : E →L[𝕜] F) {s : Set E} :
ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n (⇑L) s
theorem ContinuousLinearMap.smooth {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (L : E →L[𝕜] F) :
Smooth (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) ⇑L
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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [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
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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [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
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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [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_14} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_15} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_16} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type u_17} [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 smooth_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_18} [NormedAddCommGroup V] [NormedSpace 𝕜 V] :
Smooth ((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 : ℕ∞} {V : Type u_18} [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_18} [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_18} [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_18} [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
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} {V : Type u_18} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : SmoothWithinAt I (modelWithCornersSelf 𝕜 𝕜) f s x) (hg : SmoothWithinAt I (modelWithCornersSelf 𝕜 V) g s x) :
SmoothWithinAt I (modelWithCornersSelf 𝕜 V) (fun (p : M) => f p • g p) s x
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} {V : Type u_18} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : SmoothAt I (modelWithCornersSelf 𝕜 𝕜) f x) (hg : SmoothAt I (modelWithCornersSelf 𝕜 V) g x) :
SmoothAt I (modelWithCornersSelf 𝕜 V) (fun (p : M) => f p • g p) x
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} {V : Type u_18} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : SmoothOn I (modelWithCornersSelf 𝕜 𝕜) f s) (hg : SmoothOn I (modelWithCornersSelf 𝕜 V) g s) :
SmoothOn I (modelWithCornersSelf 𝕜 V) (fun (p : M) => f p • g p) s
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] {V : Type u_18} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : Smooth I (modelWithCornersSelf 𝕜 𝕜) f) (hg : Smooth I (modelWithCornersSelf 𝕜 V) g) :
Smooth I (modelWithCornersSelf 𝕜 V) fun (p : M) => f p • g p