A small neighborhood of a finite straight-segment arrangement

A sufficiently small ball about any point avoids every segment of a finite arrangement that does not contain that point. The proof uses compactness of actual real segments and finite union, rather than a local-disk provider.

theorem Cslib.Polygonal.exists_ball_only_incident_segments {ι : Type u_1} [Finite ι] (a b : ι → ℂ) (z : ℂ) : ∃ ε > 0, ∀ (i : ι), ∀ w ∈ Metric.ball z ε, w ∈ segment ℝ (a i) (b i) → z ∈ segment ℝ (a i) (b i)

A finite family of genuine planar segments has a neighborhood of z meeting only segments that already contain z. Degenerate segments are allowed in this general lemma.