Documentation

Mathlib.Geometry.Manifold.Algebra.LieGroup

Lie groups #

A Lie group is a group that is also a C^n manifold, in which the group operations of multiplication and inversion are C^n maps. Regularity of the group multiplication means that multiplication is a C^n 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 #

Main results #

Implementation notes #

A priori, a Lie group here is a manifold with corners.

The definition of Lie group cannot require I : ModelWithCorners 𝕜 E E with the same space as the model space and as the model vector space, as one might hope, because in the product situation, the model space is ModelProd 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 : ModelWithCorners 𝕜 E H.

class LieAddGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (G : Type u_4) [AddGroup G] [TopologicalSpace G] [ChartedSpace H G] extends ContMDiffAdd I n G :

An additive Lie group is a group and a C^n manifold at the same time in which the addition and negation operations are C^n.

Instances
class LieGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (G : Type u_4) [Group G] [TopologicalSpace G] [ChartedSpace H G] extends ContMDiffMul I n G :

A (multiplicative) Lie group is a group and a C^n manifold at the same time in which the multiplication and inverse operations are C^n.

Instances

Smoothness of inversion, negation, division and subtraction #

Let f : M → G be a C^n function into a Lie group, then f is point-wise invertible with smooth inverse f. If f and g are two such functions, the quotient f / g (i.e., the point-wise product of f and the point-wise inverse of g) is also C^n.

theorem LieGroup.of_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {m n : WithTop ℕ∞} (hmn : m n) [h : LieGroup I n G] :
LieGroup I m G
theorem LieAddGroup.of_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {m n : WithTop ℕ∞} (hmn : m n) [h : LieAddGroup I n G] :
instance instLieGroupOfSomeENatTopOfLEInfty {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {a : WithTop ℕ∞} [LieGroup I (↑) G] [h : ENat.LEInfty a] :
LieGroup I a G
instance instLieAddGroupOfSomeENatTopOfLEInfty {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {a : WithTop ℕ∞} [LieAddGroup I (↑) G] [h : ENat.LEInfty a] :
instance instLieGroupOfTopWithTopENat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {a : WithTop ℕ∞} [LieGroup I G] :
LieGroup I a G
instance instLieAddGroupOfTopWithTopENat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {a : WithTop ℕ∞} [LieAddGroup I G] :
instance instLieGroupOfNatWithTopENat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I 2 G] :
LieGroup I 1 G
instance instLieAddGroupOfNatWithTopENat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I 2 G] :
theorem contMDiff_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I n G] :
ContMDiff I I n fun (x : G) => x⁻¹

In a Lie group, inversion is C^n.

theorem contMDiff_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I n G] :
ContMDiff I I n fun (x : G) => -x

In an additive Lie group, inversion is a smooth map.

@[deprecated contMDiff_inv (since := "2024-11-21")]
theorem smooth_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I n G] :
ContMDiff I I n fun (x : G) => x⁻¹

Alias of contMDiff_inv.


In a Lie group, inversion is C^n.

@[deprecated contMDiff_neg (since := "2024-11-21")]
theorem smooth_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I n G] :
ContMDiff I I n fun (x : G) => -x

Alias of contMDiff_neg.


In an additive Lie group, inversion is a smooth map.

theorem topologicalGroup_of_lieGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I n G] :

A Lie group is a topological group. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

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 ContMDiffWithinAt.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f : MG} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) :
ContMDiffWithinAt I' I n (fun (x : M) => (f x)⁻¹) s x₀
theorem ContMDiffWithinAt.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f : MG} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) :
ContMDiffWithinAt I' I n (fun (x : M) => -f x) s x₀
theorem ContMDiffAt.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f : MG} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) :
ContMDiffAt I' I n (fun (x : M) => (f x)⁻¹) x₀
theorem ContMDiffAt.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f : MG} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) :
ContMDiffAt I' I n (fun (x : M) => -f x) x₀
theorem ContMDiffOn.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) :
ContMDiffOn I' I n (fun (x : M) => (f x)⁻¹) s
theorem ContMDiffOn.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) :
ContMDiffOn I' I n (fun (x : M) => -f x) s
theorem ContMDiff.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f : MG} (hf : ContMDiff I' I n f) :
ContMDiff I' I n fun (x : M) => (f x)⁻¹
theorem ContMDiff.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f : MG} (hf : ContMDiff I' I n f) :
ContMDiff I' I n fun (x : M) => -f x
@[deprecated ContMDiffWithinAt.inv (since := "2024-11-21")]
theorem SmoothWithinAt.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f : MG} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) :
ContMDiffWithinAt I' I n (fun (x : M) => (f x)⁻¹) s x₀

Alias of ContMDiffWithinAt.inv.

