This holds by definition, since \(\partial S\) is defined as the filter of the edge set by the condition \(|e_{\mathrm{set}} \cap S| = 1\). Unfolding the definition of edgeBoundary and simplifying gives the equivalence directly.

By extensionality, it suffices to show that no edge \(e\) belongs to \(\partial \emptyset \). Unfolding the definition and simplifying, we note that \(e_{\mathrm{set}} \cap \emptyset = \emptyset \) for any edge \(e\), so the cardinality condition \(|e_{\mathrm{set}} \cap \emptyset | = 1\) is never satisfied.

By extensionality, we show both directions. For the forward direction, suppose \(e \in \partial V\). Then \(e \in E\) and \(|e_{\mathrm{set}} \cap V| = 1\). Since \(e\) is an edge of a simple graph, \(e\) is not a diagonal, so \(|e_{\mathrm{set}}| = 2\). But \(e_{\mathrm{set}} \cap V = e_{\mathrm{set}}\) since all vertices lie in \(V\), giving \(|e_{\mathrm{set}}| = 1\), a contradiction with \(|e_{\mathrm{set}}| = 2\) (by integer arithmetic). For the reverse direction, no element belongs to \(\emptyset \), so the implication holds vacuously.

By extensionality, we show both inclusions using the membership characterization.

For the forward direction, suppose \(e \in E\) and \(|e_{\mathrm{set}} \cap S| = 1\). Since \(e\) is a non-diagonal edge, \(|e_{\mathrm{set}}| = 2\). Using the partition identity \(|e_{\mathrm{set}} \cap S| + |e_{\mathrm{set}} \cap S^c| = |e_{\mathrm{set}}|\), we substitute \(|e_{\mathrm{set}}| = 2\) and \(|e_{\mathrm{set}} \cap S| = 1\) to obtain \(|e_{\mathrm{set}} \cap S^c| = 1\) by integer arithmetic.

For the reverse direction, suppose \(e \in E\) and \(|e_{\mathrm{set}} \cap S^c| = 1\). Again \(|e_{\mathrm{set}}| = 2\). Applying the partition identity for both \(S\) and \(S^c\), and noting that \((S^c)^c = S\), we substitute \(|e_{\mathrm{set}}| = 2\) and \(|e_{\mathrm{set}} \cap S^c| = 1\) into the partition for \(S^c\) to obtain \(|e_{\mathrm{set}} \cap S| = 1\) by integer arithmetic.

Unfolding the definition, we need to find an element in the filtered set. Since \(|V| \ge 2\), we have \(|V| {\gt} 0\), so by the characterization of positive cardinality there exists some vertex \(v \in V\). The singleton \(\{ v\} \) is a member of the universal finset, it is nonempty, and \(2 \cdot 1 = 2 \le |V|\). Thus \(\{ v\} \in \mathcal{S}(V)\).

Unfolding the definition of \(h(G)\), we split into two cases. If \(\mathcal{S}(V)\) is nonempty, then \(h(G)\) is the infimum of ratios \(|\partial S|/|S|\). We show \(0\) is a lower bound by verifying that for each valid subset \(S\), the ratio \(|\partial S|/|S|\) is non-negative, since both the numerator \(|\partial S|\) and denominator \(|S|\) are non-negative (being natural number casts). If \(\mathcal{S}(V)\) is empty, then \(h(G) = 0 \ge 0\) by reflexivity.

First, we establish that \(S\) is a Cheeger-valid subset by verifying \(S \in \mathcal{S}(V)\) using the nonemptiness and size conditions. This gives us that \(\mathcal{S}(V)\) is nonempty.

We then show that \(h(G)\) equals the infimum formula by unfolding the definition of cheegerConstant and simplifying with the nonemptiness witness.

Since \(S\) is nonempty, we have \(|S| {\gt} 0\) as a positive real number. By the definition of infimum, \(h(G) \le |\partial S|/|S|\) since \(S\) is one of the sets over which the infimum is taken.

We conclude by the calculation:

where the first inequality uses \(c \le h(G)\) and \(|S| \ge 0\), the second uses the infimum bound and \(|S| \ge 0\), and the final equality follows by cancellation since \(|S| \neq 0\).

We prove both directions of the equivalence.

Forward direction. Suppose \(G\) is a \(c\)-expander, i.e., \(0 {\lt} c\) and \(c \le h(G)\). We retain \(0 {\lt} c\) and for any nonempty \(S\) with \(2|S| \le |V|\), the bound \(c \cdot |S| \le |\partial S|\) follows from the edge boundary lower bound theorem applied to \(G\), \(c\), \(c \le h(G)\), \(S\), the nonemptiness of \(S\), and the size condition.

Reverse direction. Suppose \(0 {\lt} c\) and for all valid \(S\) we have \(c \cdot |S| \le |\partial S|\). We retain \(0 {\lt} c\) and must show \(c \le h(G)\). Since \(|V| \ge 2\), the set of Cheeger-valid subsets is nonempty. Unfolding the definition of \(h(G)\) and simplifying with this nonemptiness, we need to show \(c\) is at most the infimum. We apply the le-inf’ characterization: for each \(S \in \mathcal{S}(V)\), we extract from the membership that \(S\) is nonempty with \(2|S| \le |V|\). Since \(S\) is nonempty, \(|S| {\gt} 0\) as a real number, so we rewrite the goal using the division characterization \(c \le |\partial S|/|S| \iff c \cdot |S| \le |\partial S|\), which holds by hypothesis.