We prove each direction separately. For the forward direction, assume \(\chi _S(i) = 1\). By definition of \(\chi _S\), we unfold the characteristic vector. We split on whether \(i \in S\): if \(i \in S\), we are done; if \(i \notin S\), then \(\chi _S(i) = 0\), contradicting \(\chi _S(i) = 1\) by simplification. For the reverse direction, assume \(i \in S\). Then by definition \(\chi _S(i) = 1\), and this follows by simplification using the membership hypothesis.

We prove each direction separately. For the forward direction, assume \(\chi _S(i) = 0\). Unfolding the definition of the characteristic vector and splitting on membership: if \(i \in S\), then \(\chi _S(i) = 1\), contradicting \(\chi _S(i) = 0\) by simplification; if \(i \notin S\), we are done. For the reverse direction, assume \(i \notin S\). Then by definition \(\chi _S(i) = 0\), which follows by simplification.

By extensionality, it suffices to show equality for an arbitrary element \(i\). We simplify the left-hand side using the pointwise addition definition and the characteristic vector definition, and the right-hand side using the membership condition for symmetric difference. We then perform a case split on whether \(i \in S\) and whether \(i \in T\):

• If \(i \in S\) and \(i \in T\): the left-hand side is \(1 + 1 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\), and the right-hand side is \(0\) since \(i \notin S \mathbin {\triangle } T\).

• If \(i \in S\) and \(i \notin T\): both sides equal \(1\) by simplification.

• If \(i \notin S\) and \(i \in T\): both sides equal \(1\) by simplification.

• If \(i \notin S\) and \(i \notin T\): both sides equal \(0\) by simplification.

This is the symmetric form of the previous theorem, obtained by applying symmetry to \(\chi _S + \chi _T = \chi _{S \mathbin {\triangle } T}\).

Rewriting using the addition-symmetric difference correspondence, \(\chi _S + \chi _S = \chi _{S \mathbin {\triangle } S}\). Since \(S \mathbin {\triangle } S = \emptyset \), we have \(\chi _\emptyset = 0\).

By extensionality, it suffices to show \((-\chi _S)(i) = \chi _S(i)\) for each \(i\). We simplify the negation and unfold the characteristic vector definition, then split on whether \(i \in S\). In both cases (\(\chi _S(i) = 1\) or \(\chi _S(i) = 0\)), the result follows by computation (deciding) in \(\mathbb {Z}/2\mathbb {Z}\), since \(-1 = 1\) and \(-0 = 0\) in this ring.

By extensionality, \(i \in \mathrm{fromBinaryVector}(\chi _S)\) iff \(\chi _S(i) = 1\). By the characteristic vector membership characterization, this is equivalent to \(i \in S\). The result follows by simplification.

By extensionality, it suffices to show equality at each coordinate \(i\). We unfold the definitions of the characteristic vector and \(\mathrm{fromBinaryVector}\). Since every element of \(\mathbb {Z}/2\mathbb {Z}\) is either \(0\) or \(1\), we decompose \(v(i)\) into these two cases. In each case, the result follows by simplification: if \(v(i) = 0\), then \(i \notin \mathrm{fromBinaryVector}(v)\), so \(\chi (i) = 0 = v(i)\); if \(v(i) = 1\), then \(i \in \mathrm{fromBinaryVector}(v)\), so \(\chi (i) = 1 = v(i)\).

Let \(S, T\) be finsets with \(\chi _S = \chi _T\). By extensionality, we need to show \(i \in S \iff i \in T\) for all \(i\). Using the membership characterization, \(i \in S \iff \chi _S(i) = 1 \iff \chi _T(i) = 1 \iff i \in T\), where the middle equivalence follows from \(\chi _S = \chi _T\).

Given a binary vector \(v\), take \(S = \mathrm{fromBinaryVector}(v)\). Then \(\chi _S = v\) by the round-trip property, which follows by simplification.

This follows directly from injectivity and surjectivity of the characteristic vector map.

We unfold the definition of addition on finsets (which is symmetric difference), and the result follows directly from the symmetric difference correspondence theorem.

We decompose \(c\) into the cases \(c = 0\) and \(c = 1\) (the only elements of \(\mathbb {Z}/2\mathbb {Z}\)).