@[deprecated ContMDiffAt.inv (since := "2024-11-21")]
theorem SmoothAt.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f : MG} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) :
ContMDiffAt I' I n (fun (x : M) => (f x)⁻¹) x₀

Alias of ContMDiffAt.inv.

@[deprecated ContMDiffOn.inv (since := "2024-11-21")]
theorem SmoothOn.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) :
ContMDiffOn I' I n (fun (x : M) => (f x)⁻¹) s

Alias of ContMDiffOn.inv.

@[deprecated ContMDiff.inv (since := "2024-11-21")]
theorem Smooth.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f : MG} (hf : ContMDiff I' I n f) :
ContMDiff I' I n fun (x : M) => (f x)⁻¹

Alias of ContMDiff.inv.

@[deprecated ContMDiffWithinAt.neg (since := "2024-11-21")]
theorem SmoothWithinAt.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f : MG} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) :
ContMDiffWithinAt I' I n (fun (x : M) => -f x) s x₀

Alias of ContMDiffWithinAt.neg.

@[deprecated ContMDiffAt.neg (since := "2024-11-21")]
theorem SmoothAt.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f : MG} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) :
ContMDiffAt I' I n (fun (x : M) => -f x) x₀

Alias of ContMDiffAt.neg.

@[deprecated ContMDiffOn.neg (since := "2024-11-21")]
theorem SmoothOn.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) :
ContMDiffOn I' I n (fun (x : M) => -f x) s

Alias of ContMDiffOn.neg.

@[deprecated ContMDiff.neg (since := "2024-11-21")]
theorem Smooth.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f : MG} (hf : ContMDiff I' I n f) :
ContMDiff I' I n fun (x : M) => -f x

Alias of ContMDiff.neg.

theorem ContMDiffWithinAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f g : MG} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) (hg : ContMDiffWithinAt I' I n g s x₀) :
ContMDiffWithinAt I' I n (fun (x : M) => f x / g x) s x₀
theorem ContMDiffWithinAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f g : MG} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) (hg : ContMDiffWithinAt I' I n g s x₀) :
ContMDiffWithinAt I' I n (fun (x : M) => f x - g x) s x₀
theorem ContMDiffAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f g : MG} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) (hg : ContMDiffAt I' I n g x₀) :
ContMDiffAt I' I n (fun (x : M) => f x / g x) x₀
theorem ContMDiffAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f g : MG} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) (hg : ContMDiffAt I' I n g x₀) :
ContMDiffAt I' I n (fun (x : M) => f x - g x) x₀
theorem ContMDiffOn.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f g : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) :
ContMDiffOn I' I n (fun (x : M) => f x / g x) s
theorem ContMDiffOn.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f g : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) :
ContMDiffOn I' I n (fun (x : M) => f x - g x) s
theorem ContMDiff.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f g : MG} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) :
ContMDiff I' I n fun (x : M) => f x / g x
theorem ContMDiff.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f g : MG} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) :
ContMDiff I' I n fun (x : M) => f x - g x
@[deprecated ContMDiffWithinAt.div (since := "2024-11-21")]
theorem SmoothWithinAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f g : MG} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) (hg : ContMDiffWithinAt I' I n g s x₀) :
ContMDiffWithinAt I' I n (fun (x : M) => f x / g x) s x₀

Alias of ContMDiffWithinAt.div.

@[deprecated ContMDiffAt.div (since := "2024-11-21")]
theorem SmoothAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f g : MG} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) (hg : ContMDiffAt I' I n g x₀) :
ContMDiffAt I' I n (fun (x : M) => f x / g x) x₀

Alias of ContMDiffAt.div.

@[deprecated ContMDiffOn.div (since := "2024-11-21")]
theorem SmoothOn.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f g : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) :
ContMDiffOn I' I n (fun (x : M) => f x / g x) s

Alias of ContMDiffOn.div.

@[deprecated ContMDiff.div (since := "2024-11-21")]
theorem Smooth.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieGroup I n G] {f g : MG} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) :
ContMDiff I' I n fun (x : M) => f x / g x

Alias of ContMDiff.div.

@[deprecated ContMDiffWithinAt.sub (since := "2024-11-21")]
theorem SmoothWithinAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f g : MG} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) (hg : ContMDiffWithinAt I' I n g s x₀) :
ContMDiffWithinAt I' I n (fun (x : M) => f x - g x) s x₀

Alias of ContMDiffWithinAt.sub.

@[deprecated ContMDiffAt.sub (since := "2024-11-21")]
theorem SmoothAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f g : MG} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) (hg : ContMDiffAt I' I n g x₀) :
ContMDiffAt I' I n (fun (x : M) => f x - g x) x₀

Alias of ContMDiffAt.sub.

@[deprecated ContMDiffOn.sub (since := "2024-11-21")]
theorem SmoothOn.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f g : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) :
ContMDiffOn I' I n (fun (x : M) => f x - g x) s

