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 : 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 → PartialHomeomorph.trans (PartialHomeomorph.symm e) e' ∈ contDiffGroupoid ⊤ I
• smooth_add : Smooth (ModelWithCorners.prod I 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 : 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 → PartialHomeomorph.trans (PartialHomeomorph.symm e) e' ∈ contDiffGroupoid ⊤ I
• smooth_mul : Smooth (ModelWithCorners.prod I 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 (ModelWithCorners.prod I 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 (ModelWithCorners.prod I I) I fun (p : G × G) => p.1 * p.2

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 = { val := leftMul g, property := ⋯ }

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 = { val := rightMul g, property := ⋯ }

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 : G) (h : G) : (smoothLeftMul I g) h = g * h

@[simp]

theorem R_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] (g : G) (h : G) : (smoothRightMul I g) h = h * g

@[simp]

theorem L_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_8} [Semigroup G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] (g : G) (h : G) : smoothLeftMul I (g * h) = ContMDiffMap.comp (smoothLeftMul I g) (smoothLeftMul I h)

@[simp]

theorem R_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_8} [Semigroup G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] (g : G) (h : G) : smoothRightMul I (g * h) = ContMDiffMap.comp (smoothRightMul I h) (smoothRightMul I g)

theorem smoothLeftMul_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G' : Type u_8} [Monoid G'] [TopologicalSpace G'] [ChartedSpace H G'] [SmoothMul I G'] (g' : G') : (smoothLeftMul I g') 1 = g'

theorem smoothRightMul_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G' : Type u_8} [Monoid G'] [TopologicalSpace G'] [ChartedSpace H G'] [SmoothMul I G'] (g' : G') : (smoothRightMul I g') 1 = g'

instance SmoothAdd.sum {𝕜 : Type u_8} [NontriviallyNormedField 𝕜] {E : Type u_9} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_10} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (G : Type u_11) [TopologicalSpace G] [ChartedSpace H G] [Add G] [SmoothAdd I G] {E' : Type u_12} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_13} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') (G' : Type u_14) [TopologicalSpace G'] [ChartedSpace H' G'] [Add G'] [SmoothAdd I' G'] : SmoothAdd (ModelWithCorners.prod I I') (G × G')

Equations

• ⋯ = ⋯

instance SmoothMul.prod {𝕜 : Type u_8} [NontriviallyNormedField 𝕜] {E : Type u_9} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_10} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (G : Type u_11) [TopologicalSpace G] [ChartedSpace H G] [Mul G] [SmoothMul I G] {E' : Type u_12} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_13} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') (G' : Type u_14) [TopologicalSpace G'] [ChartedSpace H' G'] [Mul G'] [SmoothMul I' G'] : SmoothMul (ModelWithCorners.prod I I') (G × G')

Equations

• ⋯ = ⋯

abbrev smooth_nsmul.match_1 (motive : ℕ → Prop) : ∀ (x : ℕ), (Unit → motive 0) → (∀ (k : ℕ), motive (Nat.succ k)) → motive x

Equations

• ⋯ = ⋯

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

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

structure SmoothAddMonoidMorphism {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜 E' H') (G : Type u_8) [TopologicalSpace G] [ChartedSpace H G] [AddMonoid G] [SmoothAdd I G] (G' : Type u_9) [TopologicalSpace G'] [ChartedSpace H' G'] [AddMonoid G'] [SmoothAdd I' G'] extends AddMonoidHom : Type (max u_8 u_9)

Morphism of additive smooth monoids.

• toFun : G → G'
• map_zero' : self.toFun 0 = 0
• map_add' : ∀ (x y : G), self.toFun (x + y) = self.toFun x + self.toFun y
• smooth_toFun : Smooth I I' self.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 MonoidHom : Type (max u_8 u_9)

Morphism of smooth monoids.

• toFun : G → G'
• map_one' : self.toFun 1 = 1
• map_mul' : ∀ (x y : G), self.toFun (x * y) = self.toFun x * self.toFun y
• smooth_toFun : Smooth I I' self.toFun

theorem instZeroSmoothAddMonoidMorphism.proof_1 {𝕜 : Type u_7} [NontriviallyNormedField 𝕜] {H : Type u_5} [TopologicalSpace H] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] {H' : Type u_2} [TopologicalSpace H'] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_1} [AddMonoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] : Smooth I I' fun (x : G) => AddZeroClass.toZero.1

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 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 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 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 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.toFun, coe_injective' := ⋯ }

