symm_image_image — Mathlib

English

Let h be a diffeomorphism between spaces M and N. Then for every subset S of M, the inverse image of the image of S under h equals S; in symbols, h^{-1}[h[S]] = S.

Русский

Пусть h — диффеоморфизм между пространствами M и N. Тогда для любого множества S ⊆ M выполняется {h[S]} под обратным отображением возвращает S; то есть h^{-1}[h[S]] = S.

LaTeX

$$$\\forall S \\subseteq M:\\; h^{-1}[h[S]] = S$$$

Lean4

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

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