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 I G : Prop

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 α.

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

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 I G : Prop

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.

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

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

@[deprecated contMDiff_mul (since := "2024-11-20")]

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] : ContMDiff (I.prod I) I ⊤ fun (p : G × G) => p.1 * p.2

Alias of contMDiff_mul.

@[deprecated contMDiff_add (since := "2024-11-20")]

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] : ContMDiff (I.prod I) I ⊤ fun (p : G × G) => p.1 + p.2

Alias of contMDiff_add.

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] : ContinuousMul 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 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] : ContinuousAdd 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 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 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.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 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.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 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.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 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.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 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.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 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.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 g : M → G} {n : ℕ∞} (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} {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 g : M → G} {n : ℕ∞} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) : ContMDiff I' I n (f + g)

@[deprecated ContMDiffWithinAt.mul (since := "2024-11-21")]

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

Alias of ContMDiffWithinAt.mul.

@[deprecated ContMDiffAt.mul (since := "2024-11-21")]

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

Alias of ContMDiffAt.mul.

@[deprecated ContMDiffOn.mul (since := "2024-11-21")]

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

Alias of ContMDiffOn.mul.

@[deprecated ContMDiff.mul (since := "2024-11-21")]

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 g : M → G} {n : ℕ∞} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) : ContMDiff I' I n (f * g)

Alias of ContMDiff.mul.

@[deprecated ContMDiffWithinAt.add (since := "2024-11-21")]

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

Alias of ContMDiffWithinAt.add.

@[deprecated ContMDiffAt.add (since := "2024-11-21")]

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

Alias of ContMDiffAt.add.

@[deprecated ContMDiffOn.add (since := "2024-11-21")]

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

Alias of ContMDiffOn.add.

@[deprecated ContMDiff.add (since := "2024-11-21")]

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 g : M → G} {n : ℕ∞} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) : ContMDiff I' I n (f + g)

Alias of ContMDiff.add.

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} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {n : ℕ∞} {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} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {n : ℕ∞} {a : G} : ContMDiff I I n fun (x : G) => a + x

@[deprecated contMDiff_mul_left (since := "2024-11-21")]

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] {n : ℕ∞} {a : G} : ContMDiff I I n fun (x : G) => a * x

Alias of contMDiff_mul_left.

@[deprecated contMDiff_add_left (since := "2024-11-21")]

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] {n : ℕ∞} {a : G} : ContMDiff I I n fun (x : G) => a + x

Alias of contMDiff_add_left.

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} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {n : ℕ∞} {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} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {n : ℕ∞} {a b : G} : ContMDiffAt I I n (fun (x : G) => a + x) 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] [SmoothMul I G] {a : G} : MDifferentiable I I 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] [SmoothAdd I G] {a : G} : MDifferentiable I I 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] [SmoothMul I G] {a b : G} : MDifferentiableAt I I (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] [SmoothAdd I G] {a b : G} : MDifferentiableAt I I (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} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {n : ℕ∞} {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} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {n : ℕ∞} {a : G} : ContMDiff I I n fun (x : G) => x + a

@[deprecated contMDiff_mul_right (since := "2024-11-21")]

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] {n : ℕ∞} {a : G} : ContMDiff I I n fun (x : G) => x * a

Alias of contMDiff_mul_right.

@[deprecated contMDiff_add_right (since := "2024-11-21")]

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] {n : ℕ∞} {a : G} : ContMDiff I I n fun (x : G) => x + a

Alias of contMDiff_add_right.

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} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {n : ℕ∞} {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} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {n : ℕ∞} {a b : G} : ContMDiffAt I I n (fun (x : G) => x + a) 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] [SmoothMul I G] {a : G} : MDifferentiable I I 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] [SmoothAdd I G] {a : G} : MDifferentiable I I 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] [SmoothMul I G] {a b : G} : MDifferentiableAt I I (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] [SmoothAdd I G] {a b : G} : MDifferentiableAt I I (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] [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.

Equations

• smoothLeftMul I g = ⟨leftMul g, ⋯⟩

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.

Equations

• smoothRightMul I g = ⟨rightMul g, ⋯⟩

def LieGroup.«term𝑳» : Lean.ParserDescr

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.

Equations

• LieGroup.«term𝑳» = Lean.ParserDescr.node `LieGroup.«term𝑳» 1024 (Lean.ParserDescr.symbol "𝑳")

def LieGroup.«term𝑹» : Lean.ParserDescr

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.

Equations

• LieGroup.«term𝑹» = Lean.ParserDescr.node `LieGroup.«term𝑹» 1024 (Lean.ParserDescr.symbol "𝑹")

@[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 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 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 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] [SmoothMul 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'] [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'

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 (I.prod 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 (I.prod I') (G × G')

theorem contMDiff_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 : ℕ) : ContMDiff I I ⊤ fun (a : G) => a ^ n

theorem contMDiff_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 : ℕ) : ContMDiff I I ⊤ fun (a : G) => n • a

@[deprecated contMDiff_pow (since := "2024-11-21")]

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 : ℕ) : ContMDiff I I ⊤ fun (a : G) => a ^ n

