coe_toDiffeomorph_symm

Mathlib.Geometry.Manifold.Diffeomorph

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

English

For a fixed n-diffeomorphism h, ContMDiff of h ∘ f equals ContMDiff of f in the usual coordinates.

Русский

Для фиксированного n-диффеоморфизма h ContMDiff(h ∘ f) равен ContMDiff(f).

LaTeX

$$ContMDiff I' J m (h ∘ f) ↔ ContMDiff I' I m f$$

Lean4

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

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

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

Разделы

Аффилиация

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