Lemma 2, injective implies locally monotone

Proved

Monotonicity_Theorem.lemma_two

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

geometry-topologyo-minimality

An injective definable map has a nonempty open subwindow on which it is strictly increasing or strictly decreasing. Second step of the monotonicity argument.

Preamble

import Definitions.Def_Monotonicity_Theorem_Framework2

Formal statement

theorem Monotonicity_Theorem.lemma_two {R : Type} [LinearOrder R] [DenselyOrdered R] [NoMaxOrder R] [NoMinOrder R] (M : OMinimalStructure R)
    {I B : Set (Power R 1)} (f : DefinableFunction M I B) (hI : Set.Infinite I)
    (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, Endpoint.lt a b ∧
      (∀ x, openInterval a b x → I x) ∧
      ((∀ x (hxI : I x) y (hyI : I y), openInterval a b x → openInterval a b y ->
          Lt1 x y → Lt1 (f.toFun (Subtype.mk x hxI)).1 (f.toFun (Subtype.mk y hyI)).1) ∨
       (∀ x (hxI : I x) y (hyI : I y), openInterval a b x → openInterval a b 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 dense and has neither a maximum nor a 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 definable in $M$ from $I$ to $B$ , suppose $I$ is infinite as a set, and suppose $f$ is injective in the sense that for any tuples $x,y$ together with proofs that $x$ belongs to $I$ and $y$ belongs to $I$ , equality of the values of the underlying function of $f$ at the corresponding elements of $I$ implies $x=y$ ; then there exist endpoints $a$ and $b$ over $R$ such that $a$ is strictly less than $b$ , every tuple $x$ belonging to the open interval bounded by $a$ and $b$ belongs to $I$ , and either the first alternative holds or the second alternative holds, where the first alternative is that for all $x$ in $I$ and all $y$ in $I$ , if $x$ lies in the open interval $(a,b)$ and $y$ lies in the open interval $(a,b)$ and $x$ is strictly less than $y$ in the strict order on unary tuples, then the unary-tuple value of $f$ at $x$ is strictly less than the unary-tuple value of $f$ at $y$ , and the second alternative is that for all $x$ in $I$ and all $y$ in $I$ , if $x$ lies in $(a,b)$ and $y$ lies in $(a,b)$ and $x$ is strictly less than $y$ in the strict order on unary tuples, then the value of $f$ at $y$ is strictly less than the value of $f$ at $x$ .

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