Lemma 1, constant or injective window

Proved

Monotonicity_Theorem.lemma_one

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

geometry-topologyo-minimality

A definable map on an infinite domain has a nonempty open subwindow on which it is either constant or injective. First step of the monotonicity argument.

Preamble

import Definitions.Def_Monotonicity_Theorem_Framework2

Formal statement

theorem Monotonicity_Theorem.lemma_one {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) :
    ∃ a b : Endpoint R, Endpoint.lt a b ∧
      (openInterval a b).Subset I ∧
      ((∀ x (hxI : I x), openInterval a b x → ∀ y (hyI : I y), openInterval a b y →
          f.toFun (Subtype.mk x hxI) = f.toFun (Subtype.mk y hyI)) ∨
       (∀ x (hxI : I x), openInterval a b x → ∀ y (hyI : I y), openInterval a b y →
          f.toFun (Subtype.mk x hxI) = f.toFun (Subtype.mk y hyI) → x = y)) := 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 $1$ -tuples over $R$ , let $f$ be a function from $I$ to $B$ definable relative to $M$ , and assume $I$ is infinite; then there exist endpoints $a$ and $b$ over $R$ such that $a$ is strictly less than $b$ , every $1$ -tuple in the open interval $(a,b)$ belongs to $I$ , and at least one of the following two alternatives holds, each quantifying only over those $x$ and $y$ that both belong to $I$ and belong to $(a,b)$ with $f$ applied to $x$ and $y$ regarded as elements of $I$ : either for all such $x$ and $y$ the values of $f$ at $x$ and $y$ are equal, or for all such $x$ and $y$ equality of the values of $f$ at $x$ and $y$ implies $x=y$ .

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