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 #
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.ContMDiffInv₀: typeclass forC^nmanifolds with0andInvsuch that inversion isC^nmap 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 → GisC^n.ContMDiff.inv₀and variants: ifContMDiffInv₀ I n N, point-wise inversion ofC^nmapsf : M → NisC^nat all points at whichfdoesn't vanish.ContMDiff.div₀and variants: if alsoContMDiffMul I n N(i.e.,Nis a Lie group except possibly for smoothness of inversion at0), similar results hold for point-wise division.instNormedSpaceLieAddGroup: 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.
structure
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 ENat)
(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.
- compatible {e e' : PartialHomeomorph G H} : Membership.mem (atlas H G) e → Membership.mem (atlas H G) e' → Membership.mem (contDiffGroupoid n I) (e.symm.trans e')
Negation is smooth in an additive Lie group.
Instances For
structure
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 ENat)
(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.
- compatible {e e' : PartialHomeomorph G H} : Membership.mem (atlas H G) e → Membership.mem (atlas H G) e' → Membership.mem (contDiffGroupoid n I) (e.symm.trans e')
Inversion is smooth in a Lie group.
Instances For
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 ENat}
(hmn : LE.le 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 ENat}
(hmn : LE.le m n)
[h : LieAddGroup I n G]
:
LieAddGroup I m G
theorem
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 ENat}
[LieGroup I (WithTop.some Top.top) G]
[h : ENat.LEInfty a]
:
LieGroup I a G
theorem
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 ENat}
[LieAddGroup I (WithTop.some Top.top) G]
[h : ENat.LEInfty a]
:
LieAddGroup I a G
theorem
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 ENat}
[LieGroup I Top.top G]
:
LieGroup I a G
theorem
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 ENat}
[LieAddGroup I Top.top G]
:
LieAddGroup I a G
theorem
instLieGroupOfNatWithTopENatOfIsTopologicalGroup
{𝕜 : 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]
[IsTopologicalGroup G]
:
LieGroup I 0 G
theorem
instLieAddGroupOfNatWithTopENatOfIsTopologicalAddGroup
{𝕜 : 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]
[IsTopologicalAddGroup G]
:
LieAddGroup I 0 G
theorem
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
theorem
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]
:
LieAddGroup I 1 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 ENat)
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I n G]
:
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 ENat)
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I n G]
:
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 ENat)
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I n G]
:
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 ENat)
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I n G]
:
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 ENat)
{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].
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)
(n : WithTop ENat)
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I n 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
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 ENat}
{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 : M → G}
{s : Set M}
{x₀ : M}
(hf : ContMDiffWithinAt I' I n f s x₀)
:
ContMDiffWithinAt I' I n (fun (x : M) => Inv.inv (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 ENat}
{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 : M → G}
{s : Set M}
{x₀ : M}
(hf : ContMDiffWithinAt I' I n f s x₀)
:
ContMDiffWithinAt I' I n (fun (x : M) => Neg.neg (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 ENat}
{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 : M → G}
{x₀ : M}
(hf : ContMDiffAt I' I n f x₀)
:
ContMDiffAt I' I n (fun (x : M) => Inv.inv (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 ENat}
{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 : M → G}
{x₀ : M}
(hf : ContMDiffAt I' I n f x₀)
:
ContMDiffAt I' I n (fun (x : M) => Neg.neg (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 ENat}
{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 : M → G}
{s : Set M}
(hf : ContMDiffOn I' I n f s)
:
ContMDiffOn I' I n (fun (x : M) => Inv.inv (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 ENat}
{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 : M → G}
{s : Set M}
(hf : ContMDiffOn I' I n f s)
:
ContMDiffOn I' I n (fun (x : M) => Neg.neg (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 ENat}
{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 : M → G}
(hf : ContMDiff I' I n f)
:
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 ENat}
{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 : M → G}
(hf : ContMDiff I' I n f)
:
@[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 ENat}
{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 : M → G}
{s : Set M}
{x₀ : M}
(hf : ContMDiffWithinAt I' I n f s x₀)
:
ContMDiffWithinAt I' I n (fun (x : M) => Inv.inv (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 ENat}
{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 : M → G}
{x₀ : M}
(hf : ContMDiffAt I' I n f x₀)
:
ContMDiffAt I' I n (fun (x : M) => Inv.inv (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 ENat}
{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 : M → G}
{s : Set M}
(hf : ContMDiffOn I' I n f s)
:
ContMDiffOn I' I n (fun (x : M) => Inv.inv (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 ENat}
{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 : M → G}
(hf : ContMDiff I' I n f)
:
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 ENat}
{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 : M → G}
{s : Set M}
{x₀ : M}
(hf : ContMDiffWithinAt I' I n f s x₀)
:
ContMDiffWithinAt I' I n (fun (x : M) => Neg.neg (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 ENat}
{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 : M → G}
{x₀ : M}
(hf : ContMDiffAt I' I n f x₀)
:
ContMDiffAt I' I n (fun (x : M) => Neg.neg (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 ENat}
{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 : M → G}
{s : Set M}
(hf : ContMDiffOn I' I n f s)
:
ContMDiffOn I' I n (fun (x : M) => Neg.neg (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 ENat}
{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 : M → G}
(hf : ContMDiff I' I n f)
:
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 ENat}
{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 : 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) => HDiv.hDiv (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 ENat}
{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 : 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) => HSub.hSub (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 ENat}
{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 : 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) => HDiv.hDiv (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 ENat}
{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 : 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) => HSub.hSub (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 ENat}
{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 : 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) => HDiv.hDiv (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 ENat}
{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 : 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) => HSub.hSub (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 ENat}
{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 : M → G}
(hf : ContMDiff I' I n f)
(hg : ContMDiff I' I n g)
:
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 ENat}
{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 : M → G}
(hf : ContMDiff I' I n f)
(hg : ContMDiff I' I n g)
:
@[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 ENat}
{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 : 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) => HDiv.hDiv (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 ENat}
{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 : 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) => HDiv.hDiv (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 ENat}
{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 : 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) => HDiv.hDiv (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 ENat}
{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 : M → G}
(hf : ContMDiff I' I n f)
(hg : ContMDiff I' I n g)
:
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 ENat}
{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 : 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) => HSub.hSub (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 ENat}
{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 : 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) => HSub.hSub (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 ENat}
{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 : 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) => HSub.hSub (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 ENat}
{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 : M → G}
(hf : ContMDiff I' I n f)
(hg : ContMDiff I' I n g)
:
Alias of ContMDiff.sub.
Binary product of Lie groups
theorem
Prod.instLieGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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']
:
theorem
Prod.instLieAddGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 (Prod G G')
Normed spaces are Lie groups #
theorem
instNormedSpaceLieAddGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
:
LieAddGroup (modelWithCornersSelf 𝕜 E) n E
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.
structure
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 ENat)
(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⦄ : Ne x 0 → ContMDiffAt I I n (fun (y : G) => Inv.inv y) x
Inversion is
C^naway from0.
Instances For
@[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 ENat)
(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
Instances For
theorem
instContMDiffInv₀ModelWithCornersSelf
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
:
ContMDiffInv₀ (modelWithCornersSelf 𝕜 𝕜) n 𝕜
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 ENat}
(hmn : LE.le m n)
[h : ContMDiffInv₀ I n G]
:
ContMDiffInv₀ I m G
theorem
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 ENat}
[ContMDiffInv₀ I (WithTop.some Top.top) G]
[h : ENat.LEInfty a]
:
ContMDiffInv₀ I a G
theorem
instContMDiffInv₀OfTopWithTopENat
{𝕜 : 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 ENat}
[ContMDiffInv₀ I Top.top G]
:
ContMDiffInv₀ I a G
theorem
instContMDiffInv₀OfNatWithTopENatOfHasContinuousInv₀
{𝕜 : 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]
[HasContinuousInv₀ G]
:
ContMDiffInv₀ I 0 G
theorem
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]
:
ContMDiffInv₀ I 1 G
theorem
contMDiffAt_inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : Ne x 0)
:
ContMDiffAt I I n (fun (y : G) => Inv.inv y) x
@[deprecated contMDiffAt_inv₀ (since := "2024-11-21")]
theorem
smoothAt_inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : Ne x 0)
:
ContMDiffAt I I n (fun (y : G) => Inv.inv y) x
Alias of contMDiffAt_inv₀.
theorem
hasContinuousInv₀_of_hasContMDiffInv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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]
:
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")]
theorem
hasContinuousInv₀_of_hasSmoothInv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 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 ENat}
{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]
:
ContMDiffOn I I n Inv.inv (HasCompl.compl (Singleton.singleton 0))
@[deprecated contMDiffOn_inv₀ (since := "2024-11-21")]
theorem
smoothOn_inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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]
:
ContMDiffOn I I n Inv.inv (HasCompl.compl (Singleton.singleton 0))
Alias of contMDiffOn_inv₀.
@[deprecated contMDiffOn_inv₀ (since := "2024-11-21")]
theorem
SmoothOn_inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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]
:
ContMDiffOn I I n Inv.inv (HasCompl.compl (Singleton.singleton 0))
Alias of contMDiffOn_inv₀.
theorem
ContMDiffWithinAt.inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
[ContMDiffInv₀ I n G]
{s : Set M}
{a : M}
(hf : ContMDiffWithinAt I' I n f s a)
(ha : Ne (f a) 0)
:
ContMDiffWithinAt I' I n (fun (x : M) => Inv.inv (f x)) s a
theorem
ContMDiffAt.inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
[ContMDiffInv₀ I n G]
{a : M}
(hf : ContMDiffAt I' I n f a)
(ha : Ne (f a) 0)
:
ContMDiffAt I' I n (fun (x : M) => Inv.inv (f x)) a
theorem
ContMDiff.inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
[ContMDiffInv₀ I n G]
(hf : ContMDiff I' I n f)
(h0 : ∀ (x : M), Ne (f x) 0)
:
theorem
ContMDiffOn.inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
[ContMDiffInv₀ I n G]
{s : Set M}
(hf : ContMDiffOn I' I n f s)
(h0 : ∀ (x : M), Membership.mem s x → Ne (f x) 0)
:
ContMDiffOn I' I n (fun (x : M) => Inv.inv (f x)) s
@[deprecated ContMDiffWithinAt.inv₀ (since := "2024-11-21")]
theorem
SmoothWithinAt.inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
[ContMDiffInv₀ I n G]
{s : Set M}
{a : M}
(hf : ContMDiffWithinAt I' I n f s a)
(ha : Ne (f a) 0)
:
ContMDiffWithinAt I' I n (fun (x : M) => Inv.inv (f x)) s a
Alias of ContMDiffWithinAt.inv₀.
@[deprecated ContMDiffAt.inv₀ (since := "2024-11-21")]
theorem
SmoothAt.inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
[ContMDiffInv₀ I n G]
{a : M}
(hf : ContMDiffAt I' I n f a)
(ha : Ne (f a) 0)
:
ContMDiffAt I' I n (fun (x : M) => Inv.inv (f x)) a
Alias of ContMDiffAt.inv₀.
@[deprecated ContMDiffOn.inv₀ (since := "2024-11-21")]
theorem
SmoothOn.inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
[ContMDiffInv₀ I n G]
{s : Set M}
(hf : ContMDiffOn I' I n f s)
(h0 : ∀ (x : M), Membership.mem s x → Ne (f x) 0)
:
ContMDiffOn I' I n (fun (x : M) => Inv.inv (f x)) s
Alias of ContMDiffOn.inv₀.
@[deprecated ContMDiff.inv₀ (since := "2024-11-21")]
theorem
Smooth.inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
[ContMDiffInv₀ I n G]
(hf : ContMDiff I' I n f)
(h0 : ∀ (x : M), Ne (f x) 0)
:
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 ENat}
{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 : M → G}
{s : Set M}
{a : M}
(hf : ContMDiffWithinAt I' I n f s a)
(hg : ContMDiffWithinAt I' I n g s a)
(h₀ : Ne (g a) 0)
:
ContMDiffWithinAt I' I n (HDiv.hDiv f g) s a
theorem
ContMDiffOn.div₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
{s : Set M}
(hf : ContMDiffOn I' I n f s)
(hg : ContMDiffOn I' I n g s)
(h₀ : ∀ (x : M), Membership.mem s x → Ne (g x) 0)
:
ContMDiffOn I' I n (HDiv.hDiv f g) s
theorem
ContMDiffAt.div₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
{a : M}
(hf : ContMDiffAt I' I n f a)
(hg : ContMDiffAt I' I n g a)
(h₀ : Ne (g a) 0)
:
ContMDiffAt I' I n (HDiv.hDiv f g) a
theorem
ContMDiff.div₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
(hf : ContMDiff I' I n f)
(hg : ContMDiff I' I n g)
(h₀ : ∀ (x : M), Ne (g x) 0)
:
@[deprecated ContMDiffWithinAt.div₀ (since := "2024-11-21")]
theorem
SmoothWithinAt.div₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
{s : Set M}
{a : M}
(hf : ContMDiffWithinAt I' I n f s a)
(hg : ContMDiffWithinAt I' I n g s a)
(h₀ : Ne (g a) 0)
:
ContMDiffWithinAt I' I n (HDiv.hDiv f g) s a
Alias of ContMDiffWithinAt.div₀.
@[deprecated ContMDiffAt.div₀ (since := "2024-11-21")]
theorem
SmoothAt.div₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
{a : M}
(hf : ContMDiffAt I' I n f a)
(hg : ContMDiffAt I' I n g a)
(h₀ : Ne (g a) 0)
:
ContMDiffAt I' I n (HDiv.hDiv f g) a
Alias of ContMDiffAt.div₀.
@[deprecated ContMDiffOn.div₀ (since := "2024-11-21")]
theorem
SmoothOn.div₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
{s : Set M}
(hf : ContMDiffOn I' I n f s)
(hg : ContMDiffOn I' I n g s)
(h₀ : ∀ (x : M), Membership.mem s x → Ne (g x) 0)
:
ContMDiffOn I' I n (HDiv.hDiv f g) s
Alias of ContMDiffOn.div₀.
@[deprecated ContMDiff.div₀ (since := "2024-11-21")]
theorem
Smooth.div₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ENat}
{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 : M → G}
(hf : ContMDiff I' I n f)
(hg : ContMDiff I' I n g)
(h₀ : ∀ (x : M), Ne (g x) 0)
:
Alias of ContMDiff.div₀.