smul_setₛₗ — Mathlib

English

If MapsTo f s t holds, then for every c ∈ M, MapsTo f (c • s) (σ c • t) holds as well; smul preserves mapping of sets.

Русский

Если f отображает множество s в t (MapsTo f s t), то отображение сохраняется после умножения на c: MapsTo f (c • s) (σ c • t).

LaTeX

$$$\text{MapsTo} f (c \cdot s) (\sigma(c) \cdot t)$$$

Lean4

@[to_additive]
theorem smul_setₛₗ (hst : MapsTo f s t) (c : M) : MapsTo f (c • s) (σ c • t) :=
  Function.Semiconj.mapsTo_image_right (map_smulₛₗ _ _) hst

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