theorem instFunLikeSmoothAddMonoidMorphism.proof_1 {𝕜 : Type u_7} [NontriviallyNormedField 𝕜] {H : Type u_6} [TopologicalSpace H] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_2} [AddMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {H' : Type u_4} [TopologicalSpace H'] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_1} [AddMonoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] [SmoothAdd I' G'] (f : SmoothAddMonoidMorphism I I' G G') (g : SmoothAddMonoidMorphism I I' G G') (h : (fun (a : SmoothAddMonoidMorphism I I' G G') => a.toFun) f = (fun (a : SmoothAddMonoidMorphism I I' G G') => a.toFun) g) : f = g

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.toFun, coe_injective' := ⋯ }

instance instAddMonoidHomClassSmoothAddMonoidMorphismToAddZeroClassToAddZeroClassInstFunLikeSmoothAddMonoidMorphism {𝕜 : 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 instMonoidHomClassSmoothMonoidMorphismToMulOneClassToMulOneClassInstFunLikeSmoothMonoidMorphism {𝕜 : 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 instContinuousMapClassSmoothAddMonoidMorphismInstFunLikeSmoothAddMonoidMorphism {𝕜 : 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

• ⋯ = ⋯

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

• ⋯ = ⋯

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.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) => Finset.sum t fun (i : ι) => f i x) s x₀

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) => Finset.prod t fun (i : ι) => f i x) s x₀

abbrev contMDiffWithinAt_finsum.match_1 {ι : Type u_1} {G : Type u_3} [AddCommMonoid G] {M : Type u_2} [TopologicalSpace M] {f : ι → M → G} {x₀ : M} (motive : (∃ (s : Finset ι), ∀ᶠ (y : M) in nhds x₀, (finsum fun (i : ι) => f i y) = Finset.sum s fun (i : ι) => f i y) → Prop) : ∀ (x : ∃ (s : Finset ι), ∀ᶠ (y : M) in nhds x₀, (finsum fun (i : ι) => f i y) = Finset.sum s fun (i : ι) => f i y), (∀ (_I : Finset ι) (hI : ∀ᶠ (y : M) in nhds x₀, (finsum fun (i : ι) => f i y) = Finset.sum _I fun (i : ι) => f i y), motive ⋯) → motive x

Equations

• ⋯ = ⋯

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) => finsum fun (i : ι) => 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) => finprod fun (i : ι) => 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 (Finset.sum t fun (i : ι) => f i) s x

theorem contMDiffWithinAt_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) : ContMDiffWithinAt I' I n (Finset.prod t fun (i : ι) => 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 (fun (x : M) => Finset.sum t fun (i : ι) => f i x) s x

theorem contMDiffWithinAt_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) : ContMDiffWithinAt I' I n (fun (x : M) => Finset.prod t fun (i : ι) => f i x) s 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) => Finset.sum t fun (i : ι) => f i x) 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) => Finset.prod t fun (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) => finsum fun (i : ι) => 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) => finprod fun (i : ι) => 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 (Finset.sum t fun (i : ι) => f i) x

theorem contMDiffAt_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x) : ContMDiffAt I' I n (Finset.prod t fun (i : ι) => 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 (fun (x : M) => Finset.sum t fun (i : ι) => f i x) x

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

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) => finsum fun (i : ι) => f i x) s

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) => finprod fun (i : ι) => 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 (Finset.sum t fun (i : ι) => f i) s

theorem contMDiffOn_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {s : Set M} {t : Finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (Finset.prod t fun (i : ι) => 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 (fun (x : M) => Finset.sum t fun (i : ι) => f i x) s

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

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) => Finset.sum t fun (i : ι) => f i x

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) => Finset.prod t fun (i : ι) => 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 (Finset.sum t fun (i : ι) => f i)

theorem contMDiff_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {t : Finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ i ∈ t, ContMDiff I' I n (f i)) : ContMDiff I' I n (Finset.prod t fun (i : ι) => 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 fun (x : M) => Finset.sum t fun (i : ι) => f i x

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

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

theorem contMDiff_finprod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), ContMDiff I' I n (f i)) (hfin : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) : ContMDiff I' I n fun (x : M) => finprod fun (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) => finsum fun (i : ι) => finsum fun (x_1 : p i) => f i x

theorem contMDiff_finprod_cond {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : ι → M → G} {n : ℕ∞} {p : ι → Prop} (hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)) (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) : ContMDiff I' I n fun (x : M) => finprod fun (i : ι) => finprod fun (x_1 : p i) => f i 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) => finsum fun (i : ι) => f i x) 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) => finprod fun (i : ι) => f i x) 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 (Finset.sum t fun (i : ι) => f i) s x

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

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

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

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

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

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

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

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

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

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

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

theorem smooth_finprod {ι : Type u_1} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : ι → M → G} (h : ∀ (i : ι), Smooth I' I (f i)) (hfin : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) : Smooth I' I fun (x : M) => finprod fun (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) => finsum fun (i : ι) => finsum fun (x_1 : p i) => f i x

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

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

Equations

• ⋯ = ⋯

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

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