symm_toDiffeomorph

Mathlib.Geometry.Manifold.Diffeomorph

URI: https://scilib.ai/kg/mathlib#ContinuousLinearEquiv.symm_toDiffeomorph

English

For a suitable n-diffeomorphism h, ContMDiffOn of h ∘ f equals ContMDiffOn of f under the transformed coordinates.

Русский

Для подходящего n-диффеоморфизма h ContMDiffOn(h ∘ f) равен ContMDiffOn(f) после преобразования координат.

LaTeX

$$ContMDiffOn I' J m (h ∘ f) s ↔ ContMDiffOn I' I m f s$$

Lean4

@[simp]
theorem symm_toDiffeomorph : e.symm.toDiffeomorph = e.toDiffeomorph.symm :=
  rfl

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

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

Разделы

Аффилиация

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