smul — Mathlib

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₂ (· • ·)⟩

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