continuous_affineMapFun
plain-language theorem explainer
The barycentric affine map sending the standard n-simplex into the ambient coordinates of the standard m-simplex, determined by any choice of m-simplex vertices, is continuous. Anyone building continuous singular simplices or subdivision operators cites this. The proof is a short pi/sum continuity chase: each coordinate is a finite sum of products of continuous coordinate projections with constants.
Claim. For any vertex tuple $v:\mathrm{Fin}(n+1)\to\Delta^m$, the map $x\mapsto\bigl(j\mapsto\sum_i x_i\,v(i)_j\bigr)$ from $\Delta^n$ into $\mathbb{R}^{m+1}$ is continuous (product topology / subspace topology on the standard simplex).
background
The ambient setting is the standard geometric simplex $\Delta^k\subset\mathbb{R}^{k+1}$ of points with nonnegative barycentric coordinates summing to 1. In this module one builds affine maps $\Delta^n\to\Delta^m$ by specifying images of the $n+1$ vertices: a tuple $v:\mathrm{Fin}(n+1)\to\Delta^m$.
The underlying set-function is the barycentric combination $x\mapsto\sum_i x_i\cdot v(i)$, written coordinatewise as $\mathrm{affineMapFun},v$. Continuity of that raw function (before re-embedding into $\Delta^m$) is the lemma here. The module sits in the singular-homology foundation layer (Mathlib singular homology imports plus local prism/subdivision scaffolding), so these maps are the geometric generators of continuous singular simplices and of subdivision operators.
proof idea
Work in the product topology on $\mathrm{Fin}(m+1)\to\mathbb{R}$. Continuity of a map into a product reduces to continuity of each coordinate projection (continuous_pi). The $j$-th coordinate is a finite sum over $i$ of $x_i\cdot v(i)_j$, so apply continuous_finset_sum. Each summand is a product of a continuous scalar function of $x$ with a constant $v(i)_j$ (Continuous.mul with continuous_const). The scalar $x\mapsto x_i$ is the $i$-th coordinate on the simplex, obtained by composing the continuous subtype inclusion $\Delta^n\hookrightarrow\mathbb{R}^{n+1}$ with continuous_apply i.
why it matters
This lemma is the continuity half of the packaged continuous map affineMap : C(\Delta^n,\Delta^m), whose toFun is the subtype-packaged barycentric combination and whose continuous_toFun is exactly (continuous_affineMapFun v).subtype_mk _. Without it, vertex-determined affine maps cannot enter the continuous singular chain complex or the subdivision/prism constructions that the Foundation.SingularSubdivision module is assembling.
In the broader Recognition Science stack this is pure geometric scaffolding for singular homology on simplices (the combinatorial side of the eight-tick / discrete-recognition story), not a physics forcing step (T5–T8). It closes a routine analytic obligation so later subdivision identities can stay inside continuous maps rather than raw functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.