instLieGroupOfNatWithTopENat — Mathlib

English

In a Lie group, the inversion map x ↦ x^{-1} is C^n for any n, i.e., is continuously differentiable to all orders in the chosen smoothness class.

Русский

На Lie-группе отображение обращения x ↦ x^{-1} является C^n для любого n, то есть бесконечно гладко.

LaTeX

$$$\text{contMDiffInv}(I,n): x \mapsto x^{-1}$ is $C^n$ on $G$.$$

Lean4

@[to_additive]
instance [LieGroup I 2 G] : LieGroup I 1 G :=
  LieGroup.of_le one_le_two

Похожие утверждения