image_smul_product — Mathlib

English

The image of the cartesian product s × t under (x, y) ↦ x • y equals the pointwise product s • t.

Русский

Образ декартова произведения s × t под отображением (x, y) ↦ x • y равен точечному произведению s • t.

LaTeX

$$$ ((s \times\! t).\mathrm{image} (\\lambda p: p.1 \cdot p.2)) = s \cdot t $$$

Lean4

@[to_additive]
theorem image_smul_product : ((s ×ˢ t).image fun x : α × β => x.fst • x.snd) = s • t :=
  rfl

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