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
    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 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 => p.fst + p.snd
      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 => p.fst * p.snd
      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 => 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 => 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 => 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 => 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.

      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.

        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) :
          @[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'
          theorem SmoothAdd.sum.proof_1 {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (G : Type u_4) [TopologicalSpace G] [ChartedSpace H G] [Add G] [SmoothAdd I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners π•œ E' H') (G' : Type u_7) [TopologicalSpace G'] [ChartedSpace H' G'] [Add G'] [SmoothAdd I' 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'] :
          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'] :
          abbrev smooth_nsmul.match_1 (motive : β„• β†’ Prop) :
          (x : β„•) β†’ (Unit β†’ motive 0) β†’ ((k : β„•) β†’ motive (Nat.succ k)) β†’ motive x
          Instances For
            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 => 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 => 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.

            Instances For
              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.

              Instances For
                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'] :
                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 => AddZeroClass.toZero.1
                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'] :
                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'] :
                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'] :
                instance instAddMonoidHomClassSmoothAddMonoidMorphismToAddZeroClassToAddZeroClass {π•œ : Type u_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'] :
                theorem instAddMonoidHomClassSmoothAddMonoidMorphismToAddZeroClassToAddZeroClass.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 => a.toFun) f = (fun a => a.toFun) g) :
                f = g
                theorem instAddMonoidHomClassSmoothAddMonoidMorphismToAddZeroClassToAddZeroClass.proof_2 {π•œ : 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') (a : G) (b : G) :
                ↑f.toAddMonoidHom (a + b) = ↑f.toAddMonoidHom a + ↑f.toAddMonoidHom b
                theorem instAddMonoidHomClassSmoothAddMonoidMorphismToAddZeroClassToAddZeroClass.proof_3 {π•œ : 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') :
                ↑f.toAddMonoidHom 0 = 0
                instance instMonoidHomClassSmoothMonoidMorphismToMulOneClassToMulOneClass {π•œ : Type u_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'] :
                theorem instContinuousMapClassSmoothAddMonoidMorphism.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') :
                Continuous f.toFun
                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'] :
                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'] :
                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 : ΞΉ), 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 : ΞΉ), i ∈ t β†’ ContMDiffWithinAt I' I n (f i) s x) :
                ContMDiffWithinAt I' I n (Finset.prod t fun i => f i) s 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 : ΞΉ), 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 : ΞΉ), i ∈ t β†’ ContMDiffAt I' I n (f i) x) :
                ContMDiffAt I' I n (Finset.prod t fun i => f i) x
                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 : ΞΉ), 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 : ΞΉ), i ∈ t β†’ ContMDiffOn I' I n (f i) s) :
                ContMDiffOn I' I n (Finset.prod t fun i => f i) s
                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 : ΞΉ), 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 : ΞΉ), i ∈ t β†’ ContMDiff I' I n (f i)) :
                ContMDiff I' I n (Finset.prod t fun i => f i)
                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 : ΞΉ), i ∈ t β†’ ContMDiffWithinAt I' I n (f i) s x) :
                ContMDiffWithinAt I' I n (fun x => 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 : ΞΉ), i ∈ t β†’ ContMDiffWithinAt I' I n (f i) s x) :
                ContMDiffWithinAt I' I n (fun x => Finset.prod t fun i => f i x) s 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 : ΞΉ), i ∈ t β†’ ContMDiffAt I' I n (f i) x) :
                ContMDiffAt I' I n (fun x => 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 : ΞΉ), i ∈ t β†’ ContMDiffAt I' I n (f i) x) :
                ContMDiffAt I' I n (fun x => Finset.prod t fun i => f i x) x
                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 : ΞΉ), i ∈ t β†’ ContMDiffOn I' I n (f i) s) :
                ContMDiffOn I' I n (fun x => 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 : ΞΉ), i ∈ t β†’ ContMDiffOn I' I n (f i) s) :
                ContMDiffOn I' I n (fun x => Finset.prod t fun i => f i x) s
                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 : ΞΉ), i ∈ t β†’ ContMDiff I' I n (f i)) :
                ContMDiff I' I n fun x => 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 : ΞΉ), i ∈ t β†’ ContMDiff I' I n (f i)) :
                ContMDiff I' I n fun x => Finset.prod t fun i => f i 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 : ΞΉ), 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 : ΞΉ), i ∈ t β†’ SmoothWithinAt I' I (f i) s x) :
                SmoothWithinAt I' I (Finset.prod t fun i => f i) 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 : ΞΉ), 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 : ΞΉ), i ∈ t β†’ SmoothAt I' I (f i) x) :
                SmoothAt I' I (Finset.prod t fun i => f i) 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 : ΞΉ), 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 : ΞΉ), i ∈ t β†’ SmoothOn I' I (f i) s) :
                SmoothOn I' I (Finset.prod t fun i => f i) 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 : ΞΉ), 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 : ΞΉ), i ∈ t β†’ Smooth I' I (f i)) :
                Smooth I' I (Finset.prod t fun i => f i)
                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 : ΞΉ), i ∈ t β†’ SmoothWithinAt I' I (f i) s x) :
                SmoothWithinAt I' I (fun x => 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 : ΞΉ), i ∈ t β†’ SmoothWithinAt I' I (f i) s x) :
                SmoothWithinAt I' I (fun x => 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 : ΞΉ), i ∈ t β†’ SmoothAt I' I (f i) x) :
                SmoothAt I' I (fun x => 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 : ΞΉ), i ∈ t β†’ SmoothAt I' I (f i) x) :
                SmoothAt I' I (fun x => 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 : ΞΉ), i ∈ t β†’ SmoothOn I' I (f i) s) :
                SmoothOn I' I (fun x => 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 : ΞΉ), i ∈ t β†’ SmoothOn I' I (f i) s) :
                SmoothOn I' I (fun x => 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 : ΞΉ), i ∈ t β†’ Smooth I' I (f i)) :
                Smooth I' I fun x => 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 : ΞΉ), i ∈ t β†’ Smooth I' I (f i)) :
                Smooth I' I fun x => 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 => βˆ‘αΆ  (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 => ∏ᢠ (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 => βˆ‘αΆ  (i : ΞΉ) (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 => ∏ᢠ (i : ι) (x_1 : p 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 => βˆ‘αΆ  (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 => ∏ᢠ (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 => βˆ‘αΆ  (i : ΞΉ) (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 => ∏ᢠ (i : ι) (x_1 : p i), f i x
                instance hasSmoothAddSelf {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] :
                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 => 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 => 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 => 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 => 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 => 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 => 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 => 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 => 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 => 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 => 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 => 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 => 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 => 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 => 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 => 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 => f x / c