image_preimage — Mathlib

English

For any e, the image of the inverse of s equals s mapped back: e '' (e ⁻¹' s) = s.

Русский

Для любого e верно, что образ обратного отображения множества s равен самому множество s.

LaTeX

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

Lean4

@[simp]
theorem image_preimage (e : P₁ ≃ᴬ[k] P₂) (s : Set P₂) : e '' (e ⁻¹' s) = s :=
  e.surjective.image_preimage s

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