Finite good partition

Proved

Monotonicity_Theorem.finite_partition_core2

by Tamas Fulop · Sep 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

geometry-topologyo-minimality

The partition assembly behind the monotonicity theorem: from the constant, increasing, and decreasing window classes with finite bad locus, cut points giving the same piecewise conclusion, under an explicit domain-inclusion hypothesis.

Preamble

import Definitions.Def_Monotonicity_Theorem_Framework2

Formal statement

theorem Monotonicity_Theorem.finite_partition_core2 {R : Type} [LinearOrder R] [DenselyOrdered R] [NoMaxOrder R] [NoMinOrder R]
    (M : OMinimalStructure R) {I B : Set (Power R 1)}
    (f : DefinableFunction M I B)
    {a b : Power R 1} (hab : Lt1 a b)
    (hsubIJ : (openInterval (Endpoint.finite (Power.coord1 a)) (Endpoint.finite (Power.coord1 b))).Subset I) :
    ∃ k : Nat, ∃ p : Fin (k + 1) → Power R 1,
      p 0 = a ∧ p (Fin.last k) = b ∧
      (∀ i : Fin k, Lt1 (p i.castSucc) (p i.succ)) ∧
      (∀ i : Fin k,
        let J : Set (Power R 1) := openInterval (Endpoint.finite ((p i.castSucc) 0)) (Endpoint.finite ((p i.succ) 0))
        (((∀ x (hxI : I x), J x → ∀ y (hyI : I y), J y ->
          f.toFun (Subtype.mk x hxI) = f.toFun (Subtype.mk y hyI)) ∧
          J.Subset (ContinuousPoints I (FunctionGraph (R := R) (m := 1) (n := 1) (A := I) (B := B) f.toFun))) ∨
         (((∀ x (hxI : I x), J x → ∀ y (hyI : I y), J y → Lt1 x y ->
            Lt1 (f.toFun (Subtype.mk x hxI)).1 (f.toFun (Subtype.mk y hyI)).1) ∨
           (∀ x (hxI : I x), J x → ∀ y (hyI : I y), J y → Lt1 x y ->
            Lt1 (f.toFun (Subtype.mk y hyI)).1 (f.toFun (Subtype.mk x hxI)).1)) ∧
          J.Subset (ContinuousPoints I (FunctionGraph (R := R) (m := 1) (n := 1) (A := I) (B := B) f.toFun))))) := by sorry

Source

van den Dries, Tame Topology and O-Minimal Structures, Ch. 3

Read-back

What the Lean code literally says, in plain math · muse-spark

Fix a type $R$ equipped with a linear order that is dense and has no maximum and no minimum, let $M$ be an o-minimal structure on $R$ , let $I$ and $B$ be sets of unary tuples over $R$ , let $f$ be a function from $I$ to $B$ definable in $M$ , let $a$ and $b$ be unary tuples, assume $a$ is strictly less than $b$ in the unary-tuple order, and assume the open interval of unary tuples with finite endpoints at the sole coordinates of $a$ and $b$ is contained in $I$ ; then there exist a natural number $k$ and a sequence $p_{0},\dots,p_{k}$ of unary tuples over $R$ such that $p_{0}=a$ and $p_{k}=b$ and $p_{i}$ is strictly less than $p_{i+1}$ for every $i<k$ , and such that for every $i<k$ , letting $J_{i}$ be the open interval of unary tuples with finite endpoints at the sole coordinates of $p_{i}$ and $p_{i+1}$ , one of the following holds: either $f$ is constant on $I\cap J_{i}$ in the sense that for all $x$ in $I$ lying in $J_{i}$ and all $y$ in $I$ lying in $J_{i}$ the values of $f$ at $x$ and $y$ are equal, and $J_{i}$ is contained in the set of points at which the graph of $f$ with source $I$ and target $B$ in dimensions $1$ and $1$ is continuous relative to $I$ ; or both $J_{i}$ is contained in that same set of continuity points and $f$ is strictly monotone on $I\cap J_{i}$ in one of two directions, namely either strictly increasing in the sense that for all $x,y$ in $I$ lying in $J_{i}$ with $x$ strictly less than $y$ the underlying unary tuple of $f(x)$ is strictly less than that of $f(y)$ , or strictly decreasing in the sense that for all such $x,y$ with $x$ strictly less than $y$ the underlying unary tuple of $f(y)$ is strictly less than that of $f(x)$ . In particular if $k=0$ there are no $i$ and the conditions on subintervals hold vacuously but $p_{0}=a$ and $p_{k}=b$ then force $a=b$ , which is incompatible with $a$ strictly less than $b$ , and for any $i$ if $I\cap J_{i}$ is empty or has no comparable distinct points then the constancy and strict monotonicity universal conditions on that $J_{i}$ hold vacuously.

Human review

Endorsed by Shuze Chen · Sep 15, 2026
Endorsed by Tamas Fulop · Sep 15, 2026
Confirmed by the mission captain (proposal self-audit).

View graph