flattenComplHomeo
plain-language theorem explainer
Inside a space W, if E ⊆ K then the points of W\E that still avoid K are homeomorphic to W\K itself: nested subtype data flattens. Algebraic topologists working the two-arc Mayer–Vietoris reduction for H₁ of complements cite this homeomorphism to move cycles between the nested and flat presentations. The construction is the explicit continuous inverse pair on subtypes, with both directions continuous by composition of subtype projections.
Claim. Let $W$ be a topological space and let $E \subseteq K \subseteq W$. Then the subspace $\{ x \in W \setminus E : x \notin K \}$ is homeomorphic to $W \setminus K$. Explicitly, the nested subtype of the complement of $E$ consisting of points outside $K$ is homeomorphic to the ordinary subtype of points of $W$ outside $K$.
background
The ambient setting is TopCat (topological spaces as a category), with complements written as subtypes: $W \setminus K$ appears as ${ y : W \mid y \notin K }$, and $W \setminus E$ as the object TopCat.of (Eᶜ). Inside that complement one can cut further by the predicate $x \notin K$, producing a subtype of a subtype.
When $E \subseteq K$, set-theoretically $(W \setminus E) \setminus K = W \setminus K$. The only work is to package that equality as a homeomorphism of the Lean subtype presentations, so that singular homology (or chain groups) of the two presentations can be identified without re-proving continuity of inclusions by hand each time.
The module develops linking-vanishing and arc-complement acyclicity in high dimension: $H_1$ of complements of closed sets, reduced via a two-arc Mayer–Vietoris pattern that repeatedly compares complements of halves $KP$, $KM$ with the complement of their union.
proof idea
Define the forward map by forgetting one subtype layer: send $\langle\langle x, _\rangle, h\rangle$ to $\langle x, h\rangle$. The inverse rebuilds the missing membership proof for $Eᶜ$ from $E \subseteq K$ and $y \notin K$: if $y \in E$ then $y \in K$, contradiction. Both composites are definitionally (or by Subtype.ext) the identity.
Continuity of each direction is Continuous.subtype_mk applied to the composite of the two subtype-value projections (forward) or a double subtype_mk of continuous_subtype_val (inverse). No external lemmas beyond mathlib subtype continuity are required; the hypothesis $E \subseteq K$ is used only in the inverse's well-definedness.
why it matters
The homeomorphism is the bookkeeping step that lets the abstract two-arc Mayer–Vietoris theorem isZero_h1_unionCompl treat $H_1(W \setminus (KP \cup KM))$ in the flat subtype form while intermediate bounds live on nested complements. Downstream, bounds_of_halves (the bisection step) uses the same flattening so that a 1-cycle in the union complement whose pushforwards bound in each half-complement already bounds, once $H_2((KP \cap KM)ᶜ) = 0$.
In the Recognition foundation stack this supports linking-vanishing for high-dimensional complements of arcs and closed sets: $H_1$-acyclicity of arc complements feeds the forcing geometry around the eight-tick and $D = 3$ landmarks by ensuring that linking classes detected in low dimension die in the high-dimensional ambient. Without a clean homeomorphism between nested and flat complements, every Mayer–Vietoris diagram would carry an extra continuous-equivalence obligation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.