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