toEquiv_coe_symm

Mathlib.Geometry.Manifold.Diffeomorph

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

English

For a subset S of M, the image of S under h equals the preimage under h.symm of S.

Русский

Для подмножества S множества M образ S под действием h равен предобразу S под действием h.symm.

LaTeX

$$$h[S] = h^{-1}[S]$ under the appropriate interpretation of h and h.symm.$$

Lean4

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

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

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

Разделы

Аффилиация

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