smulSet — Mathlib

English

The dilation of a set s by a scalar a is the image of s under the map y ↦ a • y.

Русский

Расширение множества s скаляром a — это образ множества s при отображении y ↦ a • y.

LaTeX

$$$$ \mathrm{smulSet}(a,s) = \{ a \cdot y : y \in s \} $$$$

Lean4

/-- The dilation of set `x • s` is defined as `{x • y | y ∈ s}` in scope `Pointwise`. -/
@[to_additive /-- The translation of set `x +ᵥ s` is defined as `{x +ᵥ y | y ∈ s}` in scope `Pointwise`. -/
    ]
protected def smulSet [SMul α β] : SMul α (Set β) where smul a := image (a • ·)

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