English
Let s be a finite set and t: s → Finset ι assign to each element a finite set. If the family {t x | x ∈ s} is pairwise disjoint, then the product over the biUnion of these Finsets equals the iterated product over s of the inner Finsets:
Русский
Пусть s — конечное множество, а t — отображение s в Finset ι. Предположим, что семейство {t x} состоит из попарно несовмещённых множеств. Тогда произведение по biUnion t равно последовательному произведению по s и по каждому t x:
LaTeX
$$$\displaystyle \prod x \in s.biUnion t, f(x) = \prod x \in s, \prod i \in t(x), f(i)$$$
Lean4
@[to_additive]
theorem prod_biUnion [DecidableEq ι] {s : Finset κ} {t : κ → Finset ι} (hs : Set.PairwiseDisjoint (↑s) t) :
∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i := by rw [← disjiUnion_eq_biUnion _ _ hs, prod_disjiUnion]
