continuous_coordW
plain-language theorem explainer
The real coordinate on the doubly punctured unit circle is continuous. Anyone proving that the east/west arcs are clopen (or otherwise using level sets of that coordinate) cites this. The proof is a short term composition of the ambient Euclidean projection with two subtype inclusions.
Claim. Let $W_c$ be the doubly punctured unit circle in the plane. The coordinate map $W_c \to \mathbb{R}$ sending each point to its ambient $x_0$-coordinate is continuous.
background
In SingularSphereGeometry one works with the unit sphere $S^1 \subset \mathbb{R}^2$ and removes the north and south poles, obtaining a doubly punctured circle $W_c$. Points of $W_c$ are nested subtypes of the ambient Euclidean space, so the natural real coordinate is the composition of the two subtype forgetful maps with the standard projection onto the $0$-th Euclidean factor.
That coordinate is written coordW in the module: on $w \in W_c$ it returns the ambient $0$-component of the underlying sphere point. Continuity of this map is the elementary analytic fact needed before one can treat sublevel sets such as ${x_0 \ge 0}$ as closed (or open) in the subspace topology on $W_c$.
The surrounding development builds open covers of the sphere minus poles and studies arcs cut out by sign conditions on this coordinate; those arcs later appear as clopen pieces in connectedness arguments.
proof idea
Term-mode proof by composition of continuous maps. The ambient Euclidean projection $\mathrm{proj}_0 : \mathbb{R}^2 \to \mathbb{R}$ is continuous; each of the two nested subtype valuations $W_c \hookrightarrow S^1 \hookrightarrow \mathbb{R}^2$ is continuous. The lemma is exactly
Continuous.comp (EuclideanSpace.proj 0).continuous (continuous_subtype_val.comp continuous_subtype_val),
i.e. no case split and no topology-specific lemmas beyond the standard continuity of projections and subtype inclusions.
why it matters
Immediate consumer is isClopen_arcA, which identifies the right (east) arc of the doubly punctured circle with the preimage coordW ⁻¹' (Ici 0) and uses continuity (together with the fact that the coordinate never vanishes on $W_c$) to conclude the arc is both open and closed.
That clopen decomposition is local scaffolding for the singular-sphere geometry layer of the foundation: it separates the circle into rigid east/west pieces once the poles are removed, supporting later cover and connectedness arguments in the same module. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure Euclidean topology feeding those geometric lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.