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