image_inv_eq_inv — Mathlib

English

The inverse of a set equals the image of the inverse function, i.e., image of inverse equals inverse of image.

Русский

Обратное множества равно образу функции обратного значения.

LaTeX

$$$ \mathrm{image} (x \mapsto x^{-1}) (s) = s^{-1} $$$

Lean4

@[to_additive (attr := simp)]
theorem image_inv_eq_inv : (·⁻¹) '' s = s⁻¹ :=
  congr_fun (image_eq_preimage_of_inverse inv_involutive.leftInverse inv_involutive.rightInverse) _

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