English
Let s be a finite set, t a function assigning finite sets, and h a disjointness condition; the product over the disjoint union s disjiUnion t h equals the product over i of the product over x in t(i).
Русский
Пусть s — конечное множество, t — функция, сопоставляющая ему множества, и h — условие дизjointности; произведение по disjiUnion равно произведению по внутренним произведениям.
LaTeX
$$$\\prod_{x \\in s \\disjiUnion t\\; h} f(x) = \\prod_{i \\in s} \\left( \\prod_{x \\in t(i)} f(x) \\right)$$$
Lean4
@[to_additive]
theorem prod_disjiUnion (s : Finset κ) (t : κ → Finset ι) (h) : ∏ x ∈ s.disjiUnion t h, f x = ∏ i ∈ s, ∏ x ∈ t i, f x :=
by
refine Eq.trans ?_ (fold_disjiUnion h)
dsimp [Finset.prod, Multiset.prod, Multiset.fold, Finset.disjUnion, Finset.fold]
congr
exact prod_const_one.symm
