Finite products of indicators of pairwise disjoint sets #
At a point x ∈ t i, a finite product ∏ j ∈ s, (t j).mulIndicator (f j) x over pairwise disjoint
sets t j reduces to its i-th factor f i x, since every other factor is 1
(Finset.prod_mulIndicator_apply_of_mem). Additively, a sum of indicators of pairwise disjoint
sets takes at x ∈ t i the value of its i-th summand (Finset.sum_indicator_apply_of_mem).
This is how step functions ∑ i, 1_{t i} • c i on a finite partition are evaluated.
theorem
Finset.prod_mulIndicator_apply_of_mem
{ι : Type u_1}
{κ : Type u_2}
{β : Type u_3}
[CommMonoid β]
{s : Finset ι}
{t : ι → Set κ}
(hs : (↑s).PairwiseDisjoint t)
{i : ι}
(hi : i ∈ s)
{x : κ}
(hx : x ∈ t i)
(f : ι → κ → β)
:
On a family of pairwise disjoint sets, a product of multiplicative indicators takes at
x ∈ t i the value of the i-th factor.
theorem
Finset.sum_indicator_apply_of_mem
{ι : Type u_1}
{κ : Type u_2}
{β : Type u_3}
[AddCommMonoid β]
{s : Finset ι}
{t : ι → Set κ}
(hs : (↑s).PairwiseDisjoint t)
{i : ι}
(hi : i ∈ s)
{x : κ}
(hx : x ∈ t i)
(f : ι → κ → β)
:
On a family of pairwise disjoint sets, a sum of indicators takes at x ∈ t i
the value of the i-th summand.