C^n monoid

A C^n monoid is a monoid that is also a C^n manifold, in which multiplication is a C^n map of the product manifold G × G into G.

In this file we define the basic structures to talk about C^n monoids: ContMDiffMul and its additive counterpart ContMDiffAdd. These structures are general enough to also talk about C^n semigroups.

def LibraryNote.Design_choices_about_smooth_algebraic_structures : Batteries.Util.LibraryNote

1. All C^n algebraic structures on G are Prop-valued classes that extend IsManifold I n G. This way we save users from adding both [IsManifold I n G] and [ContMDiffMul I n G] to the assumptions. While many API lemmas hold true without the IsManifold I n G assumption, we're not aware of a mathematically interesting monoid on a topological manifold such that (a) the space is not a IsManifold; (b) the multiplication is C^n at (a, b) in the charts extChartAt I a, extChartAt I b, extChartAt I (a * b).

2. Because of ModelProd we can't assume, e.g., that a LieGroup is modelled on 𝓘(𝕜, E). So, we formulate the definitions and lemmas for any model.

3. While smoothness of an operation implies its continuity, lemmas like continuousMul_of_contMDiffMul can't be instances because otherwise Lean would have to search for ContMDiffMul I n G with unknown 𝕜, E, H, and I : ModelWithCorners 𝕜 E H. If users need [ContinuousMul G] in a proof about a C^n monoid, then they need to either add [ContinuousMul G] as an assumption (worse) or use haveI in the proof (better).

class ContMDiffAdd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (G : Type u_4) [Add G] [TopologicalSpace G] [ChartedSpace H G] extends IsManifold I n G : Prop

Basic hypothesis to talk about a C^n (Lie) additive monoid or a C^n additive semigroup. A C^n additive monoid over G, for example, is obtained by requiring both the instances AddMonoid G and ContMDiffAdd I n G.

• compatible {e e' : OpenPartialHomeomorph G H} : e ∈ atlas H G → e' ∈ atlas H G → e.symm.trans e' ∈ contDiffGroupoid n I
• contMDiff_add : ContMDiff (I.prod I) I n fun (p : G × G) => p.1 + p.2

class ContMDiffMul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (G : Type u_4) [Mul G] [TopologicalSpace G] [ChartedSpace H G] extends IsManifold I n G : Prop

Basic hypothesis to talk about a C^n (Lie) monoid or a C^n semigroup. A C^n monoid over G, for example, is obtained by requiring both the instances Monoid G and ContMDiffMul I n G.

• compatible {e e' : OpenPartialHomeomorph G H} : e ∈ atlas H G → e' ∈ atlas H G → e.symm.trans e' ∈ contDiffGroupoid n I
• contMDiff_mul : ContMDiff (I.prod I) I n fun (p : G × G) => p.1 * p.2

theorem ContMDiffMul.of_le {𝕜 : 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] {m n : WithTop ℕ∞} (hmn : m ≤ n) [h : ContMDiffMul I n G] : ContMDiffMul I m G

theorem ContMDiffAdd.of_le {𝕜 : 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] {m n : WithTop ℕ∞} (hmn : m ≤ n) [h : ContMDiffAdd I n G] : ContMDiffAdd I m G

instance instContMDiffMulOfSomeENatTopOfLEInfty {𝕜 : 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] {a : WithTop ℕ∞} [ContMDiffMul I (↑⊤) G] [h : ENat.LEInfty a] : ContMDiffMul I a G

instance instContMDiffAddOfSomeENatTopOfLEInfty {𝕜 : 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] {a : WithTop ℕ∞} [ContMDiffAdd I (↑⊤) G] [h : ENat.LEInfty a] : ContMDiffAdd I a G

instance instContMDiffMulOfTopWithTopENat {𝕜 : 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] {a : WithTop ℕ∞} [ContMDiffMul I ⊤ G] : ContMDiffMul I a G

instance instContMDiffAddOfTopWithTopENat {𝕜 : 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] {a : WithTop ℕ∞} [ContMDiffAdd I ⊤ G] : ContMDiffAdd I a G

instance instContMDiffMulOfNatWithTopENatOfContinuousMul {𝕜 : 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] [ContinuousMul G] : ContMDiffMul I 0 G

instance instContMDiffAddOfNatWithTopENatOfContinuousAdd {𝕜 : 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] [ContinuousAdd G] : ContMDiffAdd I 0 G

instance instContMDiffMulOfNatWithTopENat {𝕜 : 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] [ContMDiffMul I 2 G] : ContMDiffMul I 1 G

instance instContMDiffAddOfNatWithTopENat {𝕜 : 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] [ContMDiffAdd I 2 G] : ContMDiffAdd I 1 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) (n : WithTop ℕ∞) {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] : ContMDiff (I.prod I) I n fun (p : G × G) => p.1 * p.2

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) (n : WithTop ℕ∞) {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] : ContMDiff (I.prod I) I n fun (p : G × G) => p.1 + p.2