Alias of contMDiff_pow.

@[deprecated contMDiff_nsmul (since := "2024-11-21")]

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 : ℕ) : ContMDiff I I ⊤ fun (a : G) => n • a

Alias of contMDiff_nsmul.

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 G →+ G' : Type (max u_8 u_9)

Morphism of additive smooth 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
• smooth_toFun : ContMDiff I I' ⊤ (↑self.toAddMonoidHom).toFun

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 G →* G' : Type (max u_8 u_9)

Morphism of smooth 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
• smooth_toFun : ContMDiff I I' ⊤ (↑self.toMonoidHom).toFun

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

Equations

• instOneSmoothMonoidMorphism = { one := { toMonoidHom := 1, smooth_toFun := ⋯ } }

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

Equations

• instZeroSmoothAddMonoidMorphism = { zero := { toAddMonoidHom := 0, smooth_toFun := ⋯ } }

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

Equations

• instInhabitedSmoothMonoidMorphism = { default := 1 }

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

Equations

• instInhabitedSmoothAddMonoidMorphism = { default := 0 }

instance instFunLikeSmoothMonoidMorphism {𝕜 : 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'] : FunLike (SmoothMonoidMorphism I I' G G') G G'

Equations

• instFunLikeSmoothMonoidMorphism = { coe := fun (a : SmoothMonoidMorphism I I' G G') => (↑a.toMonoidHom).toFun, coe_injective' := ⋯ }

instance instFunLikeSmoothAddMonoidMorphism {𝕜 : 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'] : FunLike (SmoothAddMonoidMorphism I I' G G') G G'

Equations

• instFunLikeSmoothAddMonoidMorphism = { coe := fun (a : SmoothAddMonoidMorphism I I' G G') => (↑a.toAddMonoidHom).toFun, coe_injective' := ⋯ }

instance instMonoidHomClassSmoothMonoidMorphism {𝕜 : 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'

instance instAddMonoidHomClassSmoothAddMonoidMorphism {𝕜 : 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'

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'

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'

Differentiability of finite point-wise sums and products

Finite point-wise products (resp. sums) of differentiable/smooth functions M → G (at x/on s) into a commutative monoid G are differentiable/smooth at x/on s.

theorem ContMDiffWithinAt.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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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} {f : ι → M → G} {n : ℕ∞} (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 𝕜] {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} {f : ι → M → G} {n : ℕ∞} (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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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} {f : ι → M → G} {n : ℕ∞} (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 𝕜] {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} {f : ι → M → G} {n : ℕ∞} (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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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} {f : ι → M → G} {n : ℕ∞} (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 𝕜] {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} {f : ι → M → G} {n : ℕ∞} (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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 ∈ 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 𝕜] {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 : M) => ∏ᶠ (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 : M) => ∑ᶠ (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 : M) => ∏ᶠ (i : ι) (_ : p 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 : M) => ∑ᶠ (i : ι) (_ : p i), f i x

@[deprecated contMDiffAt_finprod (since := "2024-11-21")]

theorem smoothAt_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] {x₀ : M} {f : ι → M → G} {n : ℕ∞} (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₀

Alias of contMDiffAt_finprod.

@[deprecated contMDiffAt_finsum (since := "2024-11-21")]

theorem smoothAt_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] {x₀ : M} {f : ι → M → G} {n : ℕ∞} (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₀

Alias of contMDiffAt_finsum.

@[deprecated contMDiffWithinAt_finset_prod' (since := "2024-11-21")]

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} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) : ContMDiffWithinAt I' I n (∏ i ∈ t, f i) s x

Alias of contMDiffWithinAt_finset_prod'.

@[deprecated contMDiffWithinAt_finset_sum' (since := "2024-11-21")]

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} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) : ContMDiffWithinAt I' I n (∑ i ∈ t, f i) s x

Alias of contMDiffWithinAt_finset_sum'.

@[deprecated contMDiffWithinAt_finset_prod (since := "2024-11-21")]

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} {n : ℕ∞} (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

Alias of contMDiffWithinAt_finset_prod.

@[deprecated contMDiffWithinAt_finset_sum (since := "2024-11-21")]

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} {n : ℕ∞} (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

Alias of contMDiffWithinAt_finset_sum.

@[deprecated contMDiffAt_finset_prod' (since := "2024-11-21")]

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} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x) : ContMDiffAt I' I n (∏ i ∈ t, f i) x

Alias of contMDiffAt_finset_prod'.

@[deprecated contMDiffAt_finset_sum' (since := "2024-11-21")]

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} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x) : ContMDiffAt I' I n (∑ i ∈ t, f i) x

Alias of contMDiffAt_finset_sum'.

@[deprecated contMDiffAt_finset_prod (since := "2024-11-21")]

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} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x) : ContMDiffAt I' I n (fun (x : M) => ∏ i ∈ t, f i x) x

