smooth_inv
theorem smooth_inv :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_5}
[inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] [inst_7 : LieGroup I G],
Smooth I I fun x => x⁻¹
This theorem states that for a given Lie group, the operation of inversion (taking the reciprocal) is a smooth map. More specifically, given a nontrivially normed field 𝕜, a topological space H, a normed additive commutative group E that is also a normed space over 𝕜, and a model with corners I for the space E with respect to the space H. If we have a topological space G which is a charted space with respect to H and a Group G that is also a Lie Group with respect to I, then the inversion operation, which takes an element of the group to its inverse, is a smooth map from 𝕜 to 𝕜 when considered in the context of the model with corners I.
More concisely: For a Lie group G endowed with a charted space structure over a normed space E and a model with corners I, the inversion map on G is a smooth function from the base space E to itself.
|
smoothAt_inv₀
theorem smoothAt_inv₀ :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_4}
[inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Inv G] [inst_7 : Zero G]
[inst_8 : SmoothInv₀ I G] {x : G}, x ≠ 0 → SmoothAt I I (fun y => y⁻¹) x
This theorem states that for a non-zero point `x` in a topological space `G` that has a smooth inverse operation (`SmoothInv₀ I G`) and is charted with a model `I` (ModelWithCorners) in a normed space `E` over a non-trivially normed field `𝕜`, the function that maps each point `y` to its inverse `y⁻¹` is smooth at `x`. This implies that the inverse function has derivatives of all orders at `x`.
More concisely: Given a non-zero point `x` in a topological space `G` endowed with a smooth inverse operation and charted in a normed space `E` over a non-trivially normed field `𝕜`, the inverse function is smooth at `x`.
|
smooth_neg
theorem smooth_neg :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_5}
[inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] [inst_7 : LieAddGroup I G],
Smooth I I fun x => -x
This theorem states that in an additive Lie group, the operation of inversion (multiplying by -1 or taking the additive inverse) is a smooth map. Here, the smoothness is defined in the context of differential geometry, meaning the map is infinitely differentiable. The theorem holds for any nontrivially normed field 𝕜, topological space H, normed additive commutative group E, and Lie add group G, under the conditions specified by the model with corners I.
More concisely: In an additive Lie group G, the inversion map is a smooth homomorphism.
|
topologicalAddGroup_of_lieAddGroup
theorem topologicalAddGroup_of_lieAddGroup :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_5}
[inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] [inst : LieAddGroup I G],
TopologicalAddGroup G
This theorem states that any additive Lie group is also an additive topological group. Specifically, for any nontrivially normed field 𝕜, topological space H and E, where E is a normed commutative additive group and a normed space over 𝕜, given a model with corners I from 𝕜 to E, and G is both a topological space and a charted space over H, if G is also an additive group and Lie add group, then it can be concluded that G is a topological additive group. Note that this isn't always the case due to certain technical reasons, as outlined in the note [Design choices about smooth algebraic structures].
More concisely: If H is a topological space, E is a normed commutative additive group and a normed space over a nontrivially normed field, G is a charted additive Lie group and an additive group over H, then G is a topological additive group.
|
LieAddGroup.smooth_neg
theorem LieAddGroup.smooth_neg :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
[inst_4 : AddGroup G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [self : LieAddGroup I G],
Smooth I I fun a => -a
This theorem states that for any nontrivially normed field `𝕜`, topological space `H`, normed commutative additive group `E`, model with corners `I` of types `𝕜`, `E`, `H`, additive group `G`, topological space `G`, and charted space `H` on `G` of a Lie additive group `I G`, the negation operation (i.e., changing the sign of each element) is smooth. In the context of differentiable manifolds, a map (or operation) being "smooth" means it is infinitely differentiable.
More concisely: For any nontrivially normed field `𝕜`, normed commutative additive group `E`, topological space `H`, model with corners `I` of types `𝕜`, `E`, `H`, additive group `G`, topological space `G`, and charted space `H` on `G` of a Lie additive group `IG`, the negation operation on `IG` is infinitely differentiable.
|
SmoothInv₀.smoothAt_inv₀
theorem SmoothInv₀.smoothAt_inv₀ :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
[inst_4 : Inv G] [inst_5 : Zero G] [inst_6 : TopologicalSpace G] [inst_7 : ChartedSpace H G]
[self : SmoothInv₀ I G] ⦃x : G⦄, x ≠ 0 → SmoothAt I I (fun y => y⁻¹) x
This theorem states that for any non-zero point `x` in a given topological space `G` that also supports inversion and has a zero, and with `𝕜` being a nontrivially normed field, `E` a normed add comm group which is a normed space over `𝕜`, `H` another topological space, and `I` a model with corners defined over `𝕜`, `E`, and `H`, the function applying inversion (i.e., taking the reciprocal) to `y` is smooth at `x`. In simpler terms, this theorem asserts that away from `0`, the function that maps a number to its inverse is smooth.
More concisely: Given a non-zero point `x` in a topological space `G` with inversion, a nontrivially normed field `𝕜`, a normed additive group `E` over `𝕜` as a normed space, another topological space `H`, and a model `I` with corners, the function `y ↦ 1/y` is smooth at `x` in the function space from `E` to `E` and from `H` to `H`.
|
LieGroup.smooth_inv
theorem LieGroup.smooth_inv :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
[inst_4 : Group G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [self : LieGroup I G],
Smooth I I fun a => a⁻¹
This theorem states that in a Lie group, the inversion operation is smooth. Here, the Lie group is denoted by `G`, which is a group that is also a differentiable manifold, such that the group operations are smooth maps. The term "smooth" means that the function has derivatives of all orders everywhere in its domain, in this case, the inversion function `a => a⁻¹` is smooth. The Lie group is characterized by certain properties defined over structures like a Normed Field `𝕜`, a Topological Space `H` and a Normed Space over `𝕜` and a Normed Additive Commutative Group `E`. The Model With Corners `I` links the manifold `G` to the Euclidean space `E`.
More concisely: In a Lie group `G` (a smooth manifold and differentiable group over a Normed Field `𝕜`), the inversion map `a => a⁻¹` is a smooth function.
|
hasContinuousInv₀_of_hasSmoothInv₀
theorem hasContinuousInv₀_of_hasSmoothInv₀ :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_4}
[inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Inv G] [inst_7 : Zero G]
[inst : SmoothInv₀ I G], HasContinuousInv₀ G
This theorem states that in a manifold, if there exists a smooth inverse function not including `0`, then this inverse function is continuous at all points excluding `0`. The manifold is expressed in terms of a model with corners, and the inverse function operates over a charted space. The mention of "not an instance for technical reasons" refers to the decision to not make this theorem into an instance, which is a specific term in Lean theorem proving referring to theorems or facts that are automatically used by Lean to solve goals. The linked note provides more information about this design decision.
More concisely: In a manifold with corners, if there exists a smooth and bijective inverse function defined outside the origin, then it is continuous at all points excluding the origin.
|
topologicalGroup_of_lieGroup
theorem topologicalGroup_of_lieGroup :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_5}
[inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] [inst : LieGroup I G],
TopologicalGroup G
This theorem states that any Lie group is also a topological group, given certain conditions. More specifically, given a nontrivially normed field `𝕜`, a topological space `H`, a normed add commutative group `E` over the field `𝕜`, a model with corners `I` on `H` with values in `E`, a topological space `G` which is a charted space over `H` and a group (possibly non-abelian), if `G` is a Lie group with regard to these structures, then `G` is also a topological group. The proof is omitted for technical reasons as mentioned in the note [Design choices about smooth algebraic structures].
More concisely: If `G` is a Lie group over a nontrivially normed field `𝕜`, endowed with a topological space `H`, a normed add commutative group `E` over `𝕜`, a model with corners `I` on `H` with values in `E`, and `G` is a charted space over `H`, then `G` is also a topological group.
|