coe_toHomeomorph_symm

Mathlib.Geometry.Manifold.Diffeomorph

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

English

The function underlying h.toHomeomorph.symm is h.symm.

Русский

Функция, лежащая в основе h.toHomeomorph.symm, равна h.symm.

LaTeX

$$$\\uparrow(h^{\\text{Homeomorph}}.symm) = h.symm$$$

Lean4

@[simp]
theorem coe_toHomeomorph_symm (h : M ≃ₘ^n⟮I, J⟯ N) : ⇑h.toHomeomorph.symm = h.symm :=
  rfl

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

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

Разделы

Аффилиация

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