English
If t is a finite set of pairwise disjoint finite sets, then the product over ⋃ t of f a equals the product over s ∈ t of the product over a ∈ s of f a.
Русский
Если t состоит из конечного числа попарно непересекающихся конечных множеств, то произведение по ⋃ t равно произведению по элементам t.
LaTeX
$$$\\prod^\\!a \\in \\bigcup t, f(a) = \\prod^\\!s \\in t, \\prod^\\!a \\in s, f(a)$$$
Lean4
/-- If `t` is a finite set of pairwise disjoint finite sets, then the product of `f a`
over `a ∈ ⋃₀ t` is the product over `s ∈ t` of the products of `f a` over `a ∈ s`. -/
@[to_additive /-- If `t` is a finite set of pairwise disjoint finite sets, then the sum of `f a` over
`a ∈ ⋃₀ t` is the sum over `s ∈ t` of the sums of `f a` over `a ∈ s`. -/
]
theorem finprod_mem_sUnion {t : Set (Set α)} (h : t.PairwiseDisjoint id) (ht₀ : t.Finite)
(ht₁ : ∀ x ∈ t, Set.Finite x) : ∏ᶠ a ∈ ⋃₀ t, f a = ∏ᶠ s ∈ t, ∏ᶠ a ∈ s, f a :=
by
rw [Set.sUnion_eq_biUnion]
exact finprod_mem_biUnion h ht₀ ht₁
