mul — Mathlib

English

The pointwise product s * t is defined as {x*y | x ∈ s, y ∈ t}.

Русский

Пусть s и t — конечные множества; их покомпонентное произведение определяется как {xy | x ∈ s, y ∈ t}.

LaTeX

$$$s * t = \{ x y \mid x \in s, y \in t \}$$$

Lean4

/-- The pointwise multiplication of finsets `s * t` and `t` is defined as `{x * y | x ∈ s, y ∈ t}`
in scope `Pointwise`. -/
@[to_additive /-- The pointwise addition of finsets `s + t` is defined as `{x + y | x ∈ s, y ∈ t}` in
      scope `Pointwise`. -/
    ]
protected def mul : Mul (Finset α) :=
  ⟨image₂ (· * ·)⟩

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