Smooth monoid #
A smooth monoid is a monoid that is also a smooth manifold, in which multiplication is a smooth map
of the product manifold G Γ G into G.
In this file we define the basic structures to talk about smooth monoids: SmoothMul and its
additive counterpart SmoothAdd. These structures are general enough to also talk about smooth
semigroups.
class
SmoothAdd
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
(I : ModelWithCorners π E H)
(G : Type u_4)
[Add G]
[TopologicalSpace G]
[ChartedSpace H G]
extends
SmoothManifoldWithCorners
:
- compatible : β {e e' : LocalHomeomorph G H}, e β atlas H G β e' β atlas H G β LocalHomeomorph.trans (LocalHomeomorph.symm e) e' β contDiffGroupoid β€ I
- smooth_add : Smooth (ModelWithCorners.prod I I) I fun p => p.fst + p.snd
Basic hypothesis to talk about a smooth (Lie) additive monoid or a smooth additive
semigroup. A smooth additive monoid over Ξ±, for example, is obtained by requiring both the
instances AddMonoid Ξ± and SmoothAdd Ξ±.
Instances
class
SmoothMul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
(I : ModelWithCorners π E H)
(G : Type u_4)
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
extends
SmoothManifoldWithCorners
:
- compatible : β {e e' : LocalHomeomorph G H}, e β atlas H G β e' β atlas H G β LocalHomeomorph.trans (LocalHomeomorph.symm e) e' β contDiffGroupoid β€ I
- smooth_mul : Smooth (ModelWithCorners.prod I I) I fun p => p.fst * p.snd
Basic hypothesis to talk about a smooth (Lie) monoid or a smooth semigroup.
A smooth monoid over G, for example, is obtained by requiring both the instances Monoid G
and SmoothMul I G.
Instances
theorem
smooth_add
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
(I : ModelWithCorners π E H)
{G : Type u_4}
[Add G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
:
Smooth (ModelWithCorners.prod I I) I fun p => p.fst + p.snd
theorem
smooth_mul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
(I : ModelWithCorners π E H)
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
:
Smooth (ModelWithCorners.prod I I) I fun p => p.fst * p.snd
theorem
continuousAdd_of_smooth
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
(I : ModelWithCorners π E H)
{G : Type u_4}
[Add G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
:
If the addition is smooth, then it is continuous. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].
theorem
continuousMul_of_smooth
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
(I : ModelWithCorners π E H)
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
:
If the multiplication is smooth, then it is continuous. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].
theorem
ContMDiffWithinAt.add
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Add G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
{s : Set M}
{x : M}
{n : ββ}
(hf : ContMDiffWithinAt I' I n f s x)
(hg : ContMDiffWithinAt I' I n g s x)
:
ContMDiffWithinAt I' I n (f + g) s x
theorem
ContMDiffWithinAt.mul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
{s : Set M}
{x : M}
{n : ββ}
(hf : ContMDiffWithinAt I' I n f s x)
(hg : ContMDiffWithinAt I' I n g s x)
:
ContMDiffWithinAt I' I n (f * g) s x
theorem
ContMDiffAt.add
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Add G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
{x : M}
{n : ββ}
(hf : ContMDiffAt I' I n f x)
(hg : ContMDiffAt I' I n g x)
:
ContMDiffAt I' I n (f + g) x
theorem
ContMDiffAt.mul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
{x : M}
{n : ββ}
(hf : ContMDiffAt I' I n f x)
(hg : ContMDiffAt I' I n g x)
:
ContMDiffAt I' I n (f * g) x
theorem
ContMDiffOn.add
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Add G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
{s : Set M}
{n : ββ}
(hf : ContMDiffOn I' I n f s)
(hg : ContMDiffOn I' I n g s)
:
ContMDiffOn I' I n (f + g) s
theorem
ContMDiffOn.mul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
{s : Set M}
{n : ββ}
(hf : ContMDiffOn I' I n f s)
(hg : ContMDiffOn I' I n g s)
:
ContMDiffOn I' I n (f * g) s
theorem
ContMDiff.add
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Add G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
{n : ββ}
(hf : ContMDiff I' I n f)
(hg : ContMDiff I' I n g)
:
theorem
ContMDiff.mul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
{n : ββ}
(hf : ContMDiff I' I n f)
(hg : ContMDiff I' I n g)
:
theorem
SmoothWithinAt.add
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Add G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
{s : Set M}
{x : M}
(hf : SmoothWithinAt I' I f s x)
(hg : SmoothWithinAt I' I g s x)
:
SmoothWithinAt I' I (f + g) s x
theorem
SmoothWithinAt.mul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
{s : Set M}
{x : M}
(hf : SmoothWithinAt I' I f s x)
(hg : SmoothWithinAt I' I g s x)
:
SmoothWithinAt I' I (f * g) s x
theorem
SmoothAt.add
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Add G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
{x : M}
(hf : SmoothAt I' I f x)
(hg : SmoothAt I' I g x)
:
theorem
SmoothAt.mul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
{x : M}
(hf : SmoothAt I' I f x)
(hg : SmoothAt I' I g x)
:
theorem
SmoothOn.add
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Add G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
{s : Set M}
(hf : SmoothOn I' I f s)
(hg : SmoothOn I' I g s)
:
theorem
SmoothOn.mul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
{s : Set M}
(hf : SmoothOn I' I f s)
(hg : SmoothOn I' I g s)
:
theorem
Smooth.add
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Add G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
(hf : Smooth I' I f)
(hg : Smooth I' I g)
:
theorem
Smooth.mul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{g : M β G}
(hf : Smooth I' I f)
(hg : Smooth I' I g)
:
theorem
smooth_add_left
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Add G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{a : G}
:
theorem
smooth_mul_left
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{a : G}
:
theorem
smooth_add_right
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Add G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{a : G}
:
theorem
smooth_mul_right
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{a : G}
:
def
smoothLeftMul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
(I : ModelWithCorners π E H)
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
(g : G)
:
ContMDiffMap I I G G β€
Left multiplication by g. It is meant to mimic the usual notation in Lie groups.
Lemmas involving smoothLeftMul with the notation π³ usually use L instead of π³ in the
names.
Instances For
def
smoothRightMul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
(I : ModelWithCorners π E H)
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
(g : G)
:
ContMDiffMap I I G G β€
Right multiplication by g. It is meant to mimic the usual notation in Lie groups.
Lemmas involving smoothRightMul with the notation πΉ usually use R instead of πΉ in the
names.
Instances For
@[simp]
theorem
L_apply
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
(I : ModelWithCorners π E H)
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
(g : G)
(h : G)
:
β(smoothLeftMul I g) h = g * h
@[simp]
theorem
R_apply
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
(I : ModelWithCorners π E H)
{G : Type u_4}
[Mul G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
(g : G)
(h : G)
:
β(smoothRightMul I g) h = h * g
@[simp]
theorem
L_mul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
(I : ModelWithCorners π E H)
{G : Type u_8}
[Semigroup G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
(g : G)
(h : G)
:
smoothLeftMul I (g * h) = ContMDiffMap.comp (smoothLeftMul I g) (smoothLeftMul I h)
@[simp]
theorem
R_mul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
(I : ModelWithCorners π E H)
{G : Type u_8}
[Semigroup G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
(g : G)
(h : G)
:
smoothRightMul I (g * h) = ContMDiffMap.comp (smoothRightMul I h) (smoothRightMul I g)
theorem
smoothLeftMul_one
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
(I : ModelWithCorners π E H)
{G' : Type u_8}
[Monoid G']
[TopologicalSpace G']
[ChartedSpace H G']
[SmoothMul I G']
(g' : G')
:
β(smoothLeftMul I g') 1 = g'
theorem
smoothRightMul_one
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
(I : ModelWithCorners π E H)
{G' : Type u_8}
[Monoid G']
[TopologicalSpace G']
[ChartedSpace H G']
[SmoothMul I G']
(g' : G')
:
β(smoothRightMul I g') 1 = g'
theorem
SmoothAdd.sum.proof_1
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners π E H)
(G : Type u_4)
[TopologicalSpace G]
[ChartedSpace H G]
[Add G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
(I' : ModelWithCorners π E' H')
(G' : Type u_7)
[TopologicalSpace G']
[ChartedSpace H' G']
[Add G']
[SmoothAdd I' G']
:
SmoothAdd (ModelWithCorners.prod I I') (G Γ G')
instance
SmoothAdd.sum
{π : Type u_8}
[NontriviallyNormedField π]
{E : Type u_9}
[NormedAddCommGroup E]
[NormedSpace π E]
{H : Type u_10}
[TopologicalSpace H]
(I : ModelWithCorners π E H)
(G : Type u_11)
[TopologicalSpace G]
[ChartedSpace H G]
[Add G]
[SmoothAdd I G]
{E' : Type u_12}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_13}
[TopologicalSpace H']
(I' : ModelWithCorners π E' H')
(G' : Type u_14)
[TopologicalSpace G']
[ChartedSpace H' G']
[Add G']
[SmoothAdd I' G']
:
SmoothAdd (ModelWithCorners.prod I I') (G Γ G')
instance
SmoothMul.prod
{π : Type u_8}
[NontriviallyNormedField π]
{E : Type u_9}
[NormedAddCommGroup E]
[NormedSpace π E]
{H : Type u_10}
[TopologicalSpace H]
(I : ModelWithCorners π E H)
(G : Type u_11)
[TopologicalSpace G]
[ChartedSpace H G]
[Mul G]
[SmoothMul I G]
{E' : Type u_12}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_13}
[TopologicalSpace H']
(I' : ModelWithCorners π E' H')
(G' : Type u_14)
[TopologicalSpace G']
[ChartedSpace H' G']
[Mul G']
[SmoothMul I' G']
:
SmoothMul (ModelWithCorners.prod I I') (G Γ G')
theorem
smooth_nsmul
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
(n : β)
:
theorem
smooth_pow
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
(n : β)
:
structure
SmoothAddMonoidMorphism
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
(I : ModelWithCorners π E H)
(I' : ModelWithCorners π E' H')
(G : Type u_8)
[TopologicalSpace G]
[ChartedSpace H G]
[AddMonoid G]
[SmoothAdd I G]
(G' : Type u_9)
[TopologicalSpace G']
[ChartedSpace H' G']
[AddMonoid G']
[SmoothAdd I' G']
extends
AddMonoidHom
:
Type (max u_8 u_9)
- toFun : G β G'
- map_zero' : ZeroHom.toFun (βs.toAddMonoidHom) 0 = 0
- map_add' : β (x y : G), ZeroHom.toFun (βs.toAddMonoidHom) (x + y) = ZeroHom.toFun (βs.toAddMonoidHom) x + ZeroHom.toFun (βs.toAddMonoidHom) y
- smooth_toFun : Smooth I I' s.toFun
Morphism of additive smooth monoids.
Instances For
structure
SmoothMonoidMorphism
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
(I : ModelWithCorners π E H)
(I' : ModelWithCorners π E' H')
(G : Type u_8)
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
[SmoothMul I G]
(G' : Type u_9)
[TopologicalSpace G']
[ChartedSpace H' G']
[Monoid G']
[SmoothMul I' G']
extends
MonoidHom
:
Type (max u_8 u_9)
- toFun : G β G'
- map_one' : OneHom.toFun (βs.toMonoidHom) 1 = 1
- map_mul' : β (x y : G), OneHom.toFun (βs.toMonoidHom) (x * y) = OneHom.toFun (βs.toMonoidHom) x * OneHom.toFun (βs.toMonoidHom) y
- smooth_toFun : Smooth I I' s.toFun
Morphism of smooth monoids.
Instances For
instance
instZeroSmoothAddMonoidMorphism
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{I' : ModelWithCorners π E' H'}
{G' : Type u_7}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothAdd I' G']
:
Zero (SmoothAddMonoidMorphism I I' G G')
theorem
instZeroSmoothAddMonoidMorphism.proof_1
{π : Type u_7}
[NontriviallyNormedField π]
{H : Type u_5}
[TopologicalSpace H]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
{H' : Type u_2}
[TopologicalSpace H']
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{I' : ModelWithCorners π E' H'}
{G' : Type u_1}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
:
Smooth I I' fun x => AddZeroClass.toZero.1
instance
instOneSmoothMonoidMorphism
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{I' : ModelWithCorners π E' H'}
{G' : Type u_7}
[Monoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothMul I' G']
:
One (SmoothMonoidMorphism I I' G G')
instance
instInhabitedSmoothAddMonoidMorphism
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{I' : ModelWithCorners π E' H'}
{G' : Type u_7}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothAdd I' G']
:
Inhabited (SmoothAddMonoidMorphism I I' G G')
instance
instInhabitedSmoothMonoidMorphism
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{I' : ModelWithCorners π E' H'}
{G' : Type u_7}
[Monoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothMul I' G']
:
Inhabited (SmoothMonoidMorphism I I' G G')
instance
instAddMonoidHomClassSmoothAddMonoidMorphismToAddZeroClassToAddZeroClass
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{I' : ModelWithCorners π E' H'}
{G' : Type u_7}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothAdd I' G']
:
AddMonoidHomClass (SmoothAddMonoidMorphism I I' G G') G G'
theorem
instAddMonoidHomClassSmoothAddMonoidMorphismToAddZeroClassToAddZeroClass.proof_1
{π : Type u_7}
[NontriviallyNormedField π]
{H : Type u_6}
[TopologicalSpace H]
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_2}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{I' : ModelWithCorners π E' H'}
{G' : Type u_1}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothAdd I' G']
(f : SmoothAddMonoidMorphism I I' G G')
(g : SmoothAddMonoidMorphism I I' G G')
(h : (fun a => a.toFun) f = (fun a => a.toFun) g)
:
f = g
theorem
instAddMonoidHomClassSmoothAddMonoidMorphismToAddZeroClassToAddZeroClass.proof_2
{π : Type u_7}
[NontriviallyNormedField π]
{H : Type u_6}
[TopologicalSpace H]
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_2}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{I' : ModelWithCorners π E' H'}
{G' : Type u_1}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothAdd I' G']
(f : SmoothAddMonoidMorphism I I' G G')
(a : G)
(b : G)
:
theorem
instAddMonoidHomClassSmoothAddMonoidMorphismToAddZeroClassToAddZeroClass.proof_3
{π : Type u_7}
[NontriviallyNormedField π]
{H : Type u_6}
[TopologicalSpace H]
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_2}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{I' : ModelWithCorners π E' H'}
{G' : Type u_1}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothAdd I' G']
(f : SmoothAddMonoidMorphism I I' G G')
:
βf.toAddMonoidHom 0 = 0
instance
instMonoidHomClassSmoothMonoidMorphismToMulOneClassToMulOneClass
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{I' : ModelWithCorners π E' H'}
{G' : Type u_7}
[Monoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothMul I' G']
:
MonoidHomClass (SmoothMonoidMorphism I I' G G') G G'
theorem
instContinuousMapClassSmoothAddMonoidMorphism.proof_1
{π : Type u_7}
[NontriviallyNormedField π]
{H : Type u_6}
[TopologicalSpace H]
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_2}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{H' : Type u_4}
[TopologicalSpace H']
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{I' : ModelWithCorners π E' H'}
{G' : Type u_1}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothAdd I' G']
(f : SmoothAddMonoidMorphism I I' G G')
:
Continuous f.toFun
instance
instContinuousMapClassSmoothAddMonoidMorphism
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[AddMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{I' : ModelWithCorners π E' H'}
{G' : Type u_7}
[AddMonoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothAdd I' G']
:
ContinuousMapClass (SmoothAddMonoidMorphism I I' G G') G G'
instance
instContinuousMapClassSmoothMonoidMorphism
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{I' : ModelWithCorners π E' H'}
{G' : Type u_7}
[Monoid G']
[TopologicalSpace G']
[ChartedSpace H' G']
[SmoothMul I' G']
:
ContinuousMapClass (SmoothMonoidMorphism I I' G G') G G'
theorem
contMDiffWithinAt_finset_sum'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiffWithinAt I' I n (f i) s x)
:
ContMDiffWithinAt I' I n (Finset.sum t fun i => f i) s x
theorem
contMDiffWithinAt_finset_prod'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiffWithinAt I' I n (f i) s x)
:
ContMDiffWithinAt I' I n (Finset.prod t fun i => f i) s x
theorem
contMDiffAt_finset_sum'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiffAt I' I n (f i) x)
:
ContMDiffAt I' I n (Finset.sum t fun i => f i) x
theorem
contMDiffAt_finset_prod'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiffAt I' I n (f i) x)
:
ContMDiffAt I' I n (Finset.prod t fun i => f i) x
theorem
contMDiffOn_finset_sum'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiffOn I' I n (f i) s)
:
ContMDiffOn I' I n (Finset.sum t fun i => f i) s
theorem
contMDiffOn_finset_prod'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiffOn I' I n (f i) s)
:
ContMDiffOn I' I n (Finset.prod t fun i => f i) s
theorem
contMDiff_finset_sum'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiff I' I n (f i))
:
ContMDiff I' I n (Finset.sum t fun i => f i)
theorem
contMDiff_finset_prod'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiff I' I n (f i))
:
ContMDiff I' I n (Finset.prod t fun i => f i)
theorem
contMDiffWithinAt_finset_sum
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiffWithinAt I' I n (f i) s x)
:
ContMDiffWithinAt I' I n (fun x => Finset.sum t fun i => f i x) s x
theorem
contMDiffWithinAt_finset_prod
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiffWithinAt I' I n (f i) s x)
:
ContMDiffWithinAt I' I n (fun x => Finset.prod t fun i => f i x) s x
theorem
contMDiffAt_finset_sum
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiffAt I' I n (f i) x)
:
ContMDiffAt I' I n (fun x => Finset.sum t fun i => f i x) x
theorem
contMDiffAt_finset_prod
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiffAt I' I n (f i) x)
:
ContMDiffAt I' I n (fun x => Finset.prod t fun i => f i x) x
theorem
contMDiffOn_finset_sum
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiffOn I' I n (f i) s)
:
ContMDiffOn I' I n (fun x => Finset.sum t fun i => f i x) s
theorem
contMDiffOn_finset_prod
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiffOn I' I n (f i) s)
:
ContMDiffOn I' I n (fun x => Finset.prod t fun i => f i x) s
theorem
contMDiff_finset_sum
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiff I' I n (f i))
:
ContMDiff I' I n fun x => Finset.sum t fun i => f i x
theorem
contMDiff_finset_prod
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), i β t β ContMDiff I' I n (f i))
:
ContMDiff I' I n fun x => Finset.prod t fun i => f i x
theorem
smoothWithinAt_finset_sum'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β SmoothWithinAt I' I (f i) s x)
:
SmoothWithinAt I' I (Finset.sum t fun i => f i) s x
theorem
smoothWithinAt_finset_prod'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β SmoothWithinAt I' I (f i) s x)
:
SmoothWithinAt I' I (Finset.prod t fun i => f i) s x
theorem
smoothAt_finset_sum'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β SmoothAt I' I (f i) x)
:
SmoothAt I' I (Finset.sum t fun i => f i) x
theorem
smoothAt_finset_prod'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β SmoothAt I' I (f i) x)
:
SmoothAt I' I (Finset.prod t fun i => f i) x
theorem
smoothOn_finset_sum'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β SmoothOn I' I (f i) s)
:
SmoothOn I' I (Finset.sum t fun i => f i) s
theorem
smoothOn_finset_prod'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β SmoothOn I' I (f i) s)
:
SmoothOn I' I (Finset.prod t fun i => f i) s
theorem
smooth_finset_sum'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β Smooth I' I (f i))
:
Smooth I' I (Finset.sum t fun i => f i)
theorem
smooth_finset_prod'
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β Smooth I' I (f i))
:
Smooth I' I (Finset.prod t fun i => f i)
theorem
smoothWithinAt_finset_sum
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β SmoothWithinAt I' I (f i) s x)
:
SmoothWithinAt I' I (fun x => Finset.sum t fun i => f i x) s x
theorem
smoothWithinAt_finset_prod
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β SmoothWithinAt I' I (f i) s x)
:
SmoothWithinAt I' I (fun x => Finset.prod t fun i => f i x) s x
theorem
smoothAt_finset_sum
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β SmoothAt I' I (f i) x)
:
SmoothAt I' I (fun x => Finset.sum t fun i => f i x) x
theorem
smoothAt_finset_prod
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{x : M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β SmoothAt I' I (f i) x)
:
SmoothAt I' I (fun x => Finset.prod t fun i => f i x) x
theorem
smoothOn_finset_sum
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β SmoothOn I' I (f i) s)
:
SmoothOn I' I (fun x => Finset.sum t fun i => f i x) s
theorem
smoothOn_finset_prod
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{s : Set M}
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β SmoothOn I' I (f i) s)
:
SmoothOn I' I (fun x => Finset.prod t fun i => f i x) s
theorem
smooth_finset_sum
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β Smooth I' I (f i))
:
Smooth I' I fun x => Finset.sum t fun i => f i x
theorem
smooth_finset_prod
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{t : Finset ΞΉ}
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), i β t β Smooth I' I (f i))
:
Smooth I' I fun x => Finset.prod t fun i => f i x
theorem
contMDiff_finsum
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), ContMDiff I' I n (f i))
(hfin : LocallyFinite fun i => Function.support (f i))
:
ContMDiff I' I n fun x => βαΆ (i : ΞΉ), f i x
theorem
contMDiff_finprod
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : ΞΉ β M β G}
{n : ββ}
(h : β (i : ΞΉ), ContMDiff I' I n (f i))
(hfin : LocallyFinite fun i => Function.mulSupport (f i))
:
ContMDiff I' I n fun x => βαΆ (i : ΞΉ), f i x
theorem
contMDiff_finsum_cond
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : ΞΉ β M β G}
{n : ββ}
{p : ΞΉ β Prop}
(hc : β (i : ΞΉ), p i β ContMDiff I' I n (f i))
(hf : LocallyFinite fun i => Function.support (f i))
:
ContMDiff I' I n fun x => βαΆ (i : ΞΉ) (x_1 : p i), f i x
theorem
contMDiff_finprod_cond
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : ΞΉ β M β G}
{n : ββ}
{p : ΞΉ β Prop}
(hc : β (i : ΞΉ), p i β ContMDiff I' I n (f i))
(hf : LocallyFinite fun i => Function.mulSupport (f i))
:
ContMDiff I' I n fun x => βαΆ (i : ΞΉ) (x_1 : p i), f i x
theorem
smooth_finsum
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), Smooth I' I (f i))
(hfin : LocallyFinite fun i => Function.support (f i))
:
Smooth I' I fun x => βαΆ (i : ΞΉ), f i x
theorem
smooth_finprod
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : ΞΉ β M β G}
(h : β (i : ΞΉ), Smooth I' I (f i))
(hfin : LocallyFinite fun i => Function.mulSupport (f i))
:
Smooth I' I fun x => βαΆ (i : ΞΉ), f i x
theorem
smooth_finsum_cond
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[AddCommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : ΞΉ β M β G}
{p : ΞΉ β Prop}
(hc : β (i : ΞΉ), p i β Smooth I' I (f i))
(hf : LocallyFinite fun i => Function.support (f i))
:
Smooth I' I fun x => βαΆ (i : ΞΉ) (x_1 : p i), f i x
theorem
smooth_finprod_cond
{ΞΉ : Type u_1}
{π : Type u_2}
[NontriviallyNormedField π]
{H : Type u_3}
[TopologicalSpace H]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_5}
[CommMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_7}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : ΞΉ β M β G}
{p : ΞΉ β Prop}
(hc : β (i : ΞΉ), p i β Smooth I' I (f i))
(hf : LocallyFinite fun i => Function.mulSupport (f i))
:
Smooth I' I fun x => βαΆ (i : ΞΉ) (x_1 : p i), f i x
instance
hasSmoothAddSelf
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
:
SmoothAdd (modelWithCornersSelf π E) E
theorem
ContMDiffWithinAt.sub_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[SubNegMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{s : Set M}
{x : M}
{n : ββ}
(c : G)
(hf : ContMDiffWithinAt I' I n f s x)
:
ContMDiffWithinAt I' I n (fun x => f x - c) s x
theorem
ContMDiffWithinAt.div_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[DivInvMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{s : Set M}
{x : M}
{n : ββ}
(c : G)
(hf : ContMDiffWithinAt I' I n f s x)
:
ContMDiffWithinAt I' I n (fun x => f x / c) s x
theorem
ContMDiffAt.sub_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[SubNegMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{x : M}
{n : ββ}
(c : G)
(hf : ContMDiffAt I' I n f x)
:
ContMDiffAt I' I n (fun x => f x - c) x
theorem
ContMDiffAt.div_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[DivInvMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{x : M}
{n : ββ}
(c : G)
(hf : ContMDiffAt I' I n f x)
:
ContMDiffAt I' I n (fun x => f x / c) x
theorem
ContMDiffOn.sub_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[SubNegMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{s : Set M}
{n : ββ}
(c : G)
(hf : ContMDiffOn I' I n f s)
:
ContMDiffOn I' I n (fun x => f x - c) s
theorem
ContMDiffOn.div_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[DivInvMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{s : Set M}
{n : ββ}
(c : G)
(hf : ContMDiffOn I' I n f s)
:
ContMDiffOn I' I n (fun x => f x / c) s
theorem
ContMDiff.sub_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[SubNegMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{n : ββ}
(c : G)
(hf : ContMDiff I' I n f)
:
theorem
ContMDiff.div_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[DivInvMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{n : ββ}
(c : G)
(hf : ContMDiff I' I n f)
:
theorem
SmoothWithinAt.sub_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[SubNegMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{s : Set M}
{x : M}
(c : G)
(hf : SmoothWithinAt I' I f s x)
:
SmoothWithinAt I' I (fun x => f x - c) s x
theorem
SmoothWithinAt.div_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[DivInvMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{s : Set M}
{x : M}
(c : G)
(hf : SmoothWithinAt I' I f s x)
:
SmoothWithinAt I' I (fun x => f x / c) s x
theorem
SmoothAt.sub_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[SubNegMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{x : M}
(c : G)
(hf : SmoothAt I' I f x)
:
theorem
SmoothAt.div_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[DivInvMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{x : M}
(c : G)
(hf : SmoothAt I' I f x)
:
theorem
SmoothOn.sub_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[SubNegMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{s : Set M}
(c : G)
(hf : SmoothOn I' I f s)
:
theorem
SmoothOn.div_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[DivInvMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
{s : Set M}
(c : G)
(hf : SmoothOn I' I f s)
:
theorem
Smooth.sub_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[SubNegMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothAdd I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
(c : G)
(hf : Smooth I' I f)
:
theorem
Smooth.div_const
{π : Type u_1}
[NontriviallyNormedField π]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace π E]
{I : ModelWithCorners π E H}
{G : Type u_4}
[DivInvMonoid G]
[TopologicalSpace G]
[ChartedSpace H G]
[SmoothMul I G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners π E' H'}
{M : Type u_7}
[TopologicalSpace M]
[ChartedSpace H' M]
{f : M β G}
(c : G)
(hf : Smooth I' I f)
: