# 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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] (I : ModelWithCorners π E H) (G : Type u_4) [Add G] [] [] extends :

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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Add G] [] [] [self : ] :
Smooth (I.prod I) I fun (p : G Γ G) => p.1 + p.2
class SmoothMul {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] (I : ModelWithCorners π E H) (G : Type u_4) [Mul G] [] [] extends :

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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Mul G] [] [] [self : ] :
Smooth (I.prod I) I fun (p : G Γ G) => p.1 * p.2
theorem smooth_add {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] (I : ModelWithCorners π E H) {G : Type u_4} [Add G] [] [] [] :
Smooth (I.prod I) I fun (p : G Γ G) => p.1 + p.2
theorem smooth_mul {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] (I : ModelWithCorners π E H) {G : Type u_4} [Mul G] [] [] [] :
Smooth (I.prod I) I fun (p : G Γ G) => p.1 * p.2
theorem continuousAdd_of_smooth {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] (I : ModelWithCorners π E H) {G : Type u_4} [Add 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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] (I : ModelWithCorners π E H) {G : Type u_4} [Mul 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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Add G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Mul G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Add G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Mul G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Add G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Mul G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Add G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Mul G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Add G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Mul G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Add G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Mul G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Add G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Mul G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Add G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Mul G] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Add G] [] [] [] {a : G} :
Smooth I I fun (b : G) => a + b
theorem smooth_mul_left {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Mul G] [] [] [] {a : G} :
Smooth I I fun (b : G) => a * b
theorem smooth_add_right {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Add G] [] [] [] {a : G} :
Smooth I I fun (b : G) => b + a
theorem smooth_mul_right {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [Mul G] [] [] [] {a : G} :
Smooth I I fun (b : G) => b * a
def smoothLeftMul {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] (I : ModelWithCorners π E H) {G : Type u_4} [Mul 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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] (I : ModelWithCorners π E H) {G : Type u_4} [Mul 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
Equations
Instances For
Equations
Instances For
@[simp]
theorem L_apply {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] (I : ModelWithCorners π E H) {G : Type u_4} [Mul G] [] [] [] (g : G) (h : G) :
() h = g * h
@[simp]
theorem R_apply {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] (I : ModelWithCorners π E H) {G : Type u_4} [Mul G] [] [] [] (g : G) (h : G) :
() h = h * g
@[simp]
theorem L_mul {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] (I : ModelWithCorners π E H) {G : Type u_8} [] [] [] [] (g : G) (h : G) :
smoothLeftMul I (g * h) = ().comp ()
@[simp]
theorem R_mul {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] (I : ModelWithCorners π E H) {G : Type u_8} [] [] [] [] (g : G) (h : G) :
smoothRightMul I (g * h) = ().comp ()
theorem smoothLeftMul_one {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] (I : ModelWithCorners π E H) {G' : Type u_8} [Monoid G'] [] [ChartedSpace H G'] [SmoothMul I G'] (g' : G') :
() 1 = g'
theorem smoothRightMul_one {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] (I : ModelWithCorners π E H) {G' : Type u_8} [Monoid G'] [] [ChartedSpace H G'] [SmoothMul I G'] (g' : G') :
() 1 = g'
instance SmoothAdd.sum {π : Type u_8} [] {E : Type u_9} [NormedSpace π E] {H : Type u_10} [] (I : ModelWithCorners π E H) (G : Type u_11) [] [] [Add G] [] {E' : Type u_12} [] [NormedSpace π E'] {H' : Type u_13} [] (I' : ModelWithCorners π E' H') (G' : Type u_14) [] [ChartedSpace H' G'] [Add G'] [SmoothAdd I' G'] :
SmoothAdd (I.prod I') (G Γ G')
Equations
• β― = β―
instance SmoothMul.prod {π : Type u_8} [] {E : Type u_9} [NormedSpace π E] {H : Type u_10} [] (I : ModelWithCorners π E H) (G : Type u_11) [] [] [Mul G] [] {E' : Type u_12} [] [NormedSpace π E'] {H' : Type u_13} [] (I' : ModelWithCorners π E' H') (G' : Type u_14) [] [ChartedSpace H' G'] [Mul G'] [SmoothMul I' G'] :
SmoothMul (I.prod I') (G Γ G')
Equations
• β― = β―
theorem smooth_nsmul {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] (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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] (n : β) :
Smooth I I fun (a : G) => a ^ n
structure SmoothAddMonoidMorphism {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {H' : Type u_5} [] {E' : Type u_6} [] [NormedSpace π E'] (I : ModelWithCorners π E H) (I' : ModelWithCorners π E' H') (G : Type u_8) [] [] [] [] (G' : Type u_9) [] [ChartedSpace H' G'] [] [SmoothAdd I' G'] extends :
Type (max u_8 u_9)

• toFun : G β G'
• map_zero' : (βself.toAddMonoidHom).toFun 0 = 0
• smooth_toFun : Smooth I I' (βself.toAddMonoidHom).toFun
Instances For
theorem SmoothAddMonoidMorphism.smooth_toFun {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {H' : Type u_5} [] {E' : Type u_6} [] [NormedSpace π E'] {I : ModelWithCorners π E H} {I' : ModelWithCorners π E' H'} {G : Type u_8} [] [] [] [] {G' : Type u_9} [] [ChartedSpace H' G'] [] [SmoothAdd I' G'] (self : SmoothAddMonoidMorphism I I' G G') :
structure SmoothMonoidMorphism {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {H' : Type u_5} [] {E' : Type u_6} [] [NormedSpace π E'] (I : ModelWithCorners π E H) (I' : ModelWithCorners π E' H') (G : Type u_8) [] [] [] [] (G' : Type u_9) [] [ChartedSpace H' G'] [Monoid G'] [SmoothMul I' G'] extends :
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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {H' : Type u_5} [] {E' : Type u_6} [] [NormedSpace π E'] {I : ModelWithCorners π E H} {I' : ModelWithCorners π E' H'} {G : Type u_8} [] [] [] [] {G' : Type u_9} [] [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} [] {H : Type u_5} [] {E : Type u_6} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] {H' : Type u_2} [] {E' : Type u_3} [] [NormedSpace π E'] {I' : ModelWithCorners π E' H'} {G' : Type u_1} [] [] [ChartedSpace H' G'] :
Smooth I I' fun (x : G) => AddZeroClass.toZero.1
instance instZeroSmoothAddMonoidMorphism {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {H' : Type u_5} [] {E' : Type u_6} [] [NormedSpace π E'] {I' : ModelWithCorners π E' H'} {G' : Type u_7} [] [] [ChartedSpace H' G'] [SmoothAdd I' G'] :
Equations
• instZeroSmoothAddMonoidMorphism = { zero := { toAddMonoidHom := 0, smooth_toFun := β― } }
instance instOneSmoothMonoidMorphism {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {H' : Type u_5} [] {E' : Type u_6} [] [NormedSpace π E'] {I' : ModelWithCorners π E' H'} {G' : Type u_7} [Monoid G'] [] [ChartedSpace H' G'] [SmoothMul I' G'] :
Equations
• instOneSmoothMonoidMorphism = { one := { toMonoidHom := 1, smooth_toFun := β― } }
instance instInhabitedSmoothAddMonoidMorphism {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {H' : Type u_5} [] {E' : Type u_6} [] [NormedSpace π E'] {I' : ModelWithCorners π E' H'} {G' : Type u_7} [] [] [ChartedSpace H' G'] [SmoothAdd I' G'] :
Equations
• instInhabitedSmoothAddMonoidMorphism = { default := 0 }
instance instInhabitedSmoothMonoidMorphism {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {H' : Type u_5} [] {E' : Type u_6} [] [NormedSpace π E'] {I' : ModelWithCorners π E' H'} {G' : Type u_7} [Monoid G'] [] [ChartedSpace H' G'] [SmoothMul I' G'] :
Equations
• instInhabitedSmoothMonoidMorphism = { default := 1 }
instance instFunLikeSmoothAddMonoidMorphism {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {H' : Type u_5} [] {E' : Type u_6} [] [NormedSpace π E'] {I' : ModelWithCorners π E' H'} {G' : Type u_7} [] [] [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} [] {H : Type u_6} [] {E : Type u_5} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_2} [] [] [] [] {H' : Type u_4} [] {E' : Type u_3} [] [NormedSpace π E'] {I' : ModelWithCorners π E' H'} {G' : Type u_1} [] [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {H' : Type u_5} [] {E' : Type u_6} [] [NormedSpace π E'] {I' : ModelWithCorners π E' H'} {G' : Type u_7} [Monoid 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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {H' : Type u_5} [] {E' : Type u_6} [] [NormedSpace π E'] {I' : ModelWithCorners π E' H'} {G' : Type u_7} [] [] [ChartedSpace H' G'] [SmoothAdd I' G'] :
Equations
• β― = β―
instance instMonoidHomClassSmoothMonoidMorphism {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {H' : Type u_5} [] {E' : Type u_6} [] [NormedSpace π E'] {I' : ModelWithCorners π E' H'} {G' : Type u_7} [Monoid G'] [] [ChartedSpace H' G'] [SmoothMul I' G'] :
Equations
• β― = β―
instance instContinuousMapClassSmoothAddMonoidMorphism {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {H' : Type u_5} [] {E' : Type u_6} [] [NormedSpace π E'] {I' : ModelWithCorners π E' H'} {G' : Type u_7} [] [] [ChartedSpace H' G'] [SmoothAdd I' G'] :
Equations
• β― = β―
instance instContinuousMapClassSmoothMonoidMorphism {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {H' : Type u_5} [] {E' : Type u_6} [] [NormedSpace π E'] {I' : ModelWithCorners π E' H'} {G' : Type u_7} [Monoid 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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {M : Type u_2} [] {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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {H : Type u_3} [] {E : Type u_4} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_5} [] [] [] [] {E' : Type u_6} [] [NormedSpace π E'] {H' : Type u_7} [] {I' : ModelWithCorners π E' H'} {M : Type u_8} [] [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} [] {E : Type u_2} [NormedSpace π E] :
Equations
• β― = β―
theorem ContMDiffWithinAt.sub_const {π : Type u_1} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [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} [] {H : Type u_2} [] {E : Type u_3} [NormedSpace π E] {I : ModelWithCorners π E H} {G : Type u_4} [] [] [] [] {E' : Type u_5} [] [NormedSpace π E'] {H' : Type u_6} [] {I' : ModelWithCorners π E' H'} {M : Type u_7} [] [ChartedSpace H' M] {f : M β G} (c : G) (hf : Smooth I' I f) :
Smooth I' I fun (x : M) => f x / c