English
For a function f and a Set s, the image of s under f equals the image of s under f with inverse map in the target.
Русский
Образ множества s под отображением f равен образу s под отображением f и обратной картой в области назначения.
LaTeX
$$$ f '' s^{-1} = (f '' s)^{-1} $$$
Lean4
@[to_additive]
theorem image_inv [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Set α) :
f '' s⁻¹ = (f '' s)⁻¹ := by rw [← image_inv_eq_inv, ← image_inv_eq_inv]; exact image_comm (map_inv _)