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.
@[class]
structure
has_smooth_add
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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
- compatible : ∀ {e e' : local_homeomorph G H}, e ∈ atlas H G → e' ∈ atlas H G → e.symm ≫ₕ e' ∈ times_cont_diff_groupoid ⊤ I
- smooth_add : smooth (I.prod I) I (λ (p : G × G), p.fst + p.snd)
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 α.
@[instance]
def
has_smooth_add.to_smooth_manifold_with_corners
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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]
[self : has_smooth_add I G] :
@[class]
structure
has_smooth_mul
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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
- compatible : ∀ {e e' : local_homeomorph G H}, e ∈ atlas H G → e' ∈ atlas H G → e.symm ≫ₕ e' ∈ times_cont_diff_groupoid ⊤ I
- smooth_mul : smooth (I.prod I) I (λ (p : G × G), (p.fst) * p.snd)
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.
@[instance]
def
has_smooth_mul.to_smooth_manifold_with_corners
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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]
[self : has_smooth_mul I G] :
theorem
smooth_add
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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] :
theorem
smooth_mul
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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] :
theorem
has_continuous_add_of_smooth
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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
smooth.mul
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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_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) :
theorem
smooth.add
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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_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) :
theorem
smooth_mul_left
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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} :
theorem
smooth_add_left
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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} :
theorem
smooth_mul_right
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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} :
theorem
smooth_add_right
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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} :
theorem
smooth_on.mul
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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_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) :
theorem
smooth_on.add
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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_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) :
@[instance]
def
has_smooth_add.sum
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_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_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')
@[instance]
def
has_smooth_mul.prod
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_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_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}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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 : ℕ) :
structure
smooth_add_monoid_morphism
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{H' : Type u_5}
[topological_space H']
{E' : Type u_6}
[normed_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)
- to_add_monoid_hom : G →+ G'
- smooth_to_fun : smooth I I' c.to_add_monoid_hom.to_fun
Morphism of additive smooth monoids.
structure
smooth_monoid_morphism
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{H' : Type u_5}
[topological_space H']
{E' : Type u_6}
[normed_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)
- to_monoid_hom : G →* G'
- smooth_to_fun : smooth I I' c.to_monoid_hom.to_fun
Morphism of smooth monoids.
@[instance]
def
smooth_add_monoid_morphism.has_zero
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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_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_zero (smooth_add_monoid_morphism I I' G G')
@[instance]
def
smooth_monoid_morphism.has_one
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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_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_one (smooth_monoid_morphism I I' G G')
Equations
- smooth_monoid_morphism.has_one = {one := {to_monoid_hom := 1, smooth_to_fun := _}}
@[instance]
def
smooth_add_monoid_morphism.inhabited
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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_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'] :
inhabited (smooth_add_monoid_morphism I I' G G')
@[instance]
def
smooth_monoid_morphism.inhabited
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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_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'] :
inhabited (smooth_monoid_morphism I I' G G')
Equations
@[instance]
def
smooth_add_monoid_morphism.has_coe_to_fun
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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_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')
@[instance]
def
smooth_monoid_morphism.has_coe_to_fun
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_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_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')
Equations
- smooth_monoid_morphism.has_coe_to_fun = {F := λ (a : smooth_monoid_morphism I I' G G'), G → G', coe := λ (a : smooth_monoid_morphism I I' G G'), a.to_monoid_hom.to_fun}
theorem
smooth_finset_sum'
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[add_comm_monoid G]
[topological_space G]
[charted_space H G]
[has_smooth_add I G]
{E' : Type u_5}
[normed_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]
{ι : Type u_8}
{s : finset ι}
{f : ι → M → G}
(h : ∀ (i : ι), i ∈ s → smooth I' I (f i)) :
smooth I' I (∑ (i : ι) in s, f i)
theorem
smooth_finset_prod'
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[comm_monoid G]
[topological_space G]
[charted_space H G]
[has_smooth_mul I G]
{E' : Type u_5}
[normed_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]
{ι : Type u_8}
{s : finset ι}
{f : ι → M → G}
(h : ∀ (i : ι), i ∈ s → smooth I' I (f i)) :
smooth I' I (∏ (i : ι) in s, f i)
theorem
smooth_finset_prod
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[comm_monoid G]
[topological_space G]
[charted_space H G]
[has_smooth_mul I G]
{E' : Type u_5}
[normed_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]
{ι : Type u_8}
{s : finset ι}
{f : ι → M → G}
(h : ∀ (i : ι), i ∈ s → smooth I' I (f i)) :
smooth I' I (λ (x : M), ∏ (i : ι) in s, f i x)
theorem
smooth_finset_sum
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[add_comm_monoid G]
[topological_space G]
[charted_space H G]
[has_smooth_add I G]
{E' : Type u_5}
[normed_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]
{ι : Type u_8}
{s : finset ι}
{f : ι → M → G}
(h : ∀ (i : ι), i ∈ s → smooth I' I (f i)) :
smooth I' I (λ (x : M), ∑ (i : ι) in s, f i x)
theorem
smooth_finprod
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[comm_monoid G]
[topological_space G]
[charted_space H G]
[has_smooth_mul I G]
{E' : Type u_5}
[normed_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]
{ι : Type u_8}
{f : ι → M → G}
(h : ∀ (i : ι), smooth I' I (f i))
(hfin : locally_finite (λ (i : ι), function.mul_support (f i))) :
smooth I' I (λ (x : M), ∏ᶠ (i : ι), f i x)
theorem
smooth_finsum
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[add_comm_monoid G]
[topological_space G]
[charted_space H G]
[has_smooth_add I G]
{E' : Type u_5}
[normed_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]
{ι : Type u_8}
{f : ι → M → G}
(h : ∀ (i : ι), smooth I' I (f i))
(hfin : locally_finite (λ (i : ι), function.support (f i))) :
smooth I' I (λ (x : M), ∑ᶠ (i : ι), f i x)
theorem
smooth_finsum_cond
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[add_comm_monoid G]
[topological_space G]
[charted_space H G]
[has_smooth_add I G]
{E' : Type u_5}
[normed_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]
{ι : Type u_8}
{f : ι → M → G}
{p : ι → Prop}
(hc : ∀ (i : ι), p i → smooth I' I (f i))
(hf : locally_finite (λ (i : ι), function.support (f i))) :
smooth I' I (λ (x : M), ∑ᶠ (i : ι) (hi : p i), f i x)
theorem
smooth_finprod_cond
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
{I : model_with_corners 𝕜 E H}
{G : Type u_4}
[comm_monoid G]
[topological_space G]
[charted_space H G]
[has_smooth_mul I G]
{E' : Type u_5}
[normed_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]
{ι : Type u_8}
{f : ι → M → G}
{p : ι → Prop}
(hc : ∀ (i : ι), p i → smooth I' I (f i))
(hf : locally_finite (λ (i : ι), function.mul_support (f i))) :
smooth I' I (λ (x : M), ∏ᶠ (i : ι) (hi : p i), f i x)