unionComplHomeo
plain-language theorem explainer
Explicit homeomorphism identifying the complement of a union KP ∪ KM with the Mayer–Vietoris intersection of the two half-complements inside (KP ∩ KM)^c. Anyone running the two-arc bisection for 1-cycles on arc complements cites it. The maps are pure subtype reindexing; both inverses are definitional and continuity follows from subtype projections.
Claim. For a topological space $W$ and subsets $K_P, K_M \subseteq W$, there is a homeomorphism $$W \setminus (K_P \cup K_M) \;\simeq_t\; \bigl\{ x \in (K_P \cap K_M)^c : x \notin K_P \bigr\} \cap \bigl\{ x \in (K_P \cap K_M)^c : x \notin K_M \bigr\}.$$
background
The module develops acyclicity of arc complements in a space $W$, feeding a Mayer–Vietoris style argument that splits a closed set into two halves. The relevant open sets are complements of closed arcs or unions of arcs; homology is taken in the singular chain complex of the corresponding TopCat objects.
Set-theoretically, a point lies outside $K_P \cup K_M$ if and only if it lies outside both $K_P$ and $K_M$, and automatically outside their intersection. The right-hand side packages that same condition as an intersection of two subsets of the ambient complement $(K_P \cap K_M)^c$. This identification is the standard open-set glueing data for a two-set Mayer–Vietoris sequence on complements.
Downstream, the bisection theorem needs a concrete homeomorphism (not merely a bijection) so that chain maps and boundary operators transport 1-cycles between the union complement and the two half-complements.
proof idea
Both directions are written as subtype constructors. Forward: from $y \notin K_P \cup K_M$, build the nested subtype whose outer witness is $y \notin K_P \cap K_M$ (via left-union membership) and whose two intersection witnesses are $y \notin K_P$ and $y \notin K_M$. Inverse: from a point of the intersection, unpack the underlying point of $W$ and reassemble the union-nonmembership by case-splitting the union.
Left and right inverses are rfl. Continuity of each map is Continuous.subtype_mk applied to continuous_subtype_val (composed once on the inverse side). No external lemmas beyond the standard continuous-subtype API.
why it matters
This is the geometric identification underlying the bisection step bounds_of_halves: a 1-cycle of the complement of $K_U = K_P \cup K_M$ whose pushforwards bound in both half-complements already bounds in the union complement, once $H_2((K_P \cap K_M)^c) = 0$. Without a homeomorphism (rather than a mere set bijection), the singular chain functors would not transport cycles and boundaries.
In the Recognition foundation stack, arc-complement acyclicity is the topological input that lets linking and higher homology vanish in high dimensions, clearing the way for the forcing chain’s dimensional and octave constraints (T7 eight-tick period, T8 $D = 3$). The definition itself is pure topology; its value is that it makes the elementwise two-arc Mayer–Vietoris argument fully constructive in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.