image_inv — Mathlib

English

If φ is a monoid homomorphism, then the image of the inverse of a finite subset s under φ equals the inverse of the image of s under φ.

Русский

Пусть φ есть однородный гомоморфизм моноидов. Тогда образ обратного множества s под φ равен обратному образу образа s под φ.

LaTeX

$$$\varphi(s^{-1}) = (\varphi(s))^{-1}$$$

Lean4

@[to_additive]
theorem image_inv (f : F) (s : Finset α) : s⁻¹.image f = (s.image f)⁻¹ :=
  image_comm (map_inv _)

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