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

theorem smooth_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] : Smooth (I.prod I) I fun (p : G × G) => p.1 * p.2

theorem smooth_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] : Smooth (I.prod I) I fun (p : G × G) => p.1 + p.2

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)

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} (hf : SmoothWithinAt I' I f s x) (hg : SmoothWithinAt I' I g s x) : SmoothWithinAt I' I (f * g) s x

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} (hf : SmoothWithinAt I' I f s x) (hg : SmoothWithinAt I' I g s x) : SmoothWithinAt I' I (f + g) s x

theorem SmoothAt.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f g : M → G} {x : M} (hf : SmoothAt I' I f x) (hg : SmoothAt I' I g x) : SmoothAt I' I (f * g) x

theorem SmoothAt.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f g : M → G} {x : M} (hf : SmoothAt I' I f x) (hg : SmoothAt I' I g x) : SmoothAt I' I (f + g) x

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} (hf : SmoothOn I' I f s) (hg : SmoothOn I' I g s) : SmoothOn I' I (f * g) s

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} (hf : SmoothOn I' I f s) (hg : SmoothOn I' I g s) : SmoothOn I' I (f + g) s

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} (hf : Smooth I' I f) (hg : Smooth I' I g) : Smooth I' I (f * g)

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} (hf : Smooth I' I f) (hg : Smooth I' I g) : Smooth I' I (f + g)

theorem smooth_mul_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {a : G} : Smooth I I fun (b : G) => a * b

theorem smooth_add_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {a : G} : Smooth I I fun (b : G) => a + b

theorem smooth_mul_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {a : G} : Smooth I I fun (b : G) => b * a

theorem smooth_add_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {a : G} : Smooth I I fun (b : G) => b + a

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

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

Equations

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

def LieGroup.«term𝑹» : Lean.ParserDescr

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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 : Smooth 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 : Smooth 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'

Equations

• ⋯ = ⋯

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'

Equations

• ⋯ = ⋯

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'

Equations

• ⋯ = ⋯

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'

Equations

• ⋯ = ⋯

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

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} (lf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) (h : ∀ (i : ι), SmoothAt I' I (f i) x₀) : SmoothAt I' I (fun (x : M) => ∏ᶠ (i : ι), f i x) x₀

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} (lf : LocallyFinite fun (i : ι) => Function.support (f i)) (h : ∀ (i : ι), SmoothAt I' I (f i) x₀) : SmoothAt I' I (fun (x : M) => ∑ᶠ (i : ι), f i x) x₀

theorem smoothWithinAt_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s x) : SmoothWithinAt I' I (∏ i ∈ t, f i) s x

theorem smoothWithinAt_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s x) : SmoothWithinAt I' I (∑ i ∈ t, f i) s x

theorem smoothWithinAt_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s x) : SmoothWithinAt I' I (fun (x : M) => ∏ i ∈ t, f i x) s x

theorem smoothWithinAt_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s x) : SmoothWithinAt I' I (fun (x : M) => ∑ i ∈ t, f i x) s x

theorem smoothAt_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, SmoothAt I' I (f i) x) : SmoothAt I' I (∏ i ∈ t, f i) x

theorem smoothAt_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, SmoothAt I' I (f i) x) : SmoothAt I' I (∑ i ∈ t, f i) x

theorem smoothAt_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, SmoothAt I' I (f i) x) : SmoothAt I' I (fun (x : M) => ∏ i ∈ t, f i x) x

theorem smoothAt_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, SmoothAt I' I (f i) x) : SmoothAt I' I (fun (x : M) => ∑ i ∈ t, f i x) x

theorem smoothOn_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {s : Set M} {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, SmoothOn I' I (f i) s) : SmoothOn I' I (∏ i ∈ t, f i) s

theorem smoothOn_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {s : Set M} {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, SmoothOn I' I (f i) s) : SmoothOn I' I (∑ i ∈ t, f i) s

theorem smoothOn_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {s : Set M} {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, SmoothOn I' I (f i) s) : SmoothOn I' I (fun (x : M) => ∏ i ∈ t, f i x) s

theorem smoothOn_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {s : Set M} {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, SmoothOn I' I (f i) s) : SmoothOn I' I (fun (x : M) => ∑ i ∈ t, f i x) s

theorem smooth_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, Smooth I' I (f i)) : Smooth I' I (∏ i ∈ t, f i)

theorem smooth_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, Smooth I' I (f i)) : Smooth I' I (∑ i ∈ t, f i)

theorem smooth_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, Smooth I' I (f i)) : Smooth I' I fun (x : M) => ∏ i ∈ t, f i x

theorem smooth_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {t : Finset ι} {f : ι → M → G} (h : ∀ i ∈ t, Smooth I' I (f i)) : Smooth I' I fun (x : M) => ∑ i ∈ t, f i x

theorem smooth_finprod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : ι → M → G} (h : ∀ (i : ι), Smooth I' I (f i)) (hfin : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) : Smooth I' I fun (x : M) => ∏ᶠ (i : ι), f i x

theorem smooth_finsum {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : ι → M → G} (h : ∀ (i : ι), Smooth I' I (f i)) (hfin : LocallyFinite fun (i : ι) => Function.support (f i)) : Smooth I' I fun (x : M) => ∑ᶠ (i : ι), f i x

theorem smooth_finprod_cond {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : ι → M → G} {p : ι → Prop} (hc : ∀ (i : ι), p i → Smooth I' I (f i)) (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) : Smooth I' I fun (x : M) => ∏ᶠ (i : ι) (_ : p i), f i x

theorem smooth_finsum_cond {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : ι → M → G} {p : ι → Prop} (hc : ∀ (i : ι), p i → Smooth I' I (f i)) (hf : LocallyFinite fun (i : ι) => Function.support (f i)) : Smooth I' I fun (x : M) => ∑ᶠ (i : ι) (_ : p i), f i x

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

Equations

• ⋯ = ⋯

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

theorem SmoothWithinAt.div_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M → G} {s : Set M} {x : M} (c : G) (hf : SmoothWithinAt I' I f s x) : SmoothWithinAt I' I (fun (x : M) => f x / c) s x

theorem SmoothWithinAt.sub_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [SubNegMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M → G} {s : Set M} {x : M} (c : G) (hf : SmoothWithinAt I' I f s x) : SmoothWithinAt I' I (fun (x : M) => f x - c) s x

theorem SmoothAt.div_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M → G} {x : M} (c : G) (hf : SmoothAt I' I f x) : SmoothAt I' I (fun (x : M) => f x / c) x

theorem SmoothAt.sub_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [SubNegMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M → G} {x : M} (c : G) (hf : SmoothAt I' I f x) : SmoothAt I' I (fun (x : M) => f x - c) x

theorem SmoothOn.div_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M → G} {s : Set M} (c : G) (hf : SmoothOn I' I f s) : SmoothOn I' I (fun (x : M) => f x / c) s

theorem SmoothOn.sub_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [SubNegMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M → G} {s : Set M} (c : G) (hf : SmoothOn I' I f s) : SmoothOn I' I (fun (x : M) => f x - c) s

theorem Smooth.div_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M → G} (c : G) (hf : Smooth I' I f) : Smooth I' I fun (x : M) => f x / c

theorem Smooth.sub_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [SubNegMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M → G} (c : G) (hf : Smooth I' I f) : Smooth I' I fun (x : M) => f x - c