mvInclV
plain-language theorem explainer
Continuous inclusion of the intersection U ∩ V into V, as a TopCat morphism. Anyone building the singular Mayer–Vietoris short complex or the homology pair map cites it as the right-hand space-level leg. It is a one-line specialization of the nested-subspace inclusion to Set.inter_subset_right.
Claim. For open sets $U,V \subseteq X$, the continuous inclusion morphism $i_V \colon U \cap V \hookrightarrow V$ in $\mathbf{Top}$.
background
Singular Mayer–Vietoris in this module is built from space-level inclusions of open sets and their intersection, then pushed to singular chain complexes and homology. The ambient data are open $U,V \subseteq X$ (typically covering $X$), with singular chains $C_\bullet$ and the small complex relative to the cover.
The helper subIncl turns a subset relation $W \subseteq W'$ into a TopCat morphism $\mathrm{Top}(W) \to \mathrm{Top}(W')$ via Set.inclusion and continuity of inclusion. The companion left leg is the inclusion $U \cap V \hookrightarrow U$. Together they induce the chain maps that enter the degreewise short complex and the biproduct pair map on homology.
Upstream, only the subset fact $U \cap V \subseteq V$ is needed; no homology vanishing or cover hypothesis appears at this layer.
proof idea
One-line definition: apply the nested-subspace inclusion constructor to the standard fact that an intersection is contained in its right factor. No further rewriting or continuity argument is local to this declaration; continuity is packaged inside the helper.
why it matters
This is the right space-level leg of singular Mayer–Vietoris. Downstream it feeds the degreewise short complex (lift of chain maps along both inclusions), the middle-exactness lemma (recovering a chain on the intersection from cancelling images in $U$ and $V$), the homology pair map $[c] \mapsto ([i_*c], -[j_*c])$, and the agreement of the two routes into the small complex.
Outside the module it is used in arc-complement acyclicity: elementwise MV injectivity at $H_1(U \cap V)$ and the bisection step for two-arc covers of a knot complement. In the Recognition foundation stack those acyclicity facts support topological control on complements, feeding later forcing and dimensional arguments rather than the J-cost or $\varphi$-ladder directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.