image_uncurry_product

Mathlib.Data.Finset.NAry

URI: https://scilib.ai/kg/mathlib#Finset.image_uncurry_product

English

The curry correspondence for image₂: image₂ (curry f) s t = (s ×ˢ t).image f.

Русский

Кари для image₂ через карри: image₂ (curry f) s t = (s ×ˢ t).image f.

LaTeX

$$$\mathrm{image}_2\ (\mathrm{Function.curry}\ f)\ s\ t = (s \times\!\!\ˢ t).\mathrm{image}\ f$$$

Lean4

@[simp]
theorem image_uncurry_product (f : α → β → γ) (s : Finset α) (t : Finset β) :
    (s ×ˢ t).image (uncurry f) = image₂ f s t :=
  rfl

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

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

Разделы

Аффилиация

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