symm_image_eq_preimage — Mathlib

English

For a family of sets under a C^n-diffeomorphism, the image of the union is the union of the images, preserving structure.

Русский

Для семейства множеств под C^n-диффеоморфизмом образ объединения совпадает с объединением образов, сохраняя структуру.

LaTeX

$$$h[\bigcup_i S_i] = \bigcup_i h[S_i].$$$

Lean4

theorem symm_image_eq_preimage (h : M ≃ₘ^n⟮I, J⟯ N) (s : Set N) : h.symm '' s = h ⁻¹' s :=
  h.symm.image_eq_preimage s

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