preimage_equiv_eq_image_symm — Mathlib

English

Alias: Set.preimage_eq_image_symm for a bijection f: β ≃ α expresses the reverse equality to image_eq_preimage.

Русский

Псевдоним: Set.preimage_eq_image_symm для биекции f: β ≃ α выражает обратное равенство image_eq_preimage.

LaTeX

$$$\text{Set.preimage} (e) S = \text{Set.image} (e^{-1}) S.$$$

Lean4

/-- Alias for `Equiv.image_eq_preimage` -/
theorem _root_.Set.preimage_equiv_eq_image_symm {α β} (S : Set α) (f : β ≃ α) : f ⁻¹' S = f.symm '' S :=
  (f.symm.image_eq_preimage S).symm

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