English
If I is a finite set of indices and t : I → Set α with pairwise disjoint t i and each t i finite, then the product over a ∈ ⋃ i∈I t i equals the product over i∈I of the products over a ∈ t i.
Русский
Если I — конечное множество индексов, а t i — попарно непересекающиеся конечные множества, то произведение по объединению равно произведению по индексам.
LaTeX
$$$\\prod^\\!a \\in \\bigcup_{i\\in I} t(i) f(a) = \\prod^\\!i\\in I, \\prod^\\!a\\in t(i) f(a)$$$
Lean4
/-- Given a family of sets `t : ι → Set α`, a finite set `I` in the index type such that all sets
`t i`, `i ∈ I`, are finite, if all `t i`, `i ∈ I`, are pairwise disjoint, then the product of `f a`
over `a ∈ ⋃ i ∈ I, t i` is equal to the product over `i ∈ I` of the products of `f a` over
`a ∈ t i`. -/
@[to_additive /-- Given a family of sets `t : ι → Set α`, a finite set `I` in the index type such that
all sets `t i`, `i ∈ I`, are finite, if all `t i`, `i ∈ I`, are pairwise disjoint, then the
sum of `f a` over `a ∈ ⋃ i ∈ I, t i` is equal to the sum over `i ∈ I` of the sums of `f a`
over `a ∈ t i`. -/
]
theorem finprod_mem_biUnion {I : Set ι} {t : ι → Set α} (h : I.PairwiseDisjoint t) (hI : I.Finite)
(ht : ∀ i ∈ I, (t i).Finite) : ∏ᶠ a ∈ ⋃ x ∈ I, t x, f a = ∏ᶠ i ∈ I, ∏ᶠ j ∈ t i, f j :=
by
haveI := hI.fintype
rw [biUnion_eq_iUnion, finprod_mem_iUnion, ← finprod_set_coe_eq_finprod_mem]
exacts [fun x y hxy => h x.2 y.2 (Subtype.coe_injective.ne hxy), fun b => ht b b.2]
