continuousInv₀_of_contMDiffInv₀

Mathlib.Geometry.Manifold.Algebra.LieGroup

URI: https://scilib.ai/kg/mathlib#continuousInv₀_of_contMDiffInv₀

Lean4

/-- 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 continuousInv₀_of_contMDiffInv₀ : ContinuousInv₀ G :=
  { continuousAt_inv₀ := fun _ hx ↦ (contMDiffAt_inv₀ (I := I) (n := n) hx).continuousAt }

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru