Lie groups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A Lie group is a group that is also a smooth manifold, in which the group operations of
multiplication and inversion are smooth maps. Smoothness of the group multiplication means that
multiplication is a smooth mapping of the product manifold G × G into G.
Note that, since a manifold here is not second-countable and Hausdorff a Lie group here is not guaranteed to be second-countable (even though it can be proved it is Hausdorff). Note also that Lie groups here are not necessarily finite dimensional.
Main definitions and statements #
lie_add_group I G: a Lie additive group whereGis a manifold on the model with cornersI.lie_group I G: a Lie multiplicative group whereGis a manifold on the model with cornersI.normed_space_lie_add_group: a normed vector space over a nontrivially normed field is an additive Lie group.
Implementation notes #
A priori, a Lie group here is a manifold with corners.
The definition of Lie group cannot require I : model_with_corners 𝕜 E E with the same space as the
model space and as the model vector space, as one might hope, beause in the product situation,
the model space is model_prod E E' and the model vector space is E × E', which are not the same,
so the definition does not apply. Hence the definition should be more general, allowing
I : model_with_corners 𝕜 E H.
@[class]
structure
lie_add_group
{𝕜 : 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_group G]
[topological_space G]
[charted_space H G] :
Prop
- to_has_smooth_add : has_smooth_add I G
- smooth_neg : smooth I I (λ (a : G), -a)
A Lie (additive) group is a group and a smooth manifold at the same time in which the addition and negation operations are smooth.
Instances of this typeclass
@[class]
structure
lie_group
{𝕜 : 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)
[group G]
[topological_space G]
[charted_space H G] :
Prop
- to_has_smooth_mul : has_smooth_mul I G
- smooth_inv : smooth I I (λ (a : G), a⁻¹)
A Lie group is a group and a smooth manifold at the same time in which the multiplication and inverse operations are smooth.
Instances of this typeclass
theorem
smooth_inv
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group I G] :
theorem
smooth_neg
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group I G] :
theorem
topological_add_group_of_lie_add_group
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group I G] :
An additive Lie group is an additive topological group. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].
theorem
topological_group_of_lie_group
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group I G] :
A Lie group is a topological group. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].
theorem
cont_mdiff_within_at.neg
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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]
{n : ℕ∞}
{f : M → G}
{s : set M}
{x₀ : M}
(hf : cont_mdiff_within_at I' I n f s x₀) :
cont_mdiff_within_at I' I n (λ (x : M), -f x) s x₀
theorem
cont_mdiff_within_at.inv
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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]
{n : ℕ∞}
{f : M → G}
{s : set M}
{x₀ : M}
(hf : cont_mdiff_within_at I' I n f s x₀) :
cont_mdiff_within_at I' I n (λ (x : M), (f x)⁻¹) s x₀
theorem
cont_mdiff_at.inv
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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]
{n : ℕ∞}
{f : M → G}
{x₀ : M}
(hf : cont_mdiff_at I' I n f x₀) :
cont_mdiff_at I' I n (λ (x : M), (f x)⁻¹) x₀
theorem
cont_mdiff_at.neg
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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]
{n : ℕ∞}
{f : M → G}
{x₀ : M}
(hf : cont_mdiff_at I' I n f x₀) :
cont_mdiff_at I' I n (λ (x : M), -f x) x₀
theorem
cont_mdiff_on.neg
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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]
{n : ℕ∞}
{f : M → G}
{s : set M}
(hf : cont_mdiff_on I' I n f s) :
cont_mdiff_on I' I n (λ (x : M), -f x) s
theorem
cont_mdiff_on.inv
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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]
{n : ℕ∞}
{f : M → G}
{s : set M}
(hf : cont_mdiff_on I' I n f s) :
cont_mdiff_on I' I n (λ (x : M), (f x)⁻¹) s
theorem
cont_mdiff.inv
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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]
{n : ℕ∞}
{f : M → G}
(hf : cont_mdiff I' I n f) :
cont_mdiff I' I n (λ (x : M), (f x)⁻¹)
theorem
cont_mdiff.neg
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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]
{n : ℕ∞}
{f : M → G}
(hf : cont_mdiff I' I n f) :
cont_mdiff I' I n (λ (x : M), -f x)
theorem
smooth_within_at.inv
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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}
{s : set M}
{x₀ : M}
(hf : smooth_within_at I' I f s x₀) :
smooth_within_at I' I (λ (x : M), (f x)⁻¹) s x₀
theorem
smooth_within_at.neg
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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}
{s : set M}
{x₀ : M}
(hf : smooth_within_at I' I f s x₀) :
smooth_within_at I' I (λ (x : M), -f x) s x₀
theorem
smooth_at.inv
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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}
{x₀ : M}
(hf : smooth_at I' I f x₀) :
theorem
smooth_at.neg
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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}
{x₀ : M}
(hf : smooth_at I' I f x₀) :
theorem
smooth_on.neg
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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}
{s : set M}
(hf : smooth_on I' I f s) :
theorem
smooth_on.inv
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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}
{s : set M}
(hf : smooth_on I' I f s) :
theorem
smooth.inv
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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}
(hf : smooth I' I f) :
theorem
smooth.neg
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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}
(hf : smooth I' I f) :
theorem
cont_mdiff_within_at.sub
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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]
{n : ℕ∞}
{f g : M → G}
{s : set M}
{x₀ : M}
(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 (λ (x : M), f x - g x) s x₀
theorem
cont_mdiff_within_at.div
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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]
{n : ℕ∞}
{f g : M → G}
{s : set M}
{x₀ : M}
(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 (λ (x : M), f x / g x) s x₀
theorem
cont_mdiff_at.sub
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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]
{n : ℕ∞}
{f g : M → G}
{x₀ : M}
(hf : cont_mdiff_at I' I n f x₀)
(hg : cont_mdiff_at I' I n g x₀) :
cont_mdiff_at I' I n (λ (x : M), f x - g x) x₀
theorem
cont_mdiff_at.div
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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]
{n : ℕ∞}
{f g : M → G}
{x₀ : M}
(hf : cont_mdiff_at I' I n f x₀)
(hg : cont_mdiff_at I' I n g x₀) :
cont_mdiff_at I' I n (λ (x : M), f x / g x) x₀
theorem
cont_mdiff_on.sub
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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]
{n : ℕ∞}
{f g : M → G}
{s : set M}
(hf : cont_mdiff_on I' I n f s)
(hg : cont_mdiff_on I' I n g s) :
cont_mdiff_on I' I n (λ (x : M), f x - g x) s
theorem
cont_mdiff_on.div
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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]
{n : ℕ∞}
{f g : M → G}
{s : set M}
(hf : cont_mdiff_on I' I n f s)
(hg : cont_mdiff_on I' I n g s) :
cont_mdiff_on I' I n (λ (x : M), f x / g x) s
theorem
cont_mdiff.sub
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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]
{n : ℕ∞}
{f g : M → G}
(hf : cont_mdiff I' I n f)
(hg : cont_mdiff I' I n g) :
cont_mdiff I' I n (λ (x : M), f x - g x)
theorem
cont_mdiff.div
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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]
{n : ℕ∞}
{f g : M → G}
(hf : cont_mdiff I' I n f)
(hg : cont_mdiff I' I n g) :
cont_mdiff I' I n (λ (x : M), f x / g x)
theorem
smooth_within_at.sub
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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 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 (λ (x : M), f x - g x) s x₀
theorem
smooth_within_at.div
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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 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 (λ (x : M), f x / g x) s x₀
theorem
smooth_at.sub
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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 g : M → G}
{x₀ : M}
(hf : smooth_at I' I f x₀)
(hg : smooth_at I' I g x₀) :
theorem
smooth_at.div
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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 g : M → G}
{x₀ : M}
(hf : smooth_at I' I f x₀)
(hg : smooth_at I' I g x₀) :
theorem
smooth_on.sub
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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 g : M → G}
{s : set M}
(hf : smooth_on I' I f s)
(hg : smooth_on I' I g s) :
theorem
smooth_on.div
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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 g : M → G}
{s : set M}
(hf : smooth_on I' I f s)
(hg : smooth_on I' I g s) :
theorem
smooth.sub
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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 g : M → G}
(hf : smooth I' I f)
(hg : smooth I' I g) :
theorem
smooth.div
{𝕜 : 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_5}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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 g : M → G}
(hf : smooth I' I f)
(hg : smooth I' I g) :
@[protected, instance]
def
prod.lie_add_group
{𝕜 : 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}
[topological_space G]
[charted_space H G]
[add_group G]
[lie_add_group 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']
[add_group G']
[lie_add_group I' G'] :
lie_add_group (I.prod I') (G × G')
@[protected, instance]
def
prod.lie_group
{𝕜 : 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}
[topological_space G]
[charted_space H G]
[group G]
[lie_group 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']
[group G']
[lie_group I' G'] :
Normed spaces are Lie groups #
@[protected, instance]
def
normed_space_lie_add_group
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E] :
lie_add_group (model_with_corners_self 𝕜 E) E