mathlib documentation

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: has_smooth_mul and its additive counterpart has_smooth_add. These structures are general enough to also talk about smooth semigroups.

  1. All smooth algebraic structures on G are Prop-valued classes that extend smooth_manifold_with_corners I G. This way we save users from adding both [smooth_manifold_with_corners I G] and [has_smooth_mul I G] to the assumptions. While many API lemmas hold true without the smooth_manifold_with_corners I G assumption, we're not aware of a mathematically interesting monoid on a topological manifold such that (a) the space is not a smooth_manifold_with_corners; (b) the multiplication is smooth at (a, b) in the charts ext_chart_at I a, ext_chart_at I b, ext_chart_at I (a * b).

  2. Because of model_prod we can't assume, e.g., that a lie_group is modelled on 𝓘(𝕜, E). So, we formulate the definitions and lemmas for any model.

  3. While smoothness of an operation implies its continuity, lemmas like has_continuous_mul_of_smooth can't be instances becausen otherwise Lean would have to search for has_smooth_mul I G with unknown 𝕜, E, H, and I : model_with_corners 𝕜 E H. If users needs [has_continuous_mul G] in a proof about a smooth monoid, then they need to either add [has_continuous_mul G] as an assumption (worse) or use haveI in the proof (better).

@[class]
structure has_smooth_add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) (G : Type u_4) [has_add G] [topological_space G] [charted_space H G] :
Prop

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

Instances of this typeclass
@[class]
structure has_smooth_mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) (G : Type u_4) [has_mul G] [topological_space G] [charted_space H G] :
Prop

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