Alias of ContMDiffOn.sub.

@[deprecated ContMDiff.sub (since := "2024-11-21")]
theorem Smooth.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] [LieAddGroup I n G] {f g : MG} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) :
ContMDiff I' I n fun (x : M) => f x - g x

Alias of ContMDiff.sub.

Binary product of Lie groups

instance Prod.instLieGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I n G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [TopologicalSpace G'] [ChartedSpace H' G'] [Group G'] [LieGroup I' n G'] :
LieGroup (I.prod I') n (G × G')
instance Prod.instLieAddGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I n G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [TopologicalSpace G'] [ChartedSpace H' G'] [AddGroup G'] [LieAddGroup I' n G'] :
LieAddGroup (I.prod I') n (G × G')

Normed spaces are Lie groups #

C^n manifolds with C^n inversion away from zero #

Typeclass for C^n manifolds with 0 and Inv such that inversion is C^n at all non-zero points. (This includes multiplicative Lie groups, but also complete normed semifields.) Point-wise inversion is C^n when the function/denominator is non-zero.

class ContMDiffInv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (G : Type u_4) [Inv G] [Zero G] [TopologicalSpace G] [ChartedSpace H G] :

A C^n manifold with 0 and Inv such that fun x ↦ x⁻¹ is C^n at all nonzero points. Any complete normed (semi)field has this property.

  • contMDiffAt_inv₀ x : G : x 0ContMDiffAt I I n (fun (y : G) => y⁻¹) x

    Inversion is C^n away from 0.

Instances
@[deprecated ContMDiffInv₀ (since := "2025-01-09")]
def SmoothInv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (G : Type u_4) [Inv G] [Zero G] [TopologicalSpace G] [ChartedSpace H G] :

Alias of ContMDiffInv₀.


A C^n manifold with 0 and Inv such that fun x ↦ x⁻¹ is C^n at all nonzero points. Any complete normed (semi)field has this property.

Equations
theorem ContMDiffInv₀.of_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] {m n : WithTop ℕ∞} (hmn : m n) [h : ContMDiffInv₀ I n G] :
instance instContMDiffInv₀OfSomeENatTopOfLEInfty {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] {a : WithTop ℕ∞} [ContMDiffInv₀ I (↑) G] [h : ENat.LEInfty a] :
instance instContMDiffInv₀OfNatWithTopENat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [ContMDiffInv₀ I 2 G] :
theorem contMDiffAt_inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [ContMDiffInv₀ I n G] {x : G} (hx : x 0) :
ContMDiffAt I I n (fun (y : G) => y⁻¹) x
@[deprecated contMDiffAt_inv₀ (since := "2024-11-21")]
theorem smoothAt_inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [ContMDiffInv₀ I n G] {x : G} (hx : x 0) :
ContMDiffAt I I n (fun (y : G) => y⁻¹) x

Alias of contMDiffAt_inv₀.

In a manifold with C^n inverse away from 0, the inverse is continuous away from 0. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

@[deprecated hasContinuousInv₀_of_hasContMDiffInv₀ (since := "2025-01-09")]

Alias of hasContinuousInv₀_of_hasContMDiffInv₀.


In a manifold with C^n inverse away from 0, the inverse is continuous away from 0. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

theorem contMDiffOn_inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [ContMDiffInv₀ I n G] :
@[deprecated contMDiffOn_inv₀ (since := "2024-11-21")]
theorem smoothOn_inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [ContMDiffInv₀ I n G] :

Alias of contMDiffOn_inv₀.

@[deprecated contMDiffOn_inv₀ (since := "2024-11-21")]
theorem SmoothOn_inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [ContMDiffInv₀ I n G] :

Alias of contMDiffOn_inv₀.

