Only finitely many points admit no good window
ProvedMonotonicity_Theorem.no_good_window_locus_finiteLet be an o-minimal structure over a dense linear order without endpoints , and let be a definable function of one variable with infinite. Call a point of the line good if some open interval containing witnesses one of
- is constant on ;
- and is strictly increasing on ;
- and is strictly decreasing on .
Claim. The set of points that are not good is finite.
The set of non-good points is definable, so by o-minimality it is a finite union of points and intervals; it therefore suffices to know that it contains no open interval. That in turn is the content of Lemmas 1–3 of this mission: on a subinterval, a definable function is constant or injective, an injective definable function is strictly monotone on a further subinterval, and the monotone situation can be arranged inside the domain. Consequently every open interval contains a point admitting a good window, so the non-good set has empty interior and is finite. Geometrically it consists of the finitely many transition points between the three regimes together with the finitely many boundary and isolated points of the domain.
import Definitions.Def_Monotonicity_Theorem_Window_Loci
theorem Monotonicity_Theorem.no_good_window_locus_finite {R : Type} (D : DenseLinearOrderNoEndpoints R)
(M : OMinimalStructure D) {I B : Set (Power R 1)} (f : DefinableFunction M I B)
(hI : IsInfinite1 I) :
IsFinite1 (setCompl (GoodWindowLocus f)) := by sorry