Case \(c = 0\): We substitute \(c = 0\). The left-hand side becomes \(\chi _{0 \cdot S} = \chi _\emptyset = 0\). For the right-hand side, by extensionality at each coordinate \(i\), we simplify \(0 \cdot \chi _S(i)\) using the zero scalar action and verify it equals \(0\) by the symmetry of \(0 \cdot x = 0\).

Case \(c = 1\): We substitute \(c = 1\). The left-hand side becomes \(\chi _{1 \cdot S} = \chi _S\). For the right-hand side, by extensionality at each coordinate \(i\), we use \(1 \cdot \chi _S(i) = \chi _S(i)\) by the symmetry of \(1 \cdot x = x\).

Rewriting using the addition-symmetric difference correspondence, it suffices to show \(S \cup T = S \mathbin {\triangle } T\). Since \(S\) and \(T\) are disjoint, the symmetric difference equals the union, which follows from the lemma that disjoint symmetric difference equals the supremum (union).

Let \(i\) be arbitrary. We unfold the definition of the characteristic vector using the membership condition for intersections. We perform a case split on whether \(i \in S\) and whether \(i \in T\):

• If \(i \in S\) and \(i \in T\): both sides equal \(1 \cdot 1 = 1\).

• If \(i \in S\) and \(i \notin T\): both sides equal \(1 \cdot 0 = 0\).

• If \(i \notin S\) and \(i \in T\): both sides equal \(0 \cdot 1 = 0\).

• If \(i \notin S\) and \(i \notin T\): both sides equal \(0 \cdot 0 = 0\).

All cases follow by simplification.

By extensionality, it suffices to verify at each coordinate \(i\). We unfold the definitions of \(\mathbf{1}\), pointwise addition, and the characteristic vector, using the membership condition for complements. We split on whether \(i \in S^c\): if \(i \notin S\) then \(\chi _{S^c}(i) = 1\) and \(1 + 0 = 1\); if \(i \in S\) then \(\chi _{S^c}(i) = 0\) and \(1 + 1 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\). Both cases are verified by computation.

We split the sum over the universe into a sum over elements in \(S\) and a sum over elements not in \(S\): \(\sum _{i \in \alpha } \mathrm{val}(\chi _S(i)) = \sum _{i \in S} \mathrm{val}(\chi _S(i)) + \sum _{i \notin S} \mathrm{val}(\chi _S(i))\). We first observe that \(\{ i \in \alpha \mid i \in S\} = S\) by extensionality and simplification. For the first sum: for each \(i \in S\), \(\chi _S(i) = 1\), so \(\mathrm{val}(\chi _S(i)) = 1\), hence \(\sum _{i \in S} 1 = |S|\) (rewriting the cardinality as a sum of ones). For the second sum: for each \(i \notin S\), \(\chi _S(i) = 0\), so \(\mathrm{val}(\chi _S(i)) = 0\), hence the sum is \(0\). Combining by integer arithmetic (omega), \(|S| = |S| + 0\).

The forward direction follows by rewriting: if \(S = T\) then \(\chi _S = \chi _T\). The reverse direction follows from injectivity of the characteristic vector map: if \(\chi _S = \chi _T\) then \(S = T\).

We use the standard cardinality identity \(|S \cup T| + |S \cap T| = |S| + |T|\) (Finset.card_union_add_card_inter). We then establish that \(S \mathbin {\triangle } T = (S \cup T) \setminus (S \cap T)\) by extensionality: \(x \in S \mathbin {\triangle } T\) iff \(x \in (S \cup T) \setminus (S \cap T)\), which follows by unfolding the definitions and applying propositional logic (tauto). Since \(S \cap T \subseteq S \cup T\) (by Finset.inter_subset_union), we apply the cardinality of set difference for subsets: \(|S \mathbin {\triangle } T| = |S \cup T| - |S \cap T|\). We also have \(|S \cap T| \le |S \cup T|\) (by monotonicity of cardinality). The desired identity \(|S \mathbin {\triangle } T| + 2|S \cap T| = |S| + |T|\) then follows by integer arithmetic (omega) from these three facts.