Finite good partition

Proved

Monotonicity_Theorem.finite_partition_core

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

geometry-topologyo-minimality

Finite good partition assembly: a definable function on an infinite domain with ordered endpoints admits finitely many cut points partitioning the interval into good pieces. Each piece is either constant, or strictly monotone and continuous there. Further retired 2026-09-14: superseded by the same-named formalization without the redundant infinitude hypothesis in the current staging proposal.

Preamble

import Definitions.Def_Monotonicity_Theorem_Framework

Formal statement

theorem Monotonicity_Theorem.finite_partition_core {R : Type} (D : DenseLinearOrderNoEndpoints R)
    (M : OMinimalStructure D) {I B : Set (Power R 1)}
    (f : DefinableFunction M I B) (hI : IsInfinite1 I)
    {a b : Power R 1} (hab : Lt1 D a b) :
    exists k : Nat, exists p : Fin (k + 1) -> Power R 1,
      p 0 = a /\ p (Fin.last k) = b /\
      (forall i : Fin k, Lt1 D (p i.castSucc) (p i.succ)) /\
      (forall i : Fin k,
        let J : Set (Power R 1) := openInterval D (Endpoint.finite ((p i.castSucc) 0)) (Endpoint.finite ((p i.succ) 0))
        ((forall x (hxI : I x), J x -> forall y (hyI : I y), J y ->
          f.toFun (Subtype.mk x hxI) = f.toFun (Subtype.mk y hyI)) \/ 
         (((forall x (hxI : I x), J x -> forall y (hyI : I y), J y -> Lt1 D x y ->
            Lt1 D (f.toFun (Subtype.mk x hxI)).1 (f.toFun (Subtype.mk y hyI)).1) \/ 
           (forall x (hxI : I x), J x -> forall y (hyI : I y), J y -> Lt1 D x y ->
            Lt1 D (f.toFun (Subtype.mk y hyI)).1 (f.toFun (Subtype.mk x hxI)).1)) /\ 
          J.Subset (ContinuousPoints D I (FunctionGraph (R := R) (m := 1) (n := 1) (A := I) (B := B) f.toFun))))) := by sorry

Source

Monotonicity theorem root assembly

View graph