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