Lie groups #
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 #
LieAddGroup I G: a Lie additive group whereGis a manifold on the model with cornersI.LieGroup I G: a Lie multiplicative group whereGis a manifold on the model with cornersI.SmoothInv₀: typeclass for smooth manifolds with0andInvsuch that inversion is a smooth map at each non-zero point. This includes complete normed fields and (multiplicative) Lie groups.
Main results #
ContMDiff.inv,ContMDiff.divand variants: point-wise inversion and division of mapsM → Gis smoothContMDiff.inv₀and variants: ifSmoothInv₀ N, point-wise inversion of smooth mapsf : M → Nis smooth at all points at whichfdoesn't vanish.ContMDiff.div₀and variants: if alsoSmoothMul N(i.e.,Nis a Lie group except possibly for smoothness of inversion at0), similar results hold for point-wise division.normedSpaceLieAddGroup: a normed vector space over a nontrivially normed field is an additive Lie group.Instances/UnitsOfNormedAlgebrashows that the group of units of a complete normed𝕜-algebra is a multiplicative Lie group.
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)
(G : Type u_4)
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H G]
extends
SmoothAdd
:
An additive Lie group is a group and a smooth manifold at the same time in which the addition and negation operations are smooth.
- compatible : ∀ {e e' : PartialHomeomorph G H}, e ∈ atlas H G → e' ∈ atlas H G → e.symm.trans e' ∈ contDiffGroupoid ⊤ I
Negation is smooth in an additive Lie group.
Instances
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 : G) => -a
Negation is smooth in an additive Lie group.
class
LieGroup
{𝕜 : 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)
[Group G]
[TopologicalSpace G]
[ChartedSpace H G]
extends
SmoothMul
:
A (multiplicative) Lie group is a group and a smooth manifold at the same time in which the multiplication and inverse operations are smooth.
- compatible : ∀ {e e' : PartialHomeomorph G H}, e ∈ atlas H G → e' ∈ atlas H G → e.symm.trans e' ∈ contDiffGroupoid ⊤ I
Inversion is smooth in a Lie group.
Instances
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 : G) => a⁻¹
Inversion is smooth in a Lie group.
Smoothness of inversion, negation, division and subtraction #
Let f : M → G be a C^n or smooth functions 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 smooth.
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)
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I G]
:
In an additive Lie group, inversion is a smooth map.
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)
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I G]
:
In a Lie group, inversion is a smooth map.
theorem
topologicalAddGroup_of_lieAddGroup
{𝕜 : 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 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
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)
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup 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
ContMDiffWithinAt.neg
{𝕜 : 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 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]
{n : ℕ∞}
{f : M → G}
{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.inv
{𝕜 : 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 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]
{n : ℕ∞}
{f : M → G}
{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.neg
{𝕜 : 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 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]
{n : ℕ∞}
{f : M → G}
{x₀ : M}
(hf : ContMDiffAt I' I n f x₀)
:
ContMDiffAt I' I n (fun (x : M) => -f x) 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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I 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]
{n : ℕ∞}
{f : M → G}
{x₀ : M}
(hf : ContMDiffAt I' I n f x₀)
:
ContMDiffAt I' I n (fun (x : M) => (f x)⁻¹) x₀
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I 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]
{n : ℕ∞}
{f : M → G}
{s : Set M}
(hf : ContMDiffOn I' I n f s)
:
ContMDiffOn I' I n (fun (x : M) => -f x) s
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I 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]
{n : ℕ∞}
{f : M → G}
{s : Set M}
(hf : ContMDiffOn I' I n f s)
:
ContMDiffOn I' I n (fun (x : M) => (f x)⁻¹) s
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I 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]
{n : ℕ∞}
{f : M → G}
(hf : ContMDiff I' I n f)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I 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]
{n : ℕ∞}
{f : M → G}
(hf : ContMDiff I' I n f)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I 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 : M → G}
{s : Set M}
{x₀ : M}
(hf : SmoothWithinAt I' I f s x₀)
:
SmoothWithinAt I' I (fun (x : M) => -f x) s x₀
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I 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 : M → G}
{s : Set M}
{x₀ : M}
(hf : SmoothWithinAt I' I f s x₀)
:
SmoothWithinAt I' I (fun (x : M) => (f x)⁻¹) s x₀
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I 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 : M → G}
{x₀ : M}
(hf : SmoothAt I' I f x₀)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I 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 : M → G}
{x₀ : M}
(hf : SmoothAt I' I f x₀)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I 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 : M → G}
{s : Set M}
(hf : SmoothOn I' I f s)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I 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 : M → G}
{s : Set M}
(hf : SmoothOn I' I f s)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I 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 : M → G}
(hf : Smooth I' I f)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I 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 : M → G}
(hf : Smooth I' I f)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I 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]
{n : ℕ∞}
{f : M → G}
{g : M → G}
{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.div
{𝕜 : 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 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]
{n : ℕ∞}
{f : M → G}
{g : M → G}
{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.sub
{𝕜 : 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 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]
{n : ℕ∞}
{f : M → G}
{g : M → G}
{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.div
{𝕜 : 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 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]
{n : ℕ∞}
{f : M → G}
{g : M → G}
{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.sub
{𝕜 : 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 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]
{n : ℕ∞}
{f : M → G}
{g : M → G}
{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.div
{𝕜 : 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 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]
{n : ℕ∞}
{f : M → G}
{g : M → G}
{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.sub
{𝕜 : 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 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]
{n : ℕ∞}
{f : M → G}
{g : M → G}
(hf : ContMDiff I' I n f)
(hg : ContMDiff I' I n g)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I 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]
{n : ℕ∞}
{f : M → G}
{g : M → G}
(hf : ContMDiff I' I n f)
(hg : ContMDiff I' I n g)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I 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 : M → G}
{g : M → G}
{s : Set M}
{x₀ : M}
(hf : SmoothWithinAt I' I f s x₀)
(hg : SmoothWithinAt I' I g s x₀)
:
SmoothWithinAt I' I (fun (x : M) => f x - g x) s x₀
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I 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 : M → G}
{g : M → G}
{s : Set M}
{x₀ : M}
(hf : SmoothWithinAt I' I f s x₀)
(hg : SmoothWithinAt I' I g s x₀)
:
SmoothWithinAt I' I (fun (x : M) => f x / g x) s x₀
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I 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 : M → G}
{g : M → G}
{x₀ : M}
(hf : SmoothAt I' I f x₀)
(hg : SmoothAt I' I g x₀)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I 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 : M → G}
{g : M → G}
{x₀ : M}
(hf : SmoothAt I' I f x₀)
(hg : SmoothAt I' I g x₀)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I 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 : M → G}
{g : M → G}
{s : Set M}
(hf : SmoothOn I' I f s)
(hg : SmoothOn I' I g s)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I 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 : M → G}
{g : M → G}
{s : Set M}
(hf : SmoothOn I' I f s)
(hg : SmoothOn I' I g s)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I 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 : M → G}
{g : M → G}
(hf : Smooth I' I f)
(hg : Smooth I' I g)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I 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 : M → G}
{g : M → G}
(hf : Smooth I' I f)
(hg : Smooth I' I g)
:
Binary product of Lie groups
instance
instLieAddGroupModelSumSumSum
{𝕜 : 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 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' G']
:
LieAddGroup (I.prod I') (G × G')
Equations
- ⋯ = ⋯
instance
instLieGroupModelProdProdProd
{𝕜 : 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 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' G']
:
Equations
- ⋯ = ⋯
Normed spaces are Lie groups #
instance
normedSpaceLieAddGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
:
LieAddGroup (modelWithCornersSelf 𝕜 E) E
Equations
- ⋯ = ⋯
Smooth manifolds with smooth inversion away from zero #
Typeclass for smooth manifolds with 0 and Inv such that inversion is smooth at all non-zero
points. (This includes multiplicative Lie groups, but also complete normed semifields.)
Point-wise inversion is smooth when the function/denominator is non-zero.
class
SmoothInv₀
{𝕜 : 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)
[Inv G]
[Zero G]
[TopologicalSpace G]
[ChartedSpace H G]
:
A smooth manifold with 0 and Inv such that fun x ↦ x⁻¹ is smooth at all nonzero points.
Any complete normed (semi)field has this property.
Inversion is smooth away from
0.
Instances
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 : G) => y⁻¹) x
Inversion is smooth away from 0.
instance
instSmoothInv₀ModelWithCornersSelfOfCompleteSpace
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
:
SmoothInv₀ (modelWithCornersSelf 𝕜 𝕜) 𝕜
Equations
- ⋯ = ⋯
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)
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Inv G]
[Zero G]
[SmoothInv₀ I G]
{x : G}
(hx : x ≠ 0)
:
theorem
hasContinuousInv₀_of_hasSmoothInv₀
{𝕜 : 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]
[SmoothInv₀ I G]
:
In a manifold with smooth 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
SmoothOn_inv₀
{𝕜 : 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]
[SmoothInv₀ I G]
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Inv G]
[Zero G]
[SmoothInv₀ I 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]
{n : ℕ∞}
{f : M → 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 𝕜]
{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]
[SmoothInv₀ I 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]
{n : ℕ∞}
{f : M → 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 𝕜]
{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]
[SmoothInv₀ I 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]
{n : ℕ∞}
{f : M → G}
(hf : ContMDiff I' I n f)
(h0 : ∀ (x : M), f x ≠ 0)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Inv G]
[Zero G]
[SmoothInv₀ I 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]
{n : ℕ∞}
{f : M → G}
{s : Set M}
(hf : ContMDiffOn I' I n f s)
(h0 : ∀ x ∈ s, f x ≠ 0)
:
ContMDiffOn I' I n (fun (x : M) => (f x)⁻¹) s
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Inv G]
[Zero G]
[SmoothInv₀ I 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 : M → G}
{s : Set M}
{a : M}
(hf : SmoothWithinAt I' I f s a)
(ha : f a ≠ 0)
:
SmoothWithinAt I' I (fun (x : M) => (f x)⁻¹) s a
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Inv G]
[Zero G]
[SmoothInv₀ I 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 : M → G}
{a : M}
(hf : SmoothAt I' I f a)
(ha : f a ≠ 0)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Inv G]
[Zero G]
[SmoothInv₀ I 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 : M → G}
(hf : Smooth I' I f)
(h0 : ∀ (x : M), f x ≠ 0)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Inv G]
[Zero G]
[SmoothInv₀ I 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 : M → G}
{s : Set M}
(hf : SmoothOn I' I f s)
(h0 : ∀ x ∈ s, f x ≠ 0)
:
Point-wise division of smooth functions #
If [SmoothMul I N] and [SmoothInv₀ I N], point-wise division of smooth functions f : M → N
is smooth whenever the denominator is non-zero. (This includes N being a completely normed field.)
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[GroupWithZero G]
[SmoothInv₀ I G]
[SmoothMul I 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 : M → G}
{g : M → G}
{s : Set M}
{a : M}
{n : ℕ∞}
(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 𝕜]
{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]
[SmoothInv₀ I G]
[SmoothMul I 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 : M → G}
{g : M → G}
{s : Set M}
{n : ℕ∞}
(hf : ContMDiffOn I' I n f s)
(hg : ContMDiffOn I' I n g s)
(h₀ : ∀ x ∈ s, g x ≠ 0)
:
ContMDiffOn I' I n (f / g) s
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[GroupWithZero G]
[SmoothInv₀ I G]
[SmoothMul I 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 : M → G}
{g : M → G}
{a : M}
{n : ℕ∞}
(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 𝕜]
{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]
[SmoothInv₀ I G]
[SmoothMul I 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 : M → G}
{g : M → G}
{n : ℕ∞}
(hf : ContMDiff I' I n f)
(hg : ContMDiff I' I n g)
(h₀ : ∀ (x : M), g x ≠ 0)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[GroupWithZero G]
[SmoothInv₀ I G]
[SmoothMul I 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 : M → G}
{g : M → G}
{s : Set M}
{a : M}
(hf : SmoothWithinAt I' I f s a)
(hg : SmoothWithinAt I' I g s a)
(h₀ : g a ≠ 0)
:
SmoothWithinAt I' I (f / g) s a
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[GroupWithZero G]
[SmoothInv₀ I G]
[SmoothMul I 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 : M → G}
{g : M → G}
{s : Set M}
(hf : SmoothOn I' I f s)
(hg : SmoothOn I' I g s)
(h₀ : ∀ x ∈ s, g x ≠ 0)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[GroupWithZero G]
[SmoothInv₀ I G]
[SmoothMul I 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 : M → G}
{g : M → G}
{a : M}
(hf : SmoothAt I' I f a)
(hg : SmoothAt I' I g a)
(h₀ : g a ≠ 0)
:
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}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[GroupWithZero G]
[SmoothInv₀ I G]
[SmoothMul I 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 : M → G}
{g : M → G}
(hf : Smooth I' I f)
(hg : Smooth I' I g)
(h₀ : ∀ (x : M), g x ≠ 0)
: