image_eq_preimage — Mathlib

English

For any subset S of M, the image under h is the same as the preimage under h.symm of S, properly interpreted.

Русский

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

LaTeX

$$$h[S] = (h.symm)^{-1}[S].$$$

Lean4

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

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