theorem continuousMul_of_contMDiffMul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] : ContinuousMul G

If the multiplication is C^n, then it is continuous. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

theorem continuousAdd_of_contMDiffAdd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] : ContinuousAdd G

If the addition is C^n, then it is continuous. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

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} {n : WithTop ℕ∞} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffMul I n G] {f g : M → G} {s : Set M} {x : M} (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.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffAdd I n G] {f g : M → G} {s : Set M} {x : M} (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.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffMul I n G] {f g : M → G} {x : M} (hf : ContMDiffAt I' I n f x) (hg : ContMDiffAt I' I n g x) : ContMDiffAt I' I n (f * g) 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} {n : WithTop ℕ∞} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffAdd I n G] {f g : M → G} {x : M} (hf : ContMDiffAt I' I n f x) (hg : ContMDiffAt I' I n g x) : ContMDiffAt I' I n (f + g) x

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} {n : WithTop ℕ∞} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffMul I n G] {f g : M → G} {s : Set M} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) : ContMDiffOn I' I n (f * g) s

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} {n : WithTop ℕ∞} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffAdd I n G] {f g : M → G} {s : Set M} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) : ContMDiffOn I' I n (f + g) s

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} {n : WithTop ℕ∞} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffMul I n G] {f g : M → G} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) : ContMDiff I' I n (f * g)

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} {n : WithTop ℕ∞} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffAdd I n G] {f g : M → G} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) : ContMDiff I' I n (f + g)

theorem contMDiff_mul_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] {a : G} : ContMDiff I I n fun (x : G) => a * x

theorem contMDiff_add_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] {a : G} : ContMDiff I I n fun (x : G) => a + x

theorem contMDiffAt_mul_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] {a b : G} : ContMDiffAt I I n (fun (x : G) => a * x) b

theorem contMDiffAt_add_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] {a b : G} : ContMDiffAt I I n (fun (x : G) => a + x) b

theorem contMDiff_mul_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] {a : G} : ContMDiff I I n fun (x : G) => x * a

theorem contMDiff_add_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] {a : G} : ContMDiff I I n fun (x : G) => x + a

theorem contMDiffAt_mul_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] {a b : G} : ContMDiffAt I I n (fun (x : G) => x * a) b

theorem contMDiffAt_add_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] {a b : G} : ContMDiffAt I I n (fun (x : G) => x + a) b

theorem mdifferentiable_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] [ContMDiffMul I 1 G] {a : G} : MDiff fun (x : G) => a * x

theorem mdifferentiable_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] [ContMDiffAdd I 1 G] {a : G} : MDiff fun (x : G) => a + x

theorem mdifferentiableAt_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] [ContMDiffMul I 1 G] {a b : G} : (MDiffAt fun (x : G) => a * x) b

theorem mdifferentiableAt_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] [ContMDiffAdd I 1 G] {a b : G} : (MDiffAt fun (x : G) => a + x) b

theorem mdifferentiable_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] [ContMDiffMul I 1 G] {a : G} : MDiff fun (x : G) => x * a

