mul — Mathlib

English

The pointwise product of two subsets s and t is defined as {xy | x ∈ s, y ∈ t}.

Русский

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

LaTeX

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

Lean4

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

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