Continuous choices from a finite family

A continuous function taking its values in a finite family of continuous functions which are pointwise distinct must choose the same member throughout a connected parameter space. This is useful for comparing different continuous labellings of simple roots: agreement at one parameter forces agreement everywhere.

Locally, distinctness can be replaced by persistence of collisions: if every family member agreeing with the chosen member at the central parameter continues to agree nearby, a continuous selection agrees with that member on a neighborhood.

theorem TauCeti.eventuallyEq_of_continuousAt_mem_range {B : Type u_1} {Y : Type u_2} {ι : Type u_3} [TopologicalSpace B] [TopologicalSpace Y] [T2Space Y] [Finite ι] {r : ι → B → Y} {f : B → Y} {b₀ : B} (hr : ∀ (j : ι), ContinuousAt (r j) b₀) (hf : ContinuousAt f b₀) (hmem : ∀ᶠ (b : B) in nhds b₀, f b ∈ Set.range fun (j : ι) => r j b) {i : ι} (h₀ : r i b₀ = f b₀) (hcollision : ∀ (j : ι), r j b₀ = r i b₀ → r j =ᶠ[nhds b₀] r i) : r i =ᶠ[nhds b₀] f

A continuous selection from a finite continuous family agrees locally with a chosen member if their values agree at the central parameter and collisions with that member persist nearby. Members with different central values are separated by continuity.

theorem TauCeti.eq_of_continuous_mem_range {B : Type u_1} {Y : Type u_2} {ι : Type u_3} [TopologicalSpace B] [PreconnectedSpace B] [TopologicalSpace Y] [T2Space Y] [Finite ι] {r : ι → B → Y} {f : B → Y} (hr : ∀ (i : ι), Continuous (r i)) (hf : Continuous f) (hinj : ∀ (b : B), Function.Injective fun (i : ι) => r i b) (hmem : ∀ (b : B), f b ∈ Set.range fun (i : ι) => r i b) (b₀ : B) {i : ι} (h₀ : r i b₀ = f b₀) : r i = f

A continuous choice from finitely many pointwise distinct continuous functions on a preconnected space agrees everywhere with the member it chooses at one point.