inv

Mathlib.Geometry.Manifold.Algebra.LieGroup

URI: https://scilib.ai/kg/mathlib#ContMDiffAt.inv

← MathLib Explorer

English

Inverse mapping preserves ContMDiffWithinAt under a Lie group operation.

Русский

Обращение сохраняет ContMDiffWithinAt для операций над группой Ли.

LaTeX

$$ContMDiffWithinAt I' I n f s x0 → ContMDiffWithinAt I' I n (inv f) s x0$$

Lean4

@[to_additive]
theorem inv {f : M → G} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) : ContMDiffAt I' I n (fun x => (f x)⁻¹) x₀ :=
  (contMDiff_inv I n).contMDiffAt.comp x₀ hf

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

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

Разделы

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

Аффилиация

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