instContinuousMapClassSomeENatTop

Mathlib.Geometry.Manifold.Diffeomorph

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

English

The refl diffeomorphism is the identity on the domain; it maps each point to itself.

Русский

Тождественный диффеоморфизм переводит каждую точку в саму себя.

LaTeX

$$$\text{Diffeomorph.refl } I\, M\, n \text{ acts as the identity on } M.$$$

Lean4

instance : ContinuousMapClass (M ≃ₘ⟮I, J⟯ N) M N where map_continuous f := f.continuous

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

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

Разделы

Аффилиация

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