image_eq_preimage — Mathlib

English

For an affine equivalence e, the image of s equals the preimage under the inverse action: e '' s = e.symm ⁻¹' s.

Русский

Для эквивалентности e верно: область образа множества s равна прообразу множества s под обратным отображением.

LaTeX

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

Lean4

protected theorem image_eq_preimage (e : P₁ ≃ᴬ[k] P₂) (s : Set P₁) : e '' s = e.symm ⁻¹' s :=
  e.toEquiv.image_eq_preimage s

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