Documentation

Mathlib.Geometry.Manifold.Algebra.Monoid

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 :

Basic hypothesis to talk about a smooth (Lie) additive monoid or a smooth additive semigroup. A smooth additive monoid over Ξ±, for example, is obtained by requiring both the instances AddMonoid Ξ± and SmoothAdd Ξ±.

Instances
    theorem SmoothAdd.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] [self : SmoothAdd I G] :
    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 :

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

    Instances
      theorem SmoothMul.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] [self : 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 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 continuousAdd_of_smooth {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] :

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

      theorem continuousMul_of_smooth {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] :

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

      theorem ContMDiffWithinAt.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners π•œ E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M β†’ G} {g : M β†’ G} {s : Set M} {x : M} {n : β„•βˆž} (hf : ContMDiffWithinAt I' I n f s x) (hg : ContMDiffWithinAt I' I n g s x) :
      ContMDiffWithinAt I' I n (f + g) s x
      theorem ContMDiffWithinAt.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners π•œ E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M β†’ G} {g : M β†’ G} {s : Set M} {x : M} {n : β„•βˆž} (hf : ContMDiffWithinAt I' I n f s x) (hg : ContMDiffWithinAt I' I n g s x) :
      ContMDiffWithinAt I' I n (f * g) s x
      theorem ContMDiffAt.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners π•œ E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M β†’ G} {g : M β†’ G} {x : M} {n : β„•βˆž} (hf : ContMDiffAt I' I n f x) (hg : ContMDiffAt I' I n g x) :
      ContMDiffAt I' I n (f + g) x
      theorem ContMDiffAt.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners π•œ E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M β†’ G} {g : M β†’ G} {x : M} {n : β„•βˆž} (hf : ContMDiffAt I' I n f x) (hg : ContMDiffAt I' I n g x) :
      ContMDiffAt I' I n (f * g) x
      theorem ContMDiffOn.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners π•œ E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M β†’ G} {g : M β†’ G} {s : Set M} {n : β„•βˆž} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) :
      ContMDiffOn I' I n (f + g) s
      theorem ContMDiffOn.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners π•œ E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M β†’ G} {g : M β†’ G} {s : Set M} {n : β„•βˆž} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) :
      ContMDiffOn I' I n (f * g) s
      theorem ContMDiff.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [SmoothAdd I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners π•œ E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : M β†’ G} {g : M β†’ G} {n : β„•βˆž} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) :
      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) :

      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
      Instances For
        def smoothRightMul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] (g : G) :

        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
        Instances For
          @[simp]
          theorem L_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] (g : G) (h : G) :
          (smoothLeftMul I g) h = g * h
          @[simp]
          theorem R_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] (g : G) (h : G) :
          (smoothRightMul I g) h = h * g
          @[simp]
          theorem L_mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) {G : Type u_8} [Semigroup G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] (g : G) (h : G) :
          smoothLeftMul I (g * h) = (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 : G) (h : 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 (I.prod 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 (I.prod I') (G Γ— G')
          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
          abbrev smooth_nsmul.match_1 (motive : β„• β†’ Prop) :
          βˆ€ (x : β„•), (Unit β†’ motive 0) β†’ (βˆ€ (k : β„•), motive k.succ) β†’ motive x
          Equations
          • β‹― = β‹―
          Instances For
            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.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
            Instances For
              theorem SmoothAddMonoidMorphism.smooth_toFun {π•œ : 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'] (self : SmoothAddMonoidMorphism I I' G G') :
              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 MonoidHom :
              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
              Instances For
                theorem SmoothMonoidMorphism.smooth_toFun {π•œ : 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'] (self : SmoothMonoidMorphism I I' G G') :
                Smooth I I' (↑self.toMonoidHom).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'] :
                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'] :
                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'] :
                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'] :
                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'] :
                Equations
                • instFunLikeSmoothAddMonoidMorphism = { coe := fun (a : SmoothAddMonoidMorphism I I' G G') => (↑a.toAddMonoidHom).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.toAddMonoidHom).toFun) f = (fun (a : SmoothAddMonoidMorphism I I' G G') => (↑a.toAddMonoidHom).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.toMonoidHom).toFun, coe_injective' := β‹― }
                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'] :
                Equations
                • β‹― = β‹―
                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'] :
                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'] :
                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'] :
                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) => t.sum 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) => t.prod fun (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) => finsum 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) = s.sum fun (i : ΞΉ) => f i y) β†’ Prop) :
                βˆ€ (x : βˆƒ (s : Finset ΞΉ), βˆ€αΆ  (y : M) in nhds xβ‚€, (finsum fun (i : ΞΉ) => f i y) = s.sum fun (i : ΞΉ) => f i y), (βˆ€ (_I : Finset ΞΉ) (hI : βˆ€αΆ  (y : M) in nhds xβ‚€, (finsum fun (i : ΞΉ) => f i y) = _I.sum fun (i : ΞΉ) => f i y), motive β‹―) β†’ motive x
                Equations
                • β‹― = β‹―
                Instances For
                  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 (t.sum 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 (t.prod 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) => t.sum 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) => t.prod 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) => t.sum 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) => t.prod 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 (t.sum 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 (t.prod 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) => t.sum 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) => t.prod 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 (t.sum 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 (t.prod 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) => t.sum 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) => t.prod 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) => t.sum 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) => t.prod 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 (t.sum 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 (t.prod 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) => t.sum 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) => t.prod 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 (t.sum 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 (t.prod 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) => t.sum 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) => t.prod 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 (t.sum 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 (t.prod 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) => t.sum 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) => t.prod 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 (t.sum 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 (t.prod 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) => t.sum 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) => t.prod 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 (t.sum 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 (t.prod 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) => t.sum 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) => t.prod 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] :
                  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