affineMap_mem_hullOf
plain-language theorem explainer
Any point of the standard m-simplex, pushed forward by the affine map of a vertex tuple u in Δ^d, lands in the convex hull of those vertices in ambient R^{d+1}. Diameter and mesh arguments in singular subdivision cite this membership. The proof rewrites the image as a convex combination and invokes convexity of the hull.
Claim. Let $u$ be a tuple of $m+1$ points of the standard $d$-simplex $\Delta^d$, and let $x\in\Delta^m$. Writing $\mathrm{aff}_u(x)$ for the affine map determined by $u$ evaluated at $x$, the ambient coordinate vector of $\mathrm{aff}_u(x)$ lies in $\mathrm{conv}\{\,u_i\,\}_{i=0}^{m}$ inside $\mathbb{R}^{d+1}$.
background
The module builds singular subdivision of simplices: affine pieces of $\Delta^d$ cut by vertex tuples, with mesh control for homology arguments. The ambient convex hull of a vertex tuple $w$ is hullOf w, namely $\mathrm{conv}(\mathrm{range},w)$ inside $\mathbb{R}^{d+1}$.
The continuous affine map $\mathrm{aff}_u:\Delta^m\to\Delta^d$ sends the $i$-th vertex of $\Delta^m$ to $u_i$. On coordinates it is the barycentric combination $\mathrm{aff}_u(x)_j=\sum_i x_i,u_i(j)$ (affineMap_apply_coe). Each vertex coe $u_i$ already sits in hullOf u by the range inclusion into the convex hull (coe_mem_hullOf).
Standard-simplex coordinates are nonnegative and sum to one; those two facts turn the barycentric formula into a genuine convex combination of the $u_i$.
proof idea
First establish the coordinate identity that the ambient vector of $\mathrm{aff}_u(x)$ equals $\sum_i x_i\cdot(u_i)$: funext on the ambient index, Finset.sum_apply, and affineMap_apply_coe.
Rewrite the goal with that identity. Apply convex_convexHull.sum_mem: nonnegativity of the weights from stdSimplex.zero_le, the partition-of-unity identity stdSimplex.sum_eq_one, and vertex membership coe_mem_hullOf u i for each summand. That places the combination in hullOf u.
why it matters
Immediate parent is dist_affineMap_le: every point of an affine piece lies within the piece's vertex spread of its zeroth vertex. That lemma applies the present membership together with dist_le_of_mem_hullOf and coe_mem_hullOf u 0.
dist_affineMap_le is the diameter step toward Stage 7 (the small-simplices theorem) in this module: open covers of a space admit singular chains supported on simplices of controlled mesh. In the Recognition foundation stack, controlled singular subdivision underwrites the combinatorial geometry that later forces the eight-tick octave and $D=3$ spatial dimensions (T7–T8), so hull membership is a low-level geometric lemma on that path rather than a physics claim itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.