small_pushIdx_left

In the singular Mayer–Vietoris setup one works with a topological space $X$ and a pair of subsets $U,V$. A singular $n$-simplex of $X$ is called small (relative to $U,V$) when the image of the corresponding continuous map $\Delta^n\to X$ lies entirely in $U$ or entirely in $V$.

The push map sends a simplex of the subspace topology on $W\subseteq X$ to the underlying simplex of $X$ by composing with the inclusion $W\hookrightarrow X$. The companion fact range_pushIdx records that this pushforward still has image inside $W$.

Together these notions let one identify the free abelian group on small simplices with a direct summand of the ordinary singular chains, which is the algebraic input to the Mayer–Vietoris long exact sequence.

One-line wrapper. Apply the range-inclusion for the push map on $U$: the geometric image of $\mathrm{push}_U(a)$ is contained in $U$. That is exactly the left disjunct of the definition of smallness, so inject via Or.inl.

Feeds the definition of the index map from $U$-simplices into the type of small simplices: that map packages the pushforward together with this smallness witness. The symmetric right-hand statement for $V$ is the twin ingredient. Both are local plumbing for the singular Mayer–Vietoris complex in the Foundation layer; they do not themselves invoke the Recognition forcing chain (T0–T8), but they sit under the singular-homology scaffolding used later for topological invariants of recognition spaces.