instCoeContMDiffMap

Mathlib.Geometry.Manifold.Diffeomorph

URI: https://scilib.ai/kg/mathlib#Diffeomorph.instCoeContMDiffMap

English

The coe (coercion) from a diffeomorphism to an Equiv is the identity on the underlying function.

Русский

Сопоставление отображает одну и ту же функцию без изменений.

LaTeX

$$$$ \text{coe_toEquiv}(h) = h. $$$$

Lean4

instance : Coe (M ≃ₘ^n⟮I, I'⟯ M') C^n⟮I, M; I', M'⟯ :=
  ⟨toContMDiffMap⟩

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

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

Разделы

Аффилиация

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