English
Let σ : α → Type and s ⊆ α be a finite set with s, and for each a ∈ α let t(a) be a finite set. Let f: Σ a∈α σ(a) → β. Then the product over all elements of the sigma-type s.sigma t equals the iterated product over a ∈ s and b ∈ t(a): ∏_{x ∈ s.sigma t} f(x) = ∏_{a ∈ s} ∏_{b ∈ t(a)} f(⟨a,b⟩).
Русский
Пусть σ : α → Type, s — конечное множество над α, и для каждого a ∈ α задано конечное множество t(a). Пусть f: Σ a∈α σ(a) → β. Тогда произведение по всем элементам сигма-типа равно повторному произведению по каждому a∈s и b∈t(a): ∏_{x∈s.sigma t} f(x) = ∏_{a∈s} ∏_{b∈t(a)} f(⟨a,b⟩).
LaTeX
$$$$\\prod_{x \\in s.\\sigma t} f(x) = \\prod_{a \\in s} \\prod_{b \\in t(a)} f\\langle a,b\\rangle.$$$$
Lean4
/-- The product over a sigma type equals the product of the fiberwise products.
For rewriting in the reverse direction, use `Finset.prod_sigma'`.
See also `Fintype.prod_sigma` for the product over the whole type. -/
@[to_additive /-- The sum over a sigma type equals the sum of the fiberwise sums. For rewriting
in the reverse direction, use `Finset.sum_sigma'`.
See also `Fintype.sum_sigma` for the sum over the whole type. -/
]
theorem prod_sigma {σ : α → Type*} (s : Finset α) (t : ∀ a, Finset (σ a)) (f : Sigma σ → β) :
∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩ := by
simp_rw [← disjiUnion_map_sigma_mk, prod_disjiUnion, prod_map, Function.Embedding.sigmaMk_apply]
