image_eq_preimage_symm — Mathlib

English

For a relation isomorphism e: r ≃r s and a set t, the image of t under e equals the preimage of t under the inverse isomorphism.

Русский

Для изоморфизма отношения e: r ≃r s и множества t образ mапирования e совпадает с предобразом t под обратным изоморфизмом.

LaTeX

$$$ e'' t = e.symm^{-1}'' t $$$

Lean4

theorem image_eq_preimage_symm (e : r ≃r s) (t : Set α) : e '' t = e.symm ⁻¹' t :=
  e.toEquiv.image_eq_preimage t

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