mem_iff_of_clopen_
plain-language theorem explainer
Both endpoints of any singular 1-simplex in a space X lie on the same side of any clopen subset A. Arguments that pair boundaries against clopen characteristic functions (partial augmentations, degree on spheres) cite this. The proof is a connectedness case-split: the continuous preimage of A in Δ¹ is clopen, hence empty or full, so the two vertices agree on membership.
Claim. Let $X$ be a topological space and let $A \subseteq X$ be clopen. For every singular $1$-simplex $\sigma$ in $X$, writing $e_0(\sigma)$ and $e_1(\sigma)$ for its two endpoints, one has $e_0(\sigma) \in A$ if and only if $e_1(\sigma) \in A$.
background
In the singular simplicial set of a space $X$, a $1$-simplex is (equivalently) a continuous map $f:\Delta^1\to X$. Its two face maps are the constant $0$-simplices at the endpoints of that path; recovering the underlying point of a $0$-simplex is the role of the point-extraction map used in the statement.
A subset is clopen when it is both open and closed. The standard $1$-simplex $\Delta^1$ is connected, so its only clopen subsets are $\emptyset$ and $\Delta^1$ itself. Therefore a continuous image of $\Delta^1$ cannot meet both a clopen set and its complement: the preimage would be a nontrivial clopen split of a connected space.
The ambient module develops singular-sphere and singular-homology infrastructure (prisms, pairs, Mayer–Vietoris, augmentations) on top of Mathlib's sphere, contractible, and path-homotopy material. The lemma is the geometric input to the partial-augmentation claim that immediately follows in the file.
proof idea
Rewrite both endpoint memberships via the face-point identity, so the claim concerns the two prism vertices of the continuous map $f$ attached to $\sigma$ by the simplex equivalence. The preimage $f^{-1}(A)$ is clopen because $A$ is clopen and $f$ is continuous. Split on whether that preimage is empty or the whole domain (the only clopen options in a connected space). If empty, each endpoint-membership hypothesis is absurd. If full, each endpoint lies in the preimage, so both directions of the biconditional hold by trivial membership.
why it matters
The next declaration in the module is the partial augmentation against a clopen set, which kills boundaries: once every $1$-simplex has endpoints on the same side of $A$, pairing the boundary operator with the characteristic function of $A$ yields zero. That algebraic vanishing is the standard input to degree, winding, and component-counting arguments on spheres.
Within Recognition Science foundation work, singular-sphere and Mayer–Vietoris tools support topological steps of the forcing chain (connectedness, dimension, and the eight-tick octave structure in T0–T8). Keeping the clopen-endpoint fact as a named lemma avoids ad-hoc path-chasing inside those later arguments. No recorded downstream edges appear on this page; the placement under the partial-augmentation doc-comment marks its intended consumer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.