continuous_twoSimplexCoordOneParam
plain-language theorem explainer
The second barycentric coordinate on the standard 2-simplex is continuous as a map into the unit interval. Anyone assembling continuous singular 2-simplices or prism maps on S¹ cites this fact. The argument reduces pointwise continuity to continuous evaluation of the Fin-index-1 coordinate on the ambient product, then restricts to the simplex subtype.
Claim. The map sending $x \in \Delta^2 = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,3)$ to its second barycentric coordinate $x_1 \in I = [0,1]$ is continuous.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular 2-simplex $F$, the alternating face sum of displacements vanishes. That identity is the chain-level half of the split injection $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$.
The standard 2-simplex $\Delta^2$ is the set of $(x_0,x_1,x_2)\in\mathbb{R}^3_{\ge 0}$ with sum 1. The helper under study reads the middle barycentric weight $x_1$ and packages it as a point of the unit interval $I$, using the membership lemma that every coordinate of a standard-simplex point lies in $[0,1]$.
Downstream prism constructions need this coordinate map to be continuous so that post-composition with a continuous path $\gamma:I\to S^1$ yields a continuous singular 2-simplex.
proof idea
Pointwise argument. Rewrite global continuity as continuity at every point. At a fixed $x$, unfold continuous-at via the subtype range criterion tendsto_subtype_rng. The resulting limit is exactly continuous evaluation at Fin-index 1 on the ambient product, composed with the continuous subtype valuation of $\Delta^2$; both pieces are library-continuous, so their composite is continuous at $x$.
why it matters
Feeds pathBacktrackMap, the triangular backtrack prism over a path $\gamma$: it sends $x\in\Delta^2$ to $\gamma(x_1)$, so its three faces are the reversed path, the constant initial edge, and the original path. Continuity of the coordinate map is exactly the continuity obligation in that definition.
That prism is part of the 2-simplex telescoping that proves displacement kills boundaries (module doc: the boundary walk $v_0\to v_1\to v_2$ is homotopic rel endpoints inside the convex simplex to the direct edge, and pushing the homotopy through $F$ with path-displacement additivity and homotopy invariance yields the alternating-sum identity). Together with the generator evaluation on the fundamental loop, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation/surjectivity half still needs a simplicial prism or subdivision operator absent from Mathlib singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.