image₂_curry

Mathlib.Data.Finset.NAry

URI: https://scilib.ai/kg/mathlib#Finset.image₂_curry

English

The order of arguments in image₂ can be swapped: image₂ f s t = image₂ (λ a b, f b a) t s.

Русский

Порядок аргументов в image₂ можно поменять: image₂ f s t = image₂ (λ a b, f b a) t s.

LaTeX

$$$\mathrm{image}_2\ f\ s\ t = \mathrm{image}_2\ (\lambda a b. f\ b\ a)\ t\ s$$$

Lean4

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

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

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

Разделы

Аффилиация

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