theorem mdifferentiable_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] [ContMDiffAdd I 1 G] {a : G} : MDiff fun (x : G) => x + a

theorem mdifferentiableAt_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] [ContMDiffMul I 1 G] {a b : G} : (MDiffAt fun (x : G) => x * a) b

theorem mdifferentiableAt_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] [ContMDiffAdd I 1 G] {a b : G} : (MDiffAt fun (x : G) => x + a) b

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] (g : G) [ContMDiffMul I (↑⊤) G] : ContMDiffMap I I G G ↑⊤

Left multiplication by g. It is meant to mimic the usual notation in Lie groups. Used mostly through the notation 𝑳. Lemmas involving smoothLeftMul with the notation 𝑳 usually use L instead of 𝑳 in the names.

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] (g : G) [ContMDiffMul I (↑⊤) G] : ContMDiffMap I I G G ↑⊤

Right multiplication by g. It is meant to mimic the usual notation in Lie groups. Used mostly through the notation 𝑹. Lemmas involving smoothRightMul with the notation 𝑹 usually use R instead of 𝑹 in the names.

def LieGroup.«term𝑳» : Lean.ParserDescr

Left multiplication by g. It is meant to mimic the usual notation in Lie groups. Used mostly through the notation 𝑳. Lemmas involving smoothLeftMul with the notation 𝑳 usually use L instead of 𝑳 in the names.

def LieGroup.«term𝑹» : Lean.ParserDescr

Right multiplication by g. It is meant to mimic the usual notation in Lie groups. Used mostly through the notation 𝑹. Lemmas involving smoothRightMul with the notation 𝑹 usually use R instead of 𝑹 in the names.

@[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] (g h : G) [ContMDiffMul I (↑⊤) 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] (g h : G) [ContMDiffMul I (↑⊤) 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] [ContMDiffMul I (↑⊤) G] (g h : G) : smoothLeftMul I (g * h) = (smoothLeftMul I g).comp (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] [ContMDiffMul I (↑⊤) G] (g h : G) : smoothRightMul I (g * h) = (smoothRightMul I h).comp (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'] [ContMDiffMul 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'] [ContMDiffMul I (↑⊤) G'] (g' : G') : (smoothRightMul I g') 1 = g'

instance ContMDiffMul.prod {n : WithTop ℕ∞} {𝕜 : 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] [ContMDiffMul I n 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'] [ContMDiffMul I' n G'] : ContMDiffMul (I.prod I') n (G × G')

instance ContMDiffAdd.prod {n : WithTop ℕ∞} {𝕜 : 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] [ContMDiffAdd I n 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'] [ContMDiffAdd I' n G'] : ContMDiffAdd (I.prod I') n (G × G')

theorem contMDiff_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n G] (i : ℕ) : ContMDiff I I n fun (a : G) => a ^ i

theorem contMDiff_nsmul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n G] (i : ℕ) : ContMDiff I I n fun (a : G) => i • a

structure ContMDiffAddMonoidMorphism {𝕜 : 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') (n : WithTop ℕ∞) (G : Type u_8) [TopologicalSpace G] [ChartedSpace H G] [AddMonoid G] (G' : Type u_9) [TopologicalSpace G'] [ChartedSpace H' G'] [AddMonoid G'] extends G →+ G' : Type (max u_8 u_9)

Morphism of additive C^n monoids.

• toFun : G → G'
• map_zero' : (↑self.toAddMonoidHom).toFun 0 = 0
• map_add' (x y : G) : (↑self.toAddMonoidHom).toFun (x + y) = (↑self.toAddMonoidHom).toFun x + (↑self.toAddMonoidHom).toFun y
• contMDiff_toFun : ContMDiff I I' n (↑self.toAddMonoidHom).toFun

structure ContMDiffMonoidMorphism {𝕜 : 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') (n : WithTop ℕ∞) (G : Type u_8) [TopologicalSpace G] [ChartedSpace H G] [Monoid G] (G' : Type u_9) [TopologicalSpace G'] [ChartedSpace H' G'] [Monoid G'] extends G →* G' : Type (max u_8 u_9)

