mathlib3 documentation

geometry.manifold.algebra.lie_group

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 #

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

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

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] :
smooth I I (λ (x : G), x⁻¹)
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] :
smooth I I (λ (x : G), -x)

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].

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₀) :
smooth_at I' I (λ (x : M), (f x)⁻¹) 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₀) :
smooth_at I' I (λ (x : M), -f x) 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) :
smooth_on I' I (λ (x : M), -f x) 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) :
smooth_on I' I (λ (x : M), (f x)⁻¹) 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) :
smooth I' I (λ (x : M), (f x)⁻¹)
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) :
smooth I' I (λ (x : M), -f x)
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₀) :
smooth_at I' I (λ (x : M), f x - g x) 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₀) :
smooth_at I' I (λ (x : M), f x / g x) 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) :
smooth_on I' I (f - 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) :
smooth_on I' I (f / 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) :
smooth I' I (f - 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) :
smooth I' I (f / 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'] :
lie_group (I.prod I') (G × G')

Normed spaces are Lie groups #

@[protected, instance]