image2_smul — Mathlib

English

The image of the product set under the multiplication map coincides with the pointwise product: image2 (•) s t = s • t.

Русский

Образ множества произведения под отображением умножения совпадает с точечным произведением: image2 (•) s t = s • t.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem image2_smul : image2 (· • ·) s t = s • t :=
  rfl

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