image_symm_image — Mathlib

English

For a Diffeomorph h: I ↔ J between manifolds, the image of s under h equals the image of its preimage under h, i.e., h '' (h.symm '' s) = s.

Русский

Для диффеоморфизма h: I ≃ J между многообразиями образ множества s под h равен образу его обратного образа через h.

LaTeX

$$$\text{For } h: M \to N \text{ a Diffeomorph}, \ h''(h^{-1}'' s) = s$$$

Lean4

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

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