image_inv — Mathlib

English

If f is bijective on s, then its inverse is bijective on s as well; i.e., the inverse image equals the image for restricted sets.

Русский

Если f ограничено на s и является биекцией, то и f^{-1} ограничено на s; то есть образ и прообраз совпадают для ограниченного множества.

LaTeX

$$If $f|_s$ is bijective, then $f^{-1}|_s$ is bijective.$$

Lean4

@[simp]
theorem image_inv (f : Perm α) (s : Set α) : ↑f⁻¹ '' s = f ⁻¹' s :=
  f⁻¹.image_eq_preimage _

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