Locally ordering the distinct values of a finite family

A finite family of continuous functions into a linearly ordered space can be ordered near a parameter by selecting one fixed label for each distinct value at that parameter, provided labels coinciding there continue to coincide nearby. The selected labels enumerate all distinct values in strictly increasing order on one common neighborhood. Empty families are included.

This keeps the original functions, rather than sorting their values independently at each parameter, so any additional regularity of the functions survives the selection. In particular, it is useful for turning analytic root labellings with persistent collisions into distinct ordered root sections.

theorem TauCeti.exists_eventually_strictMono_range_eq {B : Type u_1} {Y : Type u_2} {ι : Type u_3} [TopologicalSpace B] [LinearOrder Y] [TopologicalSpace Y] [OrderClosedTopology Y] [Finite ι] {f : ι → B → Y} {x₀ : B} (hf : ∀ (i : ι), ContinuousAt (f i) x₀) (heq : ∀ (i j : ι), f i x₀ = f j x₀ → f i =ᶠ[nhds x₀] f j) : ∃ (k : ℕ) (e : Fin k ↪ ι), ∀ᶠ (x : B) in nhds x₀, (StrictMono fun (i : Fin k) => f (e i) x) ∧ (Set.range fun (i : Fin k) => f (e i) x) = Set.range fun (i : ι) => f i x

A finite continuous family with persistent central collisions admits a fixed selection of labels whose values enumerate its range in strictly increasing order near the central parameter. Only pairs equal at the central parameter need an equality hypothesis.