29 Def 19: Edge Boundary and Vertex Incidence for Cell Complexes
Let \(X\) be a cell complex and let \(S \subseteq X_0\) be a subset of vertices (0-cells). The edge boundary of \(S\) is the set
That is, an edge \(e \in X_1\) belongs to \(\delta S\) if and only if its boundary \(\partial _1 e\) intersects both \(S\) and its complement \(S^c\).
Let \(X\) be a cell complex, \(S \subseteq X_0\), and \(e \in X_1\). Then
This follows immediately by unfolding the definition of \(\delta S\) and applying simp.
Let \(X\) be a cell complex and \(S \subseteq X_0\). If there exists an edge \(e \in X_1\) such that \(\partial _1 e\) contains a vertex in \(S\) and a vertex not in \(S\), then \(\delta S\) is nonempty.
Assume there exists \(e \in X_1\) with \((\exists \, u \in \partial _1 e,\; u \in S)\) and \((\exists \, w \in \partial _1 e,\; w \notin S)\). From the hypothesis \(h\), we obtain such an edge \(e\) together with the witness \(h_e\) of both conditions. By the membership characterization \(\texttt{mem\_ edgeBoundaryCell}\), we have \(e \in \delta S\), so \(\delta S\) is nonempty.
Let \(X\) be a cell complex and let \(E \subseteq X_1\) be a set of edges (1-cells). The set of vertices incident to \(E\) is
Let \(X\) be a cell complex, \(E \subseteq X_1\), and \(v \in X_0\). Then
This follows immediately by unfolding the definition of \(\Gamma (E)\) and applying simp.
Let \(X\) be a cell complex and \(E \subseteq X_1\). If there exists an edge \(e \in E\) with a vertex \(v \in X_0\) such that \(v \in \partial _1 e\), then \(\Gamma (E)\) is nonempty.
From the hypothesis \(h\), we obtain \(e \in E\) and \(v \in X_0\) with \(v \in \partial _1 e\). By the membership characterization \(\texttt{mem\_ incidentVerticesCell}\), we conclude \(v \in \Gamma (E)\), so \(\Gamma (E)\) is nonempty.
Let \(X\) be a cell complex and \(v \in X_0\) a vertex. The set of edges incident to \(v\) (the star of \(v\)) is
Let \(X\) be a cell complex, \(v \in X_0\), and \(e \in X_1\). Then
This follows immediately by unfolding the definition of \(\delta v\) and applying simp.
Let \(X\) be a cell complex and \(v \in X_0\). If there exists \(e \in X_1\) such that \(v \in \partial _1 e\), then \(\delta v\) is nonempty.
From the hypothesis \(h\), we obtain \(e \in X_1\) with \(v \in \partial _1 e\). By the membership characterization \(\texttt{mem\_ incidentEdges}\), we conclude \(e \in \delta v\), so \(\delta v\) is nonempty.
Let \(X\) be a cell complex, \(S \subseteq X_0\), and \(v \in X_0\). The edge boundary of \(S\) at vertex \(v\) is the intersection
Let \(X\) be a cell complex, \(S \subseteq X_0\), \(v \in X_0\), and \(e \in X_1\). Then
This follows immediately by unfolding the definition of \((\delta S)_v\) and applying simp.
Let \(X\) be a cell complex, \(S \subseteq X_0\), and \(v \in X_0\). Then
Since \((\delta S)_v\) is defined as the filter of \(\delta S\) by the predicate \(v \in \partial _1 e\), the inclusion \((\delta S)_v \subseteq \delta S\) holds by the general fact that a filtered finset is a subset of the original finset (Finset.filter_subset).
Let \(X\) be a cell complex, \(S \subseteq X_0\), and \(v \in X_0\). Then
Let \(e\) be arbitrary and assume \(e \in (\delta S)_v\). Rewriting using the membership characterization \(\texttt{mem\_ edgeBoundaryVertex}\), we obtain \(e \in \delta S\) and \(v \in \partial _1 e\). Rewriting the goal using \(\texttt{mem\_ incidentEdges}\), it suffices to show \(v \in \partial _1 e\), which is precisely the second component of the hypothesis.
Let \(X\) be a cell complex, \(S \subseteq X_0\), and \(v \in X_0\). If there exists \(e \in X_1\) such that \(e \in \delta S\) and \(v \in \partial _1 e\), then \((\delta S)_v\) is nonempty.
From the hypothesis \(h\), we obtain \(e \in X_1\) with the witness \(h_e\) satisfying \(e \in \delta S\) and \(v \in \partial _1 e\). By the membership characterization \(\texttt{mem\_ edgeBoundaryVertex}\), we conclude \(e \in (\delta S)_v\), so \((\delta S)_v\) is nonempty.
Let \(X\) be a cell complex, \(S \subseteq X_0\), \(v \in X_0\), and \(e \in X_1\). Then
Rewriting with \(\texttt{mem\_ edgeBoundaryVertex}\), the left-hand side becomes \((e \in \delta S) \land (v \in \partial _1 e)\). Rewriting with \(\texttt{mem\_ edgeBoundaryCell}\), the condition \(e \in \delta S\) expands to \((\exists \, u \in \partial _1 e,\; u \in S) \land (\exists \, w \in \partial _1 e,\; w \notin S)\). The equivalence with the right-hand side then follows by propositional logic (tauto).