A complement component absorbs a segment in an open ball

Let $U$ be an open region and let $C$ be a connected component of its complement, in the maximality sense encoded by ComplementComponent Uᶜ C. If $y\in C$, $z$ lies in the open metric ball $B(y,r)$, and the entire ball is contained in $U$, then the whole segment from $y$ to $z$ remains in $C$.

In other words, a complement component cannot be left by a straight segment that stays inside a ball disjoint from the complement of $U$. This local absorption principle is the step used to extend polygonal paths while remaining in the same complement component.

Formalization Note The hypothesis z ∈ Metric.ball y r forces the radius to be positive, so convexity of the metric ball places the segment in the ball; maximality of the component then absorbs the connected union of $C$ and that segment.