contMDiffOn_inv₀

Mathlib.Geometry.Manifold.Algebra.LieGroup

URI: https://scilib.ai/kg/mathlib#contMDiffOn_inv₀

Lean4

theorem contMDiffOn_inv₀ : ContMDiffOn I I n (Inv.inv : G → G) {0}ᶜ := fun _x hx =>
  (contMDiffAt_inv₀ hx).contMDiffWithinAt

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

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

Разделы

Аффилиация

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