Lemma 3, monotone implies continuous somewhere

Proved

Monotonicity_Theorem.lemma_three2

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

geometry-topologyo-minimality

A strictly monotone definable function is continuous on a subinterval.

Preamble

import Definitions.Def_Monotonicity_Theorem_Framework2

Formal statement

theorem Monotonicity_Theorem.lemma_three2 {R : Type} [LinearOrder R] [DenselyOrdered R] [NoMaxOrder R] [NoMinOrder R] (M : OMinimalStructure R)
    {I B : Set (Power R 1)} (f : DefinableFunction M I B)
    (hmono : StrictlyMonotoneOn I B f.toFun) (hI : Set.Infinite I) :
    ∃ a b : Endpoint R, Endpoint.lt a b ∧
      (openInterval a b).Subset I ∧
      (openInterval a b).Subset (ContinuousPoints I
        (FunctionGraph (R := R) (m := 1) (n := 1) (A := I) (B := B) 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

For any type $R$ equipped with a linear order that is densely ordered and has no maximum and no minimum, and any o-minimal structure $M$ over $R$ , and any sets $I$ and $B$ of unary tuples over $R$ , and any $M$ -definable function $f$ from $I$ to $B$ , if the underlying ordinary function of $f$ is strictly monotone on $I$ with values in $B$ and if $I$ is infinite as a set, so in particular $I$ is not empty or finite, then there exist endpoints $a$ and $b$ over $R$ , allowing infinite ends, such that $a$ is strictly less than $b$ in the endpoint order, hence excluding degenerate empty or reversed endpoint configurations, and the open interval determined by $a$ and $b$ is contained as a subset in $I$ , and that same open interval is also contained as a subset in the set of continuity points in $I$ of the function-graph, viewed as a $1$ -to- $1$ -ary graph with domain $I$ and codomain $B$ , of the underlying function of $f$ , where both containments are required jointly and would hold vacuously only if the interval were empty.

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