Alias of contMDiffAt_finset_prod.

@[deprecated contMDiffAt_finset_sum (since := "2024-11-21")]

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} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x) : ContMDiffAt I' I n (fun (x : M) => ∑ i ∈ t, f i x) x

Alias of contMDiffAt_finset_sum.

@[deprecated contMDiffOn_finset_prod' (since := "2024-11-21")]

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} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (∏ i ∈ t, f i) s

Alias of contMDiffOn_finset_prod'.

@[deprecated contMDiffOn_finset_sum' (since := "2024-11-21")]

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} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (∑ i ∈ t, f i) s

Alias of contMDiffOn_finset_sum'.

@[deprecated contMDiffOn_finset_prod (since := "2024-11-21")]

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} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (fun (x : M) => ∏ i ∈ t, f i x) s

Alias of contMDiffOn_finset_prod.

@[deprecated contMDiffOn_finset_sum (since := "2024-11-21")]

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} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (fun (x : M) => ∑ i ∈ t, f i x) s

Alias of contMDiffOn_finset_sum.

@[deprecated contMDiffOn_finset_prod' (since := "2024-11-21")]

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] {s : Set M} {t : Finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (∏ i ∈ t, f i) s

Alias of contMDiffOn_finset_prod'.

@[deprecated contMDiffOn_finset_sum' (since := "2024-11-21")]

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] {s : Set M} {t : Finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (∑ i ∈ t, f i) s

Alias of contMDiffOn_finset_sum'.

@[deprecated contMDiff_finset_prod (since := "2024-11-21")]

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} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiff I' I n (f i)) : ContMDiff I' I n fun (x : M) => ∏ i ∈ t, f i x

Alias of contMDiff_finset_prod.

@[deprecated contMDiff_finset_sum (since := "2024-11-21")]

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} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiff I' I n (f i)) : ContMDiff I' I n fun (x : M) => ∑ i ∈ t, f i x

Alias of contMDiff_finset_sum.

@[deprecated contMDiff_finprod (since := "2024-11-21")]

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} {n : ℕ∞} (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

Alias of contMDiff_finprod.

@[deprecated contMDiff_finsum (since := "2024-11-21")]

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} {n : ℕ∞} (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

Alias of contMDiff_finsum.

@[deprecated contMDiff_finprod_cond (since := "2024-11-21")]

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} {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 : M) => ∏ᶠ (i : ι) (_ : p i), f i x

Alias of contMDiff_finprod_cond.

@[deprecated contMDiff_finsum_cond (since := "2024-11-21")]

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} {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 : M) => ∑ᶠ (i : ι) (_ : p i), f i x

Alias of contMDiff_finsum_cond.

instance hasSmoothAddSelf {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] : SmoothAdd (modelWithCornersSelf 𝕜 E) E

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 : M) => f x / c) s x

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 : M) => f x - c) s 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 : M) => f x / c) 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 : M) => f x - c) x

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 : M) => f x / c) s

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 : M) => f x - c) s

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) : ContMDiff I' I n fun (x : M) => f x / c

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) : ContMDiff I' I n fun (x : M) => f x - c

@[deprecated ContMDiffWithinAt.div_const (since := "2024-11-21")]

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} {n : ℕ∞} (c : G) (hf : ContMDiffWithinAt I' I n f s x) : ContMDiffWithinAt I' I n (fun (x : M) => f x / c) s x

Alias of ContMDiffWithinAt.div_const.

@[deprecated ContMDiffAt.div_const (since := "2024-11-21")]

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} {n : ℕ∞} (c : G) (hf : ContMDiffAt I' I n f x) : ContMDiffAt I' I n (fun (x : M) => f x / c) x

Alias of ContMDiffAt.div_const.

@[deprecated ContMDiffOn.div_const (since := "2024-11-21")]

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} {n : ℕ∞} (c : G) (hf : ContMDiffOn I' I n f s) : ContMDiffOn I' I n (fun (x : M) => f x / c) s

Alias of ContMDiffOn.div_const.

@[deprecated ContMDiff.div_const (since := "2024-11-21")]

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} {n : ℕ∞} (c : G) (hf : ContMDiff I' I n f) : ContMDiff I' I n fun (x : M) => f x / c

Alias of ContMDiff.div_const.