Route B, Step 1: avoidance of a finite family of null bad sets

This file isolates the final measure-theoretic selection argument used by the relative positive-ray perturbation theorem. It does not mention collars, simplices, or equivariance.

Once every individual geometric bad set has been proved null, the theorem exists_mem_ball_avoiding_finset_of_null produces a parameter in any positive-measure perturbation ball which avoids all of them simultaneously.

theorem NRR.FoxNeuwirthOrderComplex.RouteBFiniteAvoidance.measure_iUnion_finset_null {E : Type u_1} {ι : Type u_2} [MeasurableSpace E] (μ : MeasureTheory.Measure E) (bad : ι → Set E) (indices : Finset ι) (hnull : ∀ i ∈ indices, μ (bad i) = 0) : μ (⋃ (i : ↥indices), bad ↑i) = 0

A finite union of sets of μ-measure zero has μ-measure zero.

The union is written over the subtype determined by the finite index set. This form avoids any decidability or enumeration choices in later applications.

theorem NRR.FoxNeuwirthOrderComplex.RouteBFiniteAvoidance.exists_mem_avoiding_finset_of_null {E : Type u_1} {ι : Type u_2} [MeasurableSpace E] (μ : MeasureTheory.Measure E) (bad : ι → Set E) (indices : Finset ι) (goodRegion : Set E) (hgood : μ goodRegion ≠ 0) (hnull : ∀ i ∈ indices, μ (bad i) = 0) : ∃ x ∈ goodRegion, ∀ i ∈ indices, x ∉ bad i

Every set of positive measure contains a point outside a finite family of null bad sets.

This is the abstract selection lemma needed by Route B. In the collar application, goodRegion will be an open ball around the unperturbed movable assignment, and bad i will be the positive-ray incidence set attached to one mixed face and one choice of distinguished movable vertex.

theorem NRR.FoxNeuwirthOrderComplex.RouteBFiniteAvoidance.exists_mem_ball_avoiding_finset_of_null {E : Type u_1} {ι : Type u_2} [PseudoMetricSpace E] [MeasurableSpace E] (μ : MeasureTheory.Measure E) (bad : ι → Set E) (indices : Finset ι) (center : E) (radius : ℝ) (hball : μ (Metric.ball center radius) ≠ 0) (hnull : ∀ i ∈ indices, μ (bad i) = 0) : ∃ x ∈ Metric.ball center radius, ∀ i ∈ indices, x ∉ bad i

Ball form of exists_mem_avoiding_finset_of_null.

No geometric assumptions are hidden here: positivity of the ball measure is an explicit hypothesis. A later finite-dimensional specialization will discharge it using positivity of Lebesgue measure on nonempty metric balls.