theorem ContMDiffWithinAt.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} [ContMDiffInv₀ I n G] {s : Set M} {a : M} (hf : ContMDiffWithinAt I' I n f s a) (ha : f a 0) :
ContMDiffWithinAt I' I n (fun (x : M) => (f x)⁻¹) s a
theorem ContMDiffAt.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} [ContMDiffInv₀ I n G] {a : M} (hf : ContMDiffAt I' I n f a) (ha : f a 0) :
ContMDiffAt I' I n (fun (x : M) => (f x)⁻¹) a
theorem ContMDiff.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} [ContMDiffInv₀ I n G] (hf : ContMDiff I' I n f) (h0 : ∀ (x : M), f x 0) :
ContMDiff I' I n fun (x : M) => (f x)⁻¹
theorem ContMDiffOn.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} [ContMDiffInv₀ I n G] {s : Set M} (hf : ContMDiffOn I' I n f s) (h0 : xs, f x 0) :
ContMDiffOn I' I n (fun (x : M) => (f x)⁻¹) s
@[deprecated ContMDiffWithinAt.inv₀ (since := "2024-11-21")]
theorem SmoothWithinAt.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} [ContMDiffInv₀ I n G] {s : Set M} {a : M} (hf : ContMDiffWithinAt I' I n f s a) (ha : f a 0) :
ContMDiffWithinAt I' I n (fun (x : M) => (f x)⁻¹) s a

Alias of ContMDiffWithinAt.inv₀.

@[deprecated ContMDiffAt.inv₀ (since := "2024-11-21")]
theorem SmoothAt.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} [ContMDiffInv₀ I n G] {a : M} (hf : ContMDiffAt I' I n f a) (ha : f a 0) :
ContMDiffAt I' I n (fun (x : M) => (f x)⁻¹) a

Alias of ContMDiffAt.inv₀.

@[deprecated ContMDiffOn.inv₀ (since := "2024-11-21")]
theorem SmoothOn.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} [ContMDiffInv₀ I n G] {s : Set M} (hf : ContMDiffOn I' I n f s) (h0 : xs, f x 0) :
ContMDiffOn I' I n (fun (x : M) => (f x)⁻¹) s

Alias of ContMDiffOn.inv₀.

@[deprecated ContMDiff.inv₀ (since := "2024-11-21")]
theorem Smooth.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} [ContMDiffInv₀ I n G] (hf : ContMDiff I' I n f) (h0 : ∀ (x : M), f x 0) :
ContMDiff I' I n fun (x : M) => (f x)⁻¹

Alias of ContMDiff.inv₀.

Point-wise division of C^n functions #

If [ContMDiffMul I n N] and [ContMDiffInv₀ I n N], point-wise division of C^n functions f : M → N is C^n whenever the denominator is non-zero. (This includes N being a completely normed field.)

theorem ContMDiffWithinAt.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [ContMDiffInv₀ I n G] [ContMDiffMul I n G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f g : MG} {s : Set M} {a : M} (hf : ContMDiffWithinAt I' I n f s a) (hg : ContMDiffWithinAt I' I n g s a) (h₀ : g a 0) :
ContMDiffWithinAt I' I n (f / g) s a
theorem ContMDiffOn.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [ContMDiffInv₀ I n G] [ContMDiffMul I n G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f g : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) (h₀ : xs, g x 0) :
ContMDiffOn I' I n (f / g) s
theorem ContMDiffAt.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [ContMDiffInv₀ I n G] [ContMDiffMul I n G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f g : MG} {a : M} (hf : ContMDiffAt I' I n f a) (hg : ContMDiffAt I' I n g a) (h₀ : g a 0) :
ContMDiffAt I' I n (f / g) a
theorem ContMDiff.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [ContMDiffInv₀ I n G] [ContMDiffMul I n G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f g : MG} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) (h₀ : ∀ (x : M), g x 0) :
ContMDiff I' I n (f / g)
@[deprecated ContMDiffWithinAt.div₀ (since := "2024-11-21")]
theorem SmoothWithinAt.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [ContMDiffInv₀ I n G] [ContMDiffMul I n G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f g : MG} {s : Set M} {a : M} (hf : ContMDiffWithinAt I' I n f s a) (hg : ContMDiffWithinAt I' I n g s a) (h₀ : g a 0) :
ContMDiffWithinAt I' I n (f / g) s a

Alias of ContMDiffWithinAt.div₀.

@[deprecated ContMDiffAt.div₀ (since := "2024-11-21")]
theorem SmoothAt.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [ContMDiffInv₀ I n G] [ContMDiffMul I n G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f g : MG} {a : M} (hf : ContMDiffAt I' I n f a) (hg : ContMDiffAt I' I n g a) (h₀ : g a 0) :
ContMDiffAt I' I n (f / g) a

Alias of ContMDiffAt.div₀.

@[deprecated ContMDiffOn.div₀ (since := "2024-11-21")]
theorem SmoothOn.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [ContMDiffInv₀ I n G] [ContMDiffMul I n G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f g : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) (h₀ : xs, g x 0) :
ContMDiffOn I' I n (f / g) s

Alias of ContMDiffOn.div₀.

@[deprecated ContMDiff.div₀ (since := "2024-11-21")]
theorem Smooth.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [ContMDiffInv₀ I n G] [ContMDiffMul I n G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f g : MG} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) (h₀ : ∀ (x : M), g x 0) :
ContMDiff I' I n (f / g)

Alias of ContMDiff.div₀.