image_inv — Mathlib

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 _)

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