image_smul_set — Mathlib

English

For a general action-homomorphism f between α and β with M-action, the image of the smul of a set s by c equals the smul of the image of s by c: f '' (c • s) = c • f '' s.

Русский

Для общего отображения-хомоморфизма f между пространствами с действием M, образ умножения множества s на c равен умножению образа s тем же элементом: f '' (c • s) = c • f '' s.

LaTeX

$$f''(c \cdot s) = c \cdot f''(s)$$

Lean4

@[to_additive]
theorem image_smul_set (f : F) (c : M) (s : Set α) : f '' (c • s) = c • f '' s :=
  image_smul_setₛₗ f c s

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