image_eq_preimage — Mathlib

English

For any bijection e: α ≃ β and any set S ⊆ α, the image of S under e equals the preimage of S under e⁻¹.

Русский

Для биекции e: α ≃ β и любого множества S ⊆ α образ S под действием e равен прообразу S под действием e⁻¹.

LaTeX

$$$\operatorname{image}(e)\,S = \operatorname{preimage}(e^{-1})\,S.$$$

Lean4

protected theorem image_eq_preimage {α β} (e : α ≃ β) (s : Set α) : e '' s = e.symm ⁻¹' s :=
  Set.ext fun _ => mem_image_iff_of_inverse e.left_inv e.right_inv

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