English
The indicator on the union over a Finset of sets equals the product of indicators over each set for a function f.
Русский
Индикатор объединения по Finset равно произведению индикаторов по каждому множеству для функции f.
LaTeX
$$$\operatorname{mulIndicator}\left(\bigcup i \in s, t(i)\right) f = \prod i \in s, \operatorname{mulIndicator}(t(i)) f$$$
Lean4
@[to_additive]
theorem mulIndicator_biUnion (s : Finset ι) (t : ι → Set κ) {f : κ → β} (hs : (s : Set ι).PairwiseDisjoint t) :
mulIndicator (⋃ i ∈ s, t i) f = fun a ↦ ∏ i ∈ s, mulIndicator (t i) f a := by
induction s using Finset.cons_induction with
| empty => simp
| cons i s hi ih =>
ext j
rw [coe_cons, Set.pairwiseDisjoint_insert_of_notMem (Finset.mem_coe.not.2 hi)] at hs
classical
rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]
exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)
