Singular simplices of subspaces

The singular simplices of a subspace are characterized by the image of their underlying maps. This identifies the range subcomplex of a subspace inclusion in a singular simplicial set.

theorem TopCat.mem_range_toSSet_subtypeVal_iff {X : TopCat} (S : Set ↑X) (n : SimplexCategoryᵒᵖ) (σ : (toSSet.obj X).obj n) : σ ∈ (SSet.Subcomplex.range (toSSet.map (ofHom (ContinuousMap.subtypeVal S)))).obj n ↔ Set.range ⇑((X.toSSetObjEquiv n) σ) ⊆ S

A singular simplex belongs to the range of a subspace inclusion exactly when its image is contained in the subspace.