Monotonicity theorem

Proved

Monotonicity_Theorem.monotonicity_theorem2

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

geometry-topologyo-minimality

Let an o-minimal structure M be given on a dense linear order without endpoints. For a definable function f on an infinite definable interval I, and ordered endpoints a and b, there are finitely many cut points from a to b. On each intervening open interval, f is constant, or strictly increasing and continuous, or strictly decreasing and continuous, with continuity expressed by ContinuousPoints.

Preamble

import Definitions.Def_Monotonicity_Theorem_Framework2

Formal statement

theorem Monotonicity_Theorem.monotonicity_theorem2
    {R : Type} [LinearOrder R] [DenselyOrdered R] [NoMaxOrder R] [NoMinOrder R]
    (M : OMinimalStructure R)
    {a b : Power R 1} (hab : Lt1 a b)
    (f : DefinableFunction M
      (openInterval (Endpoint.finite (Power.coord1 a))
        (Endpoint.finite (Power.coord1 b)))
      (Set.univ : Set (Power R 1))) :
    exists (k : Nat), exists (p : Fin (k + 1) -> Power R 1),
      p 0 = a /\
      p (Fin.last k) = b /\
      (forall (i : Fin k), Lt1 (p i.castSucc) (p i.succ)) /\
      (forall (i : Fin k),
        let J : Set (Power R 1) :=
          openInterval
            (Endpoint.finite ((p i.castSucc) 0))
            (Endpoint.finite ((p i.succ) 0))
        (forall (x : {x : Power R 1 //
            (openInterval (Endpoint.finite (Power.coord1 a))
              (Endpoint.finite (Power.coord1 b))) x}),
          forall (y : {y : Power R 1 //
            (openInterval (Endpoint.finite (Power.coord1 a))
              (Endpoint.finite (Power.coord1 b))) y}),
          J x.1 -> J y.1 ->
          f.toFun x = f.toFun y)
        \/
        ((forall (x : {x : Power R 1 //
            (openInterval (Endpoint.finite (Power.coord1 a))
              (Endpoint.finite (Power.coord1 b))) x}),
            forall (y : {y : Power R 1 //
            (openInterval (Endpoint.finite (Power.coord1 a))
              (Endpoint.finite (Power.coord1 b))) y}),
            J x.1 -> J y.1 -> Lt1 x.1 y.1 ->
            Lt1 (f.toFun x).1 (f.toFun y).1)
          \/
          (forall (x : {x : Power R 1 //
            (openInterval (Endpoint.finite (Power.coord1 a))
              (Endpoint.finite (Power.coord1 b))) x}),
            forall (y : {y : Power R 1 //
            (openInterval (Endpoint.finite (Power.coord1 a))
              (Endpoint.finite (Power.coord1 b))) y}),
            J x.1 -> J y.1 -> Lt1 x.1 y.1 ->
            Lt1 (f.toFun y).1 (f.toFun x).1))
        /\ J.Subset
            (ContinuousPoints
              (openInterval (Endpoint.finite (Power.coord1 a))
                (Endpoint.finite (Power.coord1 b)))
              (FunctionGraph (R := R) (m := 1) (n := 1)
                (A := openInterval (Endpoint.finite (Power.coord1 a))
                  (Endpoint.finite (Power.coord1 b)))
                (B := Set.univ)
                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 densely ordered and has neither a maximum nor a minimum, let $M$ be an o-minimal structure over $R$ , let $a$ and $b$ be unary tuples over $R$ with the hypothesis that $a$ is strictly less than $b$ in the strict order on unary tuples, and let $f$ be an $M$ -definable function whose domain is the open interval with finite endpoints at the single coordinates of $a$ and $b$ and whose codomain is the universal set of unary tuples over $R$ ; then the claim is that 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 each consecutive pair is strictly increasing, i.e. for every $i<k$ the $i$ -th term is strictly less than the $(i+1)$ -st term, and for every $i<k$ , writing $J_i$ for the open interval with finite endpoints at the $0$ -th entries of the $i$ -th and $(i+1)$ -st terms, one of the following holds: either $f$ is constant on $J_i$ in the sense that for all $x,y$ belonging to the large interval from $a$ to $b$ , if their underlying tuples lie in $J_i$ then the values of $f$ at $x$ and $y$ are equal, or both of the following hold jointly, namely $J_i$ is contained as a set in the set obtained by applying the $\mathrm{ContinuousPoints}$ construction to the large interval and to the set obtained by applying the $\mathrm{FunctionGraph}$ construction with dimensions $1,1$ , domain set the large interval, codomain set the universal set, and function the underlying function of $f$ , and at least one of two order-behaviors holds on $J_i$ , namely either $f$ is strictly increasing on $J_i$ in the sense that for all $x,y$ in the large interval whose underlying tuples lie in $J_i$ , if $x$ is strictly less than $y$ then the value of $f$ at $x$ is strictly less than the value at $y$ , or $f$ is strictly decreasing on $J_i$ in the sense that for all such $x,y$ , if $x$ is strictly less than $y$ then the value at $y$ is strictly less than the value at $x$ ; in the degenerate case $k=0$ there is no $i<k$ so the requirements on consecutive pairs and on each $J_i$ are vacuously true while $p_0=a$ and $p_0=b$ together force $a=b$ , which is incompatible with the strict inequality hypothesis if that order is irreflexive, and for any $i$ with $J_i$ empty the implications assuming membership in $J_i$ are vacuously true.

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