image_smul_prod

Mathlib.Algebra.Group.Pointwise.Set.Scalar

URI: https://scilib.ai/kg/mathlib#Set.image_smul_prod

English

The image of s × t under the map (a,b) ↦ a • b equals the product set s • t.

Русский

Образ через отображение (a,b) ↦ a • b множества s × t равен множеству s • t.

LaTeX

$$$$ \{ a \cdot b : a \in s, b \in t \} = s \cdot t $$$$

Lean4

@[to_additive vadd_image_prod]
theorem image_smul_prod : (fun x : α × β ↦ x.fst • x.snd) '' s ×ˢ t = s • t :=
  image_prod _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru