Infinite unions contain an interval
ProvedMonotonicity_Theorem.infinite_contains_interval_core2geometry-topologyo-minimality
An infinite set that is a finite union of points and intervals contains a nondegenerate open interval: empty and point cases are finite, a union splits infiniteness to one side, and a degenerate interval is empty.
Preamble
import Definitions.Def_Monotonicity_Theorem_Framework2
Formal statement
theorem Monotonicity_Theorem.infinite_contains_interval_core2 {R : Type} [LinearOrder R] [DenselyOrdered R] [NoMaxOrder R] [NoMinOrder R]
(A : Set (Power R 1)) (hDef : FiniteUnionOfPointsAndIntervals A) (hInf : Set.Infinite A) :
exists (a : Endpoint R), exists (b : Endpoint R), Endpoint.lt a b /\ forall (x : Power R 1), openInterval a b x -> A x := by sorrySource
van den Dries, Tame Topology and O-Minimal Structures, Ch. 3