apply_symm_apply

Mathlib.Geometry.Manifold.Diffeomorph

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

English

If h maps M to N, then h.symm maps N back to M, preserving differentiability class.

Русский

Если h переводит M в N, то h.symm переводит N обратно в M, сохраняя класс гладкости.

LaTeX

$$$h: M \simeq^n_I^J N \Rightarrow h^{-1} : N \simeq^n_J^I M.$$$

Lean4

@[simp]
theorem apply_symm_apply (h : M ≃ₘ^n⟮I, J⟯ N) (x : N) : h (h.symm x) = x :=
  h.toEquiv.apply_symm_apply x

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

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

Разделы

Аффилиация

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