English
If (t i) is a pairwise disjoint family of finite sets indexed by a finite type, then the product over the union equals the product over i of the products over t i.
Русский
Если семейство парно непересекающихся концевых множеств t i индексируемо конечным типом, то произведение по объединению равно произведению по i от внутренних произведений.
LaTeX
$$$\\prod^\\!a \\in \\bigcup_{i} t_i f(a) = \\prod^\\!i \\in I, \\prod^\\!a \\in t_i f(a)$$$
Lean4
/-- Given a family of pairwise disjoint finite sets `t i` indexed by a finite type, the product of
`f a` over the union `⋃ i, t i` is equal to the product over all indexes `i` of the products of
`f a` over `a ∈ t i`. -/
@[to_additive /-- Given a family of pairwise disjoint finite sets `t i` indexed by a finite type, the
sum of `f a` over the union `⋃ i, t i` is equal to the sum over all indexes `i` of the
sums of `f a` over `a ∈ t i`. -/
]
theorem finprod_mem_iUnion [Finite ι] {t : ι → Set α} (h : Pairwise (Disjoint on t)) (ht : ∀ i, (t i).Finite) :
∏ᶠ a ∈ ⋃ i : ι, t i, f a = ∏ᶠ i, ∏ᶠ a ∈ t i, f a :=
by
cases nonempty_fintype ι
lift t to ι → Finset α using ht
classical
rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset, Finset.prod_biUnion]
· simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]
· exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)