Morphism of C^n monoids.

• toFun : G → G'
• map_one' : (↑self.toMonoidHom).toFun 1 = 1
• map_mul' (x y : G) : (↑self.toMonoidHom).toFun (x * y) = (↑self.toMonoidHom).toFun x * (↑self.toMonoidHom).toFun y
• contMDiff_toFun : ContMDiff I I' n (↑self.toMonoidHom).toFun

@[implicit_reducible]

instance instOneContMDiffMonoidMorphism {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] {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'] : One (ContMDiffMonoidMorphism I I' n G G')

@[implicit_reducible]

instance instZeroContMDiffAddMonoidMorphism {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] {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'] : Zero (ContMDiffAddMonoidMorphism I I' n G G')

@[implicit_reducible]

instance instInhabitedContMDiffMonoidMorphism {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] {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'] : Inhabited (ContMDiffMonoidMorphism I I' n G G')

@[implicit_reducible]

instance instInhabitedContMDiffAddMonoidMorphism {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] {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'] : Inhabited (ContMDiffAddMonoidMorphism I I' n G G')

@[implicit_reducible]

instance instFunLikeContMDiffMonoidMorphism {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] {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'] : FunLike (ContMDiffMonoidMorphism I I' n G G') G G'

@[implicit_reducible]

instance instFunLikeContMDiffAddMonoidMorphism {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] {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'] : FunLike (ContMDiffAddMonoidMorphism I I' n G G') G G'

instance instMonoidHomClassContMDiffMonoidMorphism {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] {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'] : MonoidHomClass (ContMDiffMonoidMorphism I I' n G G') G G'

instance instAddMonoidHomClassContMDiffAddMonoidMorphism {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] {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'] : AddMonoidHomClass (ContMDiffAddMonoidMorphism I I' n G G') G G'

instance instContinuousMapClassContMDiffMonoidMorphism {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] {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'] : ContinuousMapClass (ContMDiffMonoidMorphism I I' n G G') G G'

instance instContinuousMapClassContMDiffAddMonoidMorphism {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] {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'] : ContinuousMapClass (ContMDiffAddMonoidMorphism I I' n G G') G G'

Differentiability of finite point-wise sums and products, and powers

Finite point-wise products (resp. sums), and powers, of C^n functions M → G (at x/on s) into a commutative monoid G are C^n at x/on s.

theorem ContMDiffWithinAt.prod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 ∈ t, ContMDiffWithinAt I' I n (f i) s x₀) : ContMDiffWithinAt I' I n (fun (x : M) => ∏ i ∈ t, f i x) s x₀

theorem ContMDiffWithinAt.sum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 ∈ t, ContMDiffWithinAt I' I n (f i) s x₀) : ContMDiffWithinAt I' I n (fun (x : M) => ∑ i ∈ t, f i x) s x₀

theorem contMDiffWithinAt_finprod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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} {f : ι → M → G} (lf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) {x₀ : M} (h : ∀ (i : ι), ContMDiffWithinAt I' I n (f i) s x₀) : ContMDiffWithinAt I' I n (fun (x : M) => ∏ᶠ (i : ι), f i x) s x₀

theorem contMDiffWithinAt_finsum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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} {f : ι → M → G} (lf : LocallyFinite fun (i : ι) => Function.support (f i)) {x₀ : M} (h : ∀ (i : ι), ContMDiffWithinAt I' I n (f i) s x₀) : ContMDiffWithinAt I' I n (fun (x : M) => ∑ᶠ (i : ι), f i x) s x₀

theorem contMDiffWithinAt_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 ∈ t, ContMDiffWithinAt I' I n (f i) s x) : ContMDiffWithinAt I' I n (∏ i ∈ t, f i) s x

theorem contMDiffWithinAt_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 ∈ t, ContMDiffWithinAt I' I n (f i) s x) : ContMDiffWithinAt I' I n (∑ i ∈ t, f i) s x

theorem contMDiffWithinAt_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 ∈ t, ContMDiffWithinAt I' I n (f i) s x) : ContMDiffWithinAt I' I n (fun (x : M) => ∏ i ∈ t, f i x) s x

theorem contMDiffWithinAt_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 ∈ t, ContMDiffWithinAt I' I n (f i) s x) : ContMDiffWithinAt I' I n (fun (x : M) => ∑ i ∈ t, f i x) s x

theorem ContMDiffAt.prod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 ∈ t, ContMDiffAt I' I n (f i) x₀) : ContMDiffAt I' I n (fun (x : M) => ∏ i ∈ t, f i x) x₀

theorem ContMDiffAt.sum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 ∈ t, ContMDiffAt I' I n (f i) x₀) : ContMDiffAt I' I n (fun (x : M) => ∑ i ∈ t, f i x) x₀

theorem contMDiffAt_finprod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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} {f : ι → M → G} (lf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) (h : ∀ (i : ι), ContMDiffAt I' I n (f i) x₀) : ContMDiffAt I' I n (fun (x : M) => ∏ᶠ (i : ι), f i x) x₀

theorem contMDiffAt_finsum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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} {f : ι → M → G} (lf : LocallyFinite fun (i : ι) => Function.support (f i)) (h : ∀ (i : ι), ContMDiffAt I' I n (f i) x₀) : ContMDiffAt I' I n (fun (x : M) => ∑ᶠ (i : ι), f i x) x₀

theorem contMDiffAt_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 ∈ t, ContMDiffAt I' I n (f i) x) : ContMDiffAt I' I n (∏ i ∈ t, f i) x

theorem contMDiffAt_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 ∈ t, ContMDiffAt I' I n (f i) x) : ContMDiffAt I' I n (∑ i ∈ t, f i) x

theorem contMDiffAt_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 ∈ t, ContMDiffAt I' I n (f i) x) : ContMDiffAt I' I n (fun (x : M) => ∏ i ∈ t, f i x) x

theorem contMDiffAt_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 ∈ t, ContMDiffAt I' I n (f i) x) : ContMDiffAt I' I n (fun (x : M) => ∑ i ∈ t, f i x) x

theorem contMDiffOn_finprod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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} {f : ι → M → G} (lf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) (h : ∀ (i : ι), ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (fun (x : M) => ∏ᶠ (i : ι), f i x) s

theorem contMDiffOn_finsum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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} {f : ι → M → G} (lf : LocallyFinite fun (i : ι) => Function.support (f i)) (h : ∀ (i : ι), ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (fun (x : M) => ∑ᶠ (i : ι), f i x) s

theorem contMDiffOn_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 ∈ t, ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (∏ i ∈ t, f i) s

theorem contMDiffOn_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 ∈ t, ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (∑ i ∈ t, f i) s

theorem contMDiffOn_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 ∈ t, ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (fun (x : M) => ∏ i ∈ t, f i x) s

theorem contMDiffOn_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 ∈ t, ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (fun (x : M) => ∑ i ∈ t, f i x) s

theorem ContMDiff.prod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 ∈ t, ContMDiff I' I n (f i)) : ContMDiff I' I n fun (x : M) => ∏ i ∈ t, f i x

theorem ContMDiff.sum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 ∈ t, ContMDiff I' I n (f i)) : ContMDiff I' I n fun (x : M) => ∑ i ∈ t, f i x

theorem contMDiff_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 ∈ t, ContMDiff I' I n (f i)) : ContMDiff I' I n (∏ i ∈ t, f i)

theorem contMDiff_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 ∈ t, ContMDiff I' I n (f i)) : ContMDiff I' I n (∑ i ∈ t, f i)

theorem contMDiff_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 ∈ t, ContMDiff I' I n (f i)) : ContMDiff I' I n fun (x : M) => ∏ i ∈ t, f i x

theorem contMDiff_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 ∈ t, ContMDiff I' I n (f i)) : ContMDiff I' I n fun (x : M) => ∑ i ∈ t, f i x

theorem contMDiff_finprod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 : ι), ContMDiff I' I n (f i)) (hfin : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) : ContMDiff I' I n fun (x : M) => ∏ᶠ (i : ι), f i x

theorem contMDiff_finsum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 : ι), ContMDiff I' I n (f i)) (hfin : LocallyFinite fun (i : ι) => Function.support (f i)) : ContMDiff I' I n fun (x : M) => ∑ᶠ (i : ι), f i x

theorem contMDiff_finprod_cond {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 → ContMDiff I' I n (f i)) (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) : ContMDiff I' I n fun (x : M) => ∏ᶠ (i : ι) (_ : p i), f i x

theorem contMDiff_finsum_cond {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 → ContMDiff I' I n (f i)) (hf : LocallyFinite fun (i : ι) => Function.support (f i)) : ContMDiff I' I n fun (x : M) => ∑ᶠ (i : ι) (_ : p i), f i x

theorem ContMDiffWithinAt.pow {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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} {g : M → G} (hg : ContMDiffWithinAt I' I n g s x) (m : ℕ) : ContMDiffWithinAt I' I n (fun (x : M) => g x ^ m) s x

theorem ContMDiffWithinAt.nsmul {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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} {g : M → G} (hg : ContMDiffWithinAt I' I n g s x) (m : ℕ) : ContMDiffWithinAt I' I n (fun (x : M) => m • g x) s x

theorem ContMDiffAt.pow {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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} {g : M → G} (hg : ContMDiffAt I' I n g x) (m : ℕ) : ContMDiffAt I' I n (fun (x : M) => g x ^ m) x

theorem ContMDiffAt.nsmul {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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} {g : M → G} (hg : ContMDiffAt I' I n g x) (m : ℕ) : ContMDiffAt I' I n (fun (x : M) => m • g x) x

theorem ContMDiffOn.pow {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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} {g : M → G} (hg : ContMDiffOn I' I n g s) (m : ℕ) : ContMDiffOn I' I n (fun (x : M) => g x ^ m) s

theorem ContMDiffOn.nsmul {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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} {g : M → G} (hg : ContMDiffOn I' I n g s) (m : ℕ) : ContMDiffOn I' I n (fun (x : M) => m • g x) s

theorem ContMDiff.pow {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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] {g : M → G} (hg : ContMDiff I' I n g) (m : ℕ) : ContMDiff I' I n fun (x : M) => g x ^ m

theorem ContMDiff.nsmul {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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] {g : M → G} (hg : ContMDiff I' I n g) (m : ℕ) : ContMDiff I' I n fun (x : M) => m • g x

instance instContMDiffAddSelf {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} : ContMDiffAdd (modelWithCornersSelf 𝕜 E) n E

theorem ContMDiffWithinAt.div_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 : ContMDiffWithinAt I' I n f s x) : ContMDiffWithinAt I' I n (fun (x : M) => f x / c) s x

theorem ContMDiffWithinAt.sub_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 : ContMDiffWithinAt I' I n f s x) : ContMDiffWithinAt I' I n (fun (x : M) => f x - c) s x

theorem ContMDiffAt.div_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 : ContMDiffAt I' I n f x) : ContMDiffAt I' I n (fun (x : M) => f x / c) x

theorem ContMDiffAt.sub_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 : ContMDiffAt I' I n f x) : ContMDiffAt I' I n (fun (x : M) => f x - c) x

theorem ContMDiffOn.div_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 : ContMDiffOn I' I n f s) : ContMDiffOn I' I n (fun (x : M) => f x / c) s

theorem ContMDiffOn.sub_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 : ContMDiffOn I' I n f s) : ContMDiffOn I' I n (fun (x : M) => f x - c) s

theorem ContMDiff.div_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffMul I n 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 : ContMDiff I' I n f) : ContMDiff I' I n fun (x : M) => f x / c

theorem ContMDiff.sub_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] [ContMDiffAdd I n 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 : ContMDiff I' I n f) : ContMDiff I' I n fun (x : M) => f x - c