English
If f is ContMDiffWithinAt on s at x0, then the map x ↦ f(x)^{-1} is ContMDiffWithinAt on s at x0.
Русский
Если f гладко дифференцируема в пределах s около x0, то x ↦ f(x)^{-1} гладко дифференцируема в пределах s около x0.
LaTeX
$$ContMDiffWithinAt I' I n f s x0 → ContMDiffWithinAt I' I n (fun x => (f x)^{-1}) s x0$$
Lean4
/-- A Lie group is a topological group. This is not an instance for technical reasons,
see note [Design choices about smooth algebraic structures]. -/
@[to_additive /-- 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 : IsTopologicalGroup G :=
{ continuousMul_of_contMDiffMul I n with continuous_inv := (contMDiff_inv I n).continuous }
