ThmDex – An index of mathematical definitions, results, and conjectures.

Result R4552 on D41: Indicator function
Subresult of R2369: Expressing a countably infinite pointwise sum of indicator functions in terms of set cardinality

Expressing a finite pointwise sum of indicator functions in terms of set cardinality