smul — Mathlib

English

The pointwise scalar multiplication of sets s and t is defined as { x • y | x ∈ s, y ∈ t }.

Русский

Точечное скалярное умножение множеств s и t определяется как { x • y | x ∈ s, y ∈ t }.

LaTeX

$$$$ s \cdot t = \{ x \cdot y : x \in s, y \in t \} $$$$

Lean4

/-- The pointwise scalar multiplication of sets `s • t` is defined as `{x • y | x ∈ s, y ∈ t}` in
scope `Pointwise`. -/
@[to_additive /-- The pointwise scalar addition of sets `s +ᵥ t` is defined as `{x +ᵥ y | x ∈ s, y ∈ t}` in locale
    `Pointwise`. -/
    ]
protected def smul [SMul α β] : SMul (Set α) (Set β) where smul := image2 (· • ·)

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