continuous_prismSndFun
plain-language theorem explainer
The second (height) coordinate of the i-th prism map Δ^{n+1} → Δ^n × I is a continuous real function on the standard simplex. Anyone assembling the continuous prism map for singular homology cites this. The proof is a short term: a finite sum of continuous coordinate projections off the simplex subtype.
Claim. For every index $i \in \{0,\ldots,n\}$, the real-valued height function of the $i$-th prism map $\Delta^{n+1}\to\Delta^n\times I$ (the second factor landing in the unit interval) is continuous on the standard simplex.
background
The module builds the classical prism operator of singular homology inside Lean: affine maps $\Delta^{n+1}\to\Delta^n\times I$ that subdivide the product of a simplex with the unit interval. Vertices of the domain go to the bottom face vertices $v_j=(e_j,0)$ or the top face vertices $w_j=(e_j,1)$, with the switch occurring at index $i$.
The second factor of that map is a real function prismSndFun i on the standard simplex (a subtype of $\mathbb{R}^{n+2}$). Sibling lemmas already show it is nonnegative, at most one, and therefore lands in $I=[0,1]$. Continuity of that height function is the remaining analytic ingredient before the product map can be packaged as an element of $C(\Delta^{n+1},\Delta^n\times I)$.
Upstream, Mathlib supplies continuity of finite sums, of coordinate evaluations on product spaces, and of the subtype valuation map out of the simplex.
proof idea
One-line term proof. The height function is a finite sum (over a Finset of coordinates) of the corresponding coordinate projections of the simplex point. Each summand is continuous_apply k composed with continuous_subtype_val, hence continuous; continuous_finset_sum closes the argument.
why it matters
Feeds directly into the definition of prism, the continuous $i$-th prism map $\Delta^{n+1}\to\Delta^n\times I$. That definition packages the first factor as stdSimplex.map i.predAbove and the second as the subtype pair ⟨prismSndFun i x, …⟩; its continuous_toFun field multiplies the already-known continuous simplex map by this lemma.
In the broader Recognition stack the prism operator is scaffolding for singular-homology comparisons (chain homotopies, prism operators on singular chains) that sit under the Foundation layer. It is ordinary algebraic topology, not a forcing-chain step (T0–T8), but it is required infrastructure if later modules compare discrete eight-tick or recognition complexes to continuous singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.