Continuous selections from a delineation #
A continuous root of a non-nullified member of a delineated polynomial family on a connected base chooses one fixed root section. Multiplicities and roots shared by different family members cause no difficulty: the delineation labels distinct roots, not roots with multiplicity. This is the root-selection step for semialgebraicity of continuous algebraic functions.
References #
- J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Springer, 1998, Section 8.1.
theorem
TauCeti.Delineation.exists_eq_root_of_continuous
{X : Type u_1}
{ι : Type u_2}
[TopologicalSpace X]
[ConnectedSpace X]
{P : ι → X → Polynomial ℝ}
(D : Delineation P)
{k : ι}
{f : X → ℝ}
(hf : Continuous f)
(hne : ∀ (x : X), P k x ≠ 0)
(hroot : ∀ (x : X), (P k x).IsRoot (f x))
:
A continuous root of a member that is nowhere nullified on a connected base is one fixed section of its delineation. Repeated roots are allowed.