Decreasing on a uniform below-below window

Proved

Monotonicity_Theorem.decreasing_of_uniform_below_below2

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

geometry-topologyo-minimality

If every point of a window has a below-below sign pattern, some subwindow has the function strictly decreasing. The difficult below case of Lemma 2. Retired: the window was not required to be nonempty, so the statement is false as stated; use Monotonicity_Theorem.decreasing_of_uniform_below_below_corrected instead. Further retired 2026-09-14: old-framework statement superseded by the same-named new-framework formalization in the current staging proposal; the _corrected successor names are retired, use the clean names.

Preamble

import Definitions.Def_Monotonicity_Theorem_Framework2

Formal statement

theorem Monotonicity_Theorem.decreasing_of_uniform_below_below2 {R : Type} [LinearOrder R] [DenselyOrdered R] [NoMaxOrder R] [NoMinOrder R]
    (M : OMinimalStructure R) {I B : Set (Power R 1)}
    (f : DefinableFunction M I B)
    (hinj : ∀ x y (hx : I x) (hy : I y),
      f.toFun (Subtype.mk x hx) = f.toFun (Subtype.mk y hy) → x = y)
    {a b : Endpoint R} (hsubJ : ∀ x, openInterval a b x → I x)
    (hlt : Endpoint.lt a b)
    (hU : ∀ x (hxI : I x), openInterval a b x ->
        ∃ c1 c2 : Power R 1, openInterval a b c1 ∧ openInterval a b c2 ∧
        Lt1 c1 x ∧ Lt1 x c2 ∧
        (∀ y (hyI : I y), openInterval a b y → Lt1 c1 y → Lt1 y x ->
          Lt1 (f.toFun (Subtype.mk y hyI)).1 (f.toFun (Subtype.mk x hxI)).1) ∧
        (∀ y (hyI : I y), openInterval a b y → Lt1 x y → Lt1 y c2 ->
          Lt1 (f.toFun (Subtype.mk y hyI)).1 (f.toFun (Subtype.mk x hxI)).1)) :
    ∃ a2 b2 : Endpoint R, Endpoint.lt a2 b2 ∧
      (∀ x, openInterval a2 b2 x → I x) ∧
      (∀ x (hxI : I x) y (hyI : I y), openInterval a2 b2 x → openInterval a2 b2 y ->
        Lt1 x y → Lt1 (f.toFun (Subtype.mk y hyI)).1 (f.toFun (Subtype.mk x hxI)).1) := 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

Let $R$ be a type equipped with a linear order that is densely ordered 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$ , and let $f$ be a function definable in $M$ from $I$ to $B$ , writing $f(x)$ for the underlying unary tuple assigned to $x$ in $I$ ; suppose $f$ is injective on $I$ in the sense that for any $x,y$ belonging to $I$ , if $f(x)$ equals $f(y)$ as unary tuples then $x$ equals $y$ ; let $a$ and $b$ be endpoints over $R$ , where an open interval determined by such endpoints is the collection of unary tuples strictly between them and one endpoint is strictly less than another in the endpoint order, such that every unary tuple in the open interval $(a,b)$ belongs to $I$ and $a$ is strictly less than $b$ , so the interval is nondegenerate and, in the dense order without ends, contains points and hence forces $I$ to be nonempty; suppose further the following uniform two-sided below property holds: for every $x$ belonging both to $I$ and to $(a,b)$ , there exist unary tuples $c_1,c_2$ belonging to $(a,b)$ with $c_1$ strictly less than $x$ and $x$ strictly less than $c_2$ in the strict order $<_1$ on unary tuples, such that for every $y$ belonging both to $I$ and to $(a,b)$ , if $y$ lies strictly between $c_1$ and $x$ then $f(y)$ is strictly $<_1$ -less than $f(x)$ , and if $y$ lies strictly between $x$ and $c_2$ then $f(y)$ is strictly $<_1$ -less than $f(x)$ , where the bracketing points $c_1,c_2$ may depend on $x$ ; then there exist endpoints $a_2$ and $b_2$ with $a_2$ strictly less than $b_2$ , such that every unary tuple in $(a_2,b_2)$ belongs to $I$ and $f$ is strictly decreasing on $(a_2,b_2)$ intersected with $I$ in the sense that for any $x,y$ belonging to $I$ and to $(a_2,b_2)$ , if $x$ is strictly $<_1$ -less than $y$ then $f(y)$ is strictly $<_1$ -less than $f(x)$ , a condition that is vacuously true if there are fewer than two such comparable points.

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