prodMap_image_product

Mathlib.Data.Finset.Prod

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

← MathLib Explorer

English

If a ∈ s and b ∈ t then (a,b) ∈ s ×ˢ t.

Русский

Если a ∈ s и b ∈ t, то (a,b) ∈ s ×ˢ t.

LaTeX

$$$(ha : a \in s) (hb : b \in t) \Rightarrow (a,b) \in s ×ˢ t$$

Lean4

theorem prodMap_image_product {δ : Type*} [DecidableEq β] [DecidableEq δ] (f : α → β) (g : γ → δ) (s : Finset α)
    (t : Finset γ) : (s ×ˢ t).image (Prod.map f g) = s.image f ×ˢ t.image g :=
  mod_cast Set.prodMap_image_prod f g s t

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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