Small
plain-language theorem explainer
A singular n-simplex is small relative to a pair of subsets U, V when its geometric image lies entirely in U or entirely in V. This is the standard support condition for the small-chain subcomplex in a Mayer–Vietoris argument. Anyone building the singular MV sequence on TopCat cites it. The body is a one-line disjunction on range inclusion via the simplex realization map.
Claim. Fix a topological space $X$ and subsets $U,V \subseteq X$. A singular $n$-simplex $s$ of $X$ is small (relative to $U,V$) when the image of its geometric realization is contained in $U$ or contained in $V$.
background
The module develops a singular Mayer–Vietoris package over TopCat, importing Mathlib homology complexes together with the local singular infrastructure (prisms, pairs, subdivision). The index type Idx X n labels singular $n$-simplices of $X$; each index is realized by a continuous map from the standard simplex, written here via simplexEquiv.
Classically, the Mayer–Vietoris long exact sequence is obtained by comparing the singular chain complex of $X$ with the subcomplex of chains whose simplices are supported in $U$ or in $V$ (for an open cover $X = U \cup V$). The predicate defined here is exactly that support condition: range of the realization lies in $U$ or in $V$.
A companion face lemma (immediately below the definition) records that faces of small simplices remain small, which is needed so the small generators close under the singular boundary.
proof idea
Pure definition: the proposition is the disjunction
range(simplexEquiv X n s) ⊆ U ∨ range(simplexEquiv X n s) ⊆ V.
No proof obligations. The adjacent face lemma Small.δ is a short case split: the face realization factors through the parent realization (simplexEquiv_δ plus range_comp_subset_range), so either inclusion transports by subset transitivity.
why it matters
This predicate is the generator filter for the small singular chain groups in the module (SIdx, sCgrp, sgen, and the inclusion/retraction maps sInc, sRet, sBnd). Downstream in-module results such as genUnit_mem_smallSpan depend on it to place fundamental classes inside the small span.
In the broader Recognition Science foundation layer, singular MV is part of the topological toolkit used when comparing local recognition data on overlapping charts. The definition itself is classical algebraic topology, not an RS forcing step (T0–T8); it supplies the support language those later geometric arguments need when they invoke subdivision and gluing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.