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.
-
All smooth algebraic structures on
GareProp-valued classes that extendsmooth_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 thesmooth_manifold_with_corners I Gassumption, we're not aware of a mathematically interesting monoid on a topological manifold such that (a) the space is not asmooth_manifold_with_corners; (b) the multiplication is smooth at(a, b)in the chartsext_chart_at I a,ext_chart_at I b,ext_chart_at I (a * b). -
Because of
model_prodwe can't assume, e.g., that alie_groupis modelled on𝓘(𝕜, E). So, we formulate the definitions and lemmas for any model. -
While smoothness of an operation implies its continuity, lemmas like
has_continuous_mul_of_smoothcan't be instances becausen otherwise Lean would have to search forhas_smooth_mul I Gwith unknown𝕜,E,H, andI : 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 usehaveIin 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
- to_smooth_manifold_with_corners : smooth_manifold_with_corners I G
- 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 α.
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
- to_smooth_manifold_with_corners : smooth_manifold_with_corners I G
- 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.
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] :
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] :
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) :
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) :
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) :
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) :
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) :
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) :
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} :
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} :
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} :
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} :
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) :
cont_mdiff_map I I 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
- smooth_left_mul I g = {to_fun := left_mul g, cont_mdiff_to_fun := _}
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) :
cont_mdiff_map I I 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
- smooth_right_mul I g = {to_fun := right_mul g, cont_mdiff_to_fun := _}
@[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) :
smooth_left_mul I (g * h) = (smooth_left_mul I g).comp (smooth_left_mul I h)
@[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) :
smooth_right_mul I (g * h) = (smooth_right_mul I h).comp (smooth_right_mul I 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') :
⇑(smooth_right_mul I g') 1 = 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 : ℕ) :
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)
- to_add_monoid_hom : G →+ G'
- smooth_to_fun : smooth I I' self.to_add_monoid_hom.to_fun
Morphism of additive smooth monoids.
Instances for smooth_add_monoid_morphism
- smooth_add_monoid_morphism.has_sizeof_inst
- smooth_add_monoid_morphism.has_zero
- smooth_add_monoid_morphism.inhabited
- smooth_add_monoid_morphism.has_coe_to_fun
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)
- to_monoid_hom : G →* G'
- smooth_to_fun : smooth I I' self.to_monoid_hom.to_fun
Morphism of smooth monoids.
Instances for smooth_monoid_morphism
- smooth_monoid_morphism.has_sizeof_inst
- smooth_monoid_morphism.has_one
- smooth_monoid_morphism.inhabited
- smooth_monoid_morphism.has_coe_to_fun
@[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'] :
has_zero (smooth_add_monoid_morphism I I' G G')
Equations
- smooth_add_monoid_morphism.has_zero = {zero := {to_add_monoid_hom := 0, smooth_to_fun := _}}
@[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'] :
has_one (smooth_monoid_morphism I I' G G')
Equations
- smooth_monoid_morphism.has_one = {one := {to_monoid_hom := 1, smooth_to_fun := _}}
@[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'] :
inhabited (smooth_add_monoid_morphism I I' G 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'] :
inhabited (smooth_monoid_morphism I I' G 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
- smooth_add_monoid_morphism.has_coe_to_fun = {coe := λ (a : smooth_add_monoid_morphism I I' G G'), a.to_add_monoid_hom.to_fun}
@[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
- smooth_monoid_morphism.has_coe_to_fun = {coe := λ (a : smooth_monoid_morphism I I' G G'), a.to_monoid_hom.to_fun}
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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → cont_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 ∈ t → smooth_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 ∈ t → smooth_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 ∈ t → smooth_at I' 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 ∈ t → smooth_at I' 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 ∈ t → smooth_on I' 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 ∈ t → smooth_on I' 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 ∈ t → smooth I' 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 ∈ t → smooth I' 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 ∈ t → smooth_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 ∈ t → smooth_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 ∈ t → smooth_at I' 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 ∈ t → smooth_at I' 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 ∈ t → smooth_on I' 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 ∈ t → smooth_on I' I (f i) 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 ∈ t → smooth I' I (f i)) :
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 ∈ t → smooth I' I (f i)) :
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 i → cont_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 i → cont_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))) :
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))) :
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 i → smooth I' I (f i))
(hf : locally_finite (λ (i : ι), function.support (f i))) :
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 i → smooth I' I (f i))
(hf : locally_finite (λ (i : ι), function.mul_support (f i))) :