Instances of this typeclass
theorem smooth_add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) {G : Type u_4} [has_add G] [topological_space G] [charted_space H G] [has_smooth_add I G] :
smooth (I.prod I) I (λ (p : G × G), p.fst + p.snd)
theorem smooth_mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] :
smooth (I.prod I) I (λ (p : G × G), p.fst * p.snd)
theorem has_continuous_add_of_smooth {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) {G : Type u_4} [has_add G] [topological_space G] [charted_space H G] [has_smooth_add 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 has_continuous_mul_of_smooth {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul 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 cont_mdiff_within_at.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_add G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} {s : set M} {x : M} {n : ℕ∞} (hf : cont_mdiff_within_at I' I n f s x) (hg : cont_mdiff_within_at I' I n g s x) :
cont_mdiff_within_at I' I n (f + g) s x
theorem cont_mdiff_within_at.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} {s : set M} {x : M} {n : ℕ∞} (hf : cont_mdiff_within_at I' I n f s x) (hg : cont_mdiff_within_at I' I n g s x) :
cont_mdiff_within_at I' I n (f * g) s x
theorem cont_mdiff_at.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} {x : M} {n : ℕ∞} (hf : cont_mdiff_at I' I n f x) (hg : cont_mdiff_at I' I n g x) :
cont_mdiff_at I' I n (f * g) x
theorem cont_mdiff_at.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_add G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} {x : M} {n : ℕ∞} (hf : cont_mdiff_at I' I n f x) (hg : cont_mdiff_at I' I n g x) :
cont_mdiff_at I' I n (f + g) x
theorem cont_mdiff_on.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} {s : set M} {n : ℕ∞} (hf : cont_mdiff_on I' I n f s) (hg : cont_mdiff_on I' I n g s) :
cont_mdiff_on I' I n (f * g) s
theorem cont_mdiff_on.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_add G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} {s : set M} {n : ℕ∞} (hf : cont_mdiff_on I' I n f s) (hg : cont_mdiff_on I' I n g s) :
cont_mdiff_on I' I n (f + g) s
theorem cont_mdiff.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_add G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} {n : ℕ∞} (hf : cont_mdiff I' I n f) (hg : cont_mdiff I' I n g) :
cont_mdiff I' I n (f + g)
theorem cont_mdiff.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} {n : ℕ∞} (hf : cont_mdiff I' I n f) (hg : cont_mdiff I' I n g) :
cont_mdiff I' I n (f * g)
theorem smooth_within_at.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} {s : set M} {x : M} (hf : smooth_within_at I' I f s x) (hg : smooth_within_at I' I g s x) :
smooth_within_at I' I (f * g) s x
theorem smooth_within_at.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_add G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} {s : set M} {x : M} (hf : smooth_within_at I' I f s x) (hg : smooth_within_at I' I g s x) :
smooth_within_at I' I (f + g) s x
theorem smooth_at.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} {x : M} (hf : smooth_at I' I f x) (hg : smooth_at I' I g x) :
smooth_at I' I (f * g) x
theorem smooth_at.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_add G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} {x : M} (hf : smooth_at I' I f x) (hg : smooth_at I' I g x) :
smooth_at I' I (f + g) x
theorem smooth_on.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} {s : set M} (hf : smooth_on I' I f s) (hg : smooth_on I' I g s) :
smooth_on I' I (f * g) s
theorem smooth_on.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_add G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} {s : set M} (hf : smooth_on I' I f s) (hg : smooth_on I' I g s) :
smooth_on I' I (f + g) s
theorem smooth.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} (hf : smooth I' I f) (hg : smooth I' I g) :
smooth I' I (f * g)
theorem smooth.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_add G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_7} [topological_space M] [charted_space H' M] {f g : M → G} (hf : smooth I' I f) (hg : smooth I' I g) :
smooth I' I (f + g)
theorem smooth_mul_left {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {a : G} :
smooth I I (λ (b : G), a * b)
theorem smooth_add_left {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_add G] [topological_space G] [charted_space H G] [has_smooth_add I G] {a : G} :
smooth I I (λ (b : G), a + b)
theorem smooth_mul_right {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {a : G} :
smooth I I (λ (b : G), b * a)
theorem smooth_add_right {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [has_add G] [topological_space G] [charted_space H G] [has_smooth_add I G] {a : G} :
smooth I I (λ (b : G), b + a)
def smooth_left_mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] (g : G) :

Left multiplication by g. It is meant to mimic the usual notation in Lie groups. Lemmas involving smooth_left_mul with the notation 𝑳 usually use L instead of 𝑳 in the names.

Equations
def smooth_right_mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] (g : G) :

Right multiplication by g. It is meant to mimic the usual notation in Lie groups. Lemmas involving smooth_right_mul with the notation 𝑹 usually use R instead of 𝑹 in the names.

Equations
@[simp]
theorem L_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] (g h : G) :
(smooth_left_mul I g) h = g * h
@[simp]
theorem R_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) {G : Type u_4} [has_mul G] [topological_space G] [charted_space H G] [has_smooth_mul I G] (g h : G) :
(smooth_right_mul I g) h = h * g
@[simp]
theorem L_mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) {G : Type u_4} [semigroup G] [topological_space G] [charted_space H G] [has_smooth_mul I G] (g h : G) :
@[simp]
theorem R_mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) {G : Type u_4} [semigroup G] [topological_space G] [charted_space H G] [has_smooth_mul I G] (g h : G) :
theorem smooth_left_mul_one {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) {G' : Type u_8} [monoid G'] [topological_space G'] [charted_space H G'] [has_smooth_mul I G'] (g' : G') :
(smooth_left_mul I g') 1 = g'
theorem smooth_right_mul_one {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) {G' : Type u_8} [monoid G'] [topological_space G'] [charted_space H G'] [has_smooth_mul I G'] (g' : G') :
@[protected, instance]
def has_smooth_add.sum {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) (G : Type u_4) [topological_space G] [charted_space H G] [has_add G] [has_smooth_add I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') (G' : Type u_7) [topological_space G'] [charted_space H' G'] [has_add G'] [has_smooth_add I' G'] :
has_smooth_add (I.prod I') (G × G')
@[protected, instance]
def has_smooth_mul.prod {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) (G : Type u_4) [topological_space G] [charted_space H G] [has_mul G] [has_smooth_mul I G] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') (G' : Type u_7) [topological_space G'] [charted_space H' G'] [has_mul G'] [has_smooth_mul I' G'] :
has_smooth_mul (I.prod I') (G × G')
theorem smooth_pow {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] (n : ) :
smooth I I (λ (a : G), a ^ n)
structure smooth_add_monoid_morphism {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {H' : Type u_5} [topological_space H'] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] (I : model_with_corners 𝕜 E H) (I' : model_with_corners 𝕜 E' H') (G : Type u_8) [topological_space G] [charted_space H G] [add_monoid G] [has_smooth_add I G] (G' : Type u_9) [topological_space G'] [charted_space H' G'] [add_monoid G'] [has_smooth_add I' G'] :
Type (max u_8 u_9)

Morphism of additive smooth monoids.

Instances for smooth_add_monoid_morphism
structure smooth_monoid_morphism {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {H' : Type u_5} [topological_space H'] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] (I : model_with_corners 𝕜 E H) (I' : model_with_corners 𝕜 E' H') (G : Type u_8) [topological_space G] [charted_space H G] [monoid G] [has_smooth_mul I G] (G' : Type u_9) [topological_space G'] [charted_space H' G'] [monoid G'] [has_smooth_mul I' G'] :
Type (max u_8 u_9)

Morphism of smooth monoids.

Instances for smooth_monoid_morphism
@[protected, instance]
def smooth_add_monoid_morphism.has_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [add_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {H' : Type u_5} [topological_space H'] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {I' : model_with_corners 𝕜 E' H'} {G' : Type u_7} [add_monoid G'] [topological_space G'] [charted_space H' G'] [has_smooth_add I' G'] :
Equations
@[protected, instance]
def smooth_monoid_morphism.has_one {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {H' : Type u_5} [topological_space H'] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {I' : model_with_corners 𝕜 E' H'} {G' : Type u_7} [monoid G'] [topological_space G'] [charted_space H' G'] [has_smooth_mul I' G'] :
Equations
@[protected, instance]
def smooth_add_monoid_morphism.inhabited {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [add_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {H' : Type u_5} [topological_space H'] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {I' : model_with_corners 𝕜 E' H'} {G' : Type u_7} [add_monoid G'] [topological_space G'] [charted_space H' G'] [has_smooth_add I' G'] :
Equations
@[protected, instance]
def smooth_monoid_morphism.inhabited {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {H' : Type u_5} [topological_space H'] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {I' : model_with_corners 𝕜 E' H'} {G' : Type u_7} [monoid G'] [topological_space G'] [charted_space H' G'] [has_smooth_mul I' G'] :
Equations
@[protected, instance]
def smooth_add_monoid_morphism.has_coe_to_fun {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [add_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {H' : Type u_5} [topological_space H'] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {I' : model_with_corners 𝕜 E' H'} {G' : Type u_7} [add_monoid G'] [topological_space G'] [charted_space H' G'] [has_smooth_add I' G'] :
has_coe_to_fun (smooth_add_monoid_morphism I I' G G') (λ (_x : smooth_add_monoid_morphism I I' G G'), G → G')
Equations
@[protected, instance]
def smooth_monoid_morphism.has_coe_to_fun {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_4} [monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {H' : Type u_5} [topological_space H'] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {I' : model_with_corners 𝕜 E' H'} {G' : Type u_7} [monoid G'] [topological_space G'] [charted_space H' G'] [has_smooth_mul I' G'] :
has_coe_to_fun (smooth_monoid_morphism I I' G G') (λ (_x : smooth_monoid_morphism I I' G G'), G → G')
Equations
theorem cont_mdiff_within_at_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff_within_at I' I n (f i) s x) :
cont_mdiff_within_at I' I n (t.prod (λ (i : ι), f i)) s x
theorem cont_mdiff_within_at_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff_within_at I' I n (f i) s x) :
cont_mdiff_within_at I' I n (t.sum (λ (i : ι), f i)) s x
theorem cont_mdiff_at_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff_at I' I n (f i) x) :
cont_mdiff_at I' I n (t.prod (λ (i : ι), f i)) x
theorem cont_mdiff_at_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff_at I' I n (f i) x) :
cont_mdiff_at I' I n (t.sum (λ (i : ι), f i)) x
theorem cont_mdiff_on_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff_on I' I n (f i) s) :
cont_mdiff_on I' I n (t.prod (λ (i : ι), f i)) s
theorem cont_mdiff_on_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff_on I' I n (f i) s) :
cont_mdiff_on I' I n (t.sum (λ (i : ι), f i)) s
theorem cont_mdiff_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff I' I n (f i)) :
cont_mdiff I' I n (t.sum (λ (i : ι), f i))
theorem cont_mdiff_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff I' I n (f i)) :
cont_mdiff I' I n (t.prod (λ (i : ι), f i))
theorem cont_mdiff_within_at_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff_within_at I' I n (f i) s x) :
cont_mdiff_within_at I' I n (λ (x : M), t.sum (λ (i : ι), f i x)) s x
theorem cont_mdiff_within_at_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff_within_at I' I n (f i) s x) :
cont_mdiff_within_at I' I n (λ (x : M), t.prod (λ (i : ι), f i x)) s x
theorem cont_mdiff_at_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff_at I' I n (f i) x) :
cont_mdiff_at I' I n (λ (x : M), t.sum (λ (i : ι), f i x)) x
theorem cont_mdiff_at_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {x : M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff_at I' I n (f i) x) :
cont_mdiff_at I' I n (λ (x : M), t.prod (λ (i : ι), f i x)) x
theorem cont_mdiff_on_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff_on I' I n (f i) s) :
cont_mdiff_on I' I n (λ (x : M), t.sum (λ (i : ι), f i x)) s
theorem cont_mdiff_on_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff_on I' I n (f i) s) :
cont_mdiff_on I' I n (λ (x : M), t.prod (λ (i : ι), f i x)) s
theorem cont_mdiff_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff I' I n (f i)) :
cont_mdiff I' I n (λ (x : M), t.sum (λ (i : ι), f i x))
theorem cont_mdiff_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {t : finset ι} {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), i tcont_mdiff I' I n (f i)) :
cont_mdiff I' I n (λ (x : M), t.prod (λ (i : ι), f i x))
theorem smooth_within_at_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth_within_at I' I (f i) s x) :
smooth_within_at I' I (t.prod (λ (i : ι), f i)) s x
theorem smooth_within_at_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth_within_at I' I (f i) s x) :
smooth_within_at I' I (t.sum (λ (i : ι), f i)) s x
theorem smooth_at_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth_at I' I (f i) x) :
smooth_at I' I (t.sum (λ (i : ι), f i)) x
theorem smooth_at_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth_at I' I (f i) x) :
smooth_at I' I (t.prod (λ (i : ι), f i)) x
theorem smooth_on_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth_on I' I (f i) s) :
smooth_on I' I (t.sum (λ (i : ι), f i)) s
theorem smooth_on_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth_on I' I (f i) s) :
smooth_on I' I (t.prod (λ (i : ι), f i)) s
theorem smooth_finset_sum' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth I' I (f i)) :
smooth I' I (t.sum (λ (i : ι), f i))
theorem smooth_finset_prod' {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth I' I (f i)) :
smooth I' I (t.prod (λ (i : ι), f i))
theorem smooth_within_at_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth_within_at I' I (f i) s x) :
smooth_within_at I' I (λ (x : M), t.sum (λ (i : ι), f i x)) s x
theorem smooth_within_at_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth_within_at I' I (f i) s x) :
smooth_within_at I' I (λ (x : M), t.prod (λ (i : ι), f i x)) s x
theorem smooth_at_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth_at I' I (f i) x) :
smooth_at I' I (λ (x : M), t.sum (λ (i : ι), f i x)) x
theorem smooth_at_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {x : M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth_at I' I (f i) x) :
smooth_at I' I (λ (x : M), t.prod (λ (i : ι), f i x)) x
theorem smooth_on_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth_on I' I (f i) s) :
smooth_on I' I (λ (x : M), t.sum (λ (i : ι), f i x)) s
theorem smooth_on_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {s : set M} {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth_on I' I (f i) s) :
smooth_on I' I (λ (x : M), t.prod (λ (i : ι), f i x)) s
theorem smooth_finset_prod {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth I' I (f i)) :
smooth I' I (λ (x : M), t.prod (λ (i : ι), f i x))
theorem smooth_finset_sum {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {t : finset ι} {f : ι → M → G} (h : ∀ (i : ι), i tsmooth I' I (f i)) :
smooth I' I (λ (x : M), t.sum (λ (i : ι), f i x))
theorem cont_mdiff_finsum {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), cont_mdiff I' I n (f i)) (hfin : locally_finite (λ (i : ι), function.support (f i))) :
cont_mdiff I' I n (λ (x : M), finsum (λ (i : ι), f i x))
theorem cont_mdiff_finprod {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {f : ι → M → G} {n : ℕ∞} (h : ∀ (i : ι), cont_mdiff I' I n (f i)) (hfin : locally_finite (λ (i : ι), function.mul_support (f i))) :
cont_mdiff I' I n (λ (x : M), finprod (λ (i : ι), f i x))
theorem cont_mdiff_finprod_cond {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {f : ι → M → G} {n : ℕ∞} {p : ι → Prop} (hc : ∀ (i : ι), p icont_mdiff I' I n (f i)) (hf : locally_finite (λ (i : ι), function.mul_support (f i))) :
cont_mdiff I' I n (λ (x : M), finprod (λ (i : ι), finprod (λ (hi : p i), f i x)))
theorem cont_mdiff_finsum_cond {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {f : ι → M → G} {n : ℕ∞} {p : ι → Prop} (hc : ∀ (i : ι), p icont_mdiff I' I n (f i)) (hf : locally_finite (λ (i : ι), function.support (f i))) :
cont_mdiff I' I n (λ (x : M), finsum (λ (i : ι), finsum (λ (hi : p i), f i x)))
theorem smooth_finprod {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {f : ι → M → G} (h : ∀ (i : ι), smooth I' I (f i)) (hfin : locally_finite (λ (i : ι), function.mul_support (f i))) :
smooth I' I (λ (x : M), finprod (λ (i : ι), f i x))
theorem smooth_finsum {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {f : ι → M → G} (h : ∀ (i : ι), smooth I' I (f i)) (hfin : locally_finite (λ (i : ι), function.support (f i))) :
smooth I' I (λ (x : M), finsum (λ (i : ι), f i x))
theorem smooth_finsum_cond {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [add_comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_add I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {f : ι → M → G} {p : ι → Prop} (hc : ∀ (i : ι), p ismooth I' I (f i)) (hf : locally_finite (λ (i : ι), function.support (f i))) :
smooth I' I (λ (x : M), finsum (λ (i : ι), finsum (λ (hi : p i), f i x)))
theorem smooth_finprod_cond {ι : Type u_1} {𝕜 : Type u_2} [nontrivially_normed_field 𝕜] {H : Type u_3} [topological_space H] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {G : Type u_5} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G] {E' : Type u_6} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_7} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M : Type u_8} [topological_space M] [charted_space H' M] {f : ι → M → G} {p : ι → Prop} (hc : ∀ (i : ι), p ismooth I' I (f i)) (hf : locally_finite (λ (i : ι), function.mul_support (f i))) :
smooth I' I (λ (x : M), finprod (λ (i : ι), finprod (λ (hi : p i), f i x)))