image_smul_setₛₗ — Mathlib

English

Let f be a MulActionSemiHomClass map with σ: M →* N. For any c ∈ M and any set s ⊆ α, the image of c • s under f equals σ(c) • the image of s: f '' (c • s) = σ c • f '' s.

Русский

Пусть f является полуподстановкой между действиями с σ: M →* N. Тогда образ множества c • s под действием f равен σ(c) умножению образа s: f '' (c • s) = σ c • f '' s.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem image_smul_setₛₗ (f : F) (c : M) (s : Set α) : f '' (c • s) = σ c • f '' s :=
  Semiconj.set_image (map_smulₛₗ f c) s

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