1 Finset
1.1 Piecewise
Let \(s, t\) be finite sets of indices in \(\iota \), and let \(f \colon \iota \to M\). Then
\[ \prod _{x \in s} \begin{cases} 1, & \text{if } x \in t, \\ f(x), & \text{otherwise} \end{cases} = \prod _{x \in s \setminus t} f(x). \]
Proof
We split the product over the disjoint union \(s = (s \setminus t) \cup (s \cap t)\).
\begin{align*} \prod _{x \in s} \begin{cases} 1, & \text{if } x \in t \\ f(x), & \text{otherwise} \end{cases}& = \left( \prod _{x \in s \setminus t} f(x) \right) \cdot \left( \prod _{x \in s \cap t} 1 \right) \\ & = \prod _{x \in s \setminus t} f(x). \end{align*}
The first equality holds because for any \(x \in s \setminus t\), the term is \(f(x)\), while for any \(x \in s \cap t\), the term is \(1\). The product of ones is one.
Let \(s, t\) be finite sets of indices in \(\iota \), and let \(f \colon \iota \to A\) be a function to an additive commutative monoid. Then
\[ \sum _{x \in s} \begin{cases} 0, & \text{if } x \in t, \\ f(x), & \text{otherwise} \end{cases} = \sum _{x \in s \setminus t} f(x). \]
Proof
We split the sum over the disjoint union \(s = (s \setminus t) \cup (s \cap t)\).
\begin{align*} \sum _{x \in s} \begin{cases} 0, & \text{if } x \in t \\ f(x), & \text{otherwise} \end{cases}& = \left( \sum _{x \in s \setminus t} f(x) \right) + \left( \sum _{x \in s \cap t} 0 \right) \\ & = \sum _{x \in s \setminus t} f(x). \end{align*}
The first equality holds because for any \(x \in s \setminus t\), the term is \(f(x)\), while for any \(x \in s \cap t\), the term is \(0\). The sum of zeros is zero.