image_symm — Mathlib

English

Let f: P₁ → P₂ be a bijectiveContinuousAffineEquiv. Then for every subset s ⊆ P₂ the image of s under the inverse map f^{-1} equals the preimage of s under f.

Русский

Пусть f: P₁ → P₂ является биективным непрерывно аффинным эквивалентом. Тогда для любого подмножества s ⊆ P₂ образ этого множества под обратной функцией f равен прообразу s по f.

LaTeX

$$$\operatorname{Set.image}(f^{\mathrm{symm}})(s) = \operatorname{Set.preimage}(f)(s)$$$

Lean4

@[simp]
theorem image_symm (f : P₁ ≃ᴬ[k] P₂) (s : Set P₂) : f.symm '' s = f ⁻¹' s :=
  f.symm.toEquiv.image_eq_preimage _

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