English
Let σ : α → Type, s ⊆ α finite, t(a) finite for each a, and f(a) : σ(a) → β. Then ∏_{x ∈ s.sigma t} f x.1 x.2 equals ∏_{a ∈ s} ∏_{b ∈ t(a)} f(a,b).
Русский
Пусть σ : α → Type, s — конечное множество над α, t(a) — конечное множество для каждого a, и f(a) : σ(a) → β. Тогда ∏_{x ∈ s.sigma t} f x.1 x.2 = ∏_{a ∈ s} ∏_{b ∈ t(a)} f(a,b).
LaTeX
$$$$\\prod_{x \in s.\\sigma t} f(x.1, x.2) = \\prod_{a \\in s} \\prod_{b \\in t(a)} f(a,b). $$$$
Lean4
/-- The product over a sigma type equals the product of the fiberwise products. For rewriting
in the reverse direction, use `Finset.prod_sigma`. -/
@[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` -/
]
theorem prod_sigma' {σ : α → Type*} (s : Finset α) (t : ∀ a, Finset (σ a)) (f : ∀ a, σ a → β) :
(∏ a ∈ s, ∏ s ∈ t a, f a s) = ∏ x ∈ s.sigma t, f x.1 x.2 :=
Eq.symm <| prod_sigma s t fun x => f x.1 x.2
