Infinite definable sets contain intervals
ProvedMonotonicity_Theorem.infinite_definable_set_contains_interval2geometry-topologyo-minimality
An infinite definable set of unary tuples contains a nondegenerate open interval: o-minimality turns definability into a finite-union structure, and infiniteness forces an interval piece.
Preamble
import Definitions.Def_Monotonicity_Theorem_Framework2
Formal statement
theorem Monotonicity_Theorem.infinite_definable_set_contains_interval2 {R : Type} [LinearOrder R] [DenselyOrdered R] [NoMaxOrder R] [NoMinOrder R] (M : OMinimalStructure R) (I : Set (Power R 1)) (hDef : M.S 1 I) (hInf : Set.Infinite I) : exists (a : Endpoint R), exists (b : Endpoint R), Endpoint.lt a b /\ (openInterval a b).Subset I := by sorrySource
van den Dries, Tame Topology and O-Minimal Structures, Ch. 3