English
The pointwise product of two Finsets s ⊆ α and t ⊆ β is defined by s • t = { x • y | x ∈ s, y ∈ t }. This equals the image₂ of s and t under the action.
Русский
Точечное произведение двух конечных множеств s ⊆ α и 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 product of two finsets `s` and `t`: `s • t = {x • y | x ∈ s, y ∈ t}`. -/
@[to_additive /-- The pointwise sum of two finsets `s` and `t`: `s +ᵥ t = {x +ᵥ y | x ∈ s, y ∈ t}`. -/
]
protected def smul : SMul (Finset α) (Finset β) :=
⟨image₂ (· • ·)⟩