image_uncurry_prod

Mathlib.Data.Set.NAry

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

English

The image of the uncurry of f on s × t equals image2 f s t.

Русский

Образ раскрученного по парам отображения равен image2 f s t.

LaTeX

$$uncurry f '' s ×ˢ t = image2 f s t.$$

Lean4

@[simp]
theorem image_uncurry_prod (s : Set α) (t : Set β) : uncurry f '' s ×ˢ t = image2 f s t :=
  image_prod _

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

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

Разделы

Аффилиация

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