image_vsub_prod

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

image (x ↦ x.fst -ᵥ x.snd) (s × t) = s -ᵥ t

Русский

image (x ↦ x.fst -ᵥ x.snd) (s × t) = s -ᵥ t

LaTeX

$$$ \\mathrm{image} (\\lambda x. x_{\\mathrm{fst}} -ᵥ x_{\\mathrm snd}) (s \\times t) = s -ᵥ t $$$

Lean4

theorem image_vsub_prod : (fun x : β × β ↦ x.fst -ᵥ x.snd) '' s ×ˢ t = s -ᵥ t :=
  image_prod _

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

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

Разделы

Аффилиация

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