stdSimplex_eq_vertex_two_of_coord_two_eq_one
plain-language theorem explainer
In the standard 2-simplex Δ², any point whose third barycentric coordinate equals 1 must be exactly the apex vertex v₂. Continuity arguments for the cone map Δ² → S¹ cite this to collapse the apex case to a single point. The proof is a three-case coordinate chase: the simplex sum and nonnegativity force the other two coordinates to zero.
Claim. Let $x$ be a point of the standard $2$-simplex $\Delta^2 = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,3)$. If the barycentric coordinate $x_2 = 1$, then $x$ equals the vertex $v_2$ (the Dirac mass at index $2$).
background
The ambient module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries: for every singular $2$-simplex $F:\Delta^2\to S^1$, 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$ consists of triples $(x_0,x_1,x_2)$ of nonnegative reals summing to $1$. Its three vertices are the standard basis vectors $v_0,v_1,v_2$. Mathlib records stdSimplex.sum_eq_one and the coordinate bounds via membership in $[0,1]$.
Downstream, a pointwise cone construction $\mathrm{coneCirclePoint},\gamma:\Delta^2\to S^1$ is built from a loop $\gamma$. Continuity of that cone needs a clean description of the apex locus ${x_2=1}$, which is exactly this lemma.
proof idea
Pointwise equality of simplex points is checked coordinatewise (ext i), then by cases on $i\in{0,1,2}$.
For $i=0$ and $i=1$: rewrite stdSimplex.sum_eq_one as $x_0+x_1+x_2=1$, insert the hypothesis $x_2=1$, and use nonnegativity of $x_0,x_1$ (from mem_Icc_of_mem_stdSimplex) with linarith to conclude each is zero.
For $i=2$: the goal is literally the hypothesis $x_2=1$, which matches the third coordinate of $v_2$.
why it matters
The sole downstream consumer is continuous_coneCirclePoint: continuity of the pointwise cone $\Delta^2\to S^1$. That theorem splits on whether $x_2=1$; on the apex branch it rewrites via this identity so the cone value is the constant basepoint and the squeeze argument applies.
Closing apex continuity finishes the analytic packaging of the cone, which sits inside the singular-simplex winding apparatus of CircleWindingChain. That apparatus supplies the kills-boundaries identity for $1$-cycles on $S^1$ and the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The lemma itself is pure convex geometry; its framework role is as a small but necessary hinge in the continuity proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.