The above-below germ pattern forces strict decrease on the interval

Proved

Monotonicity_Theorem.decreasing_of_uniform_above_below_on_interval

by Gabewhigham · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

geometry-topologyo-minimality

Let $M$ be an o-minimal structure over a dense linear order without endpoints $D$ , let $f : I \to B$ be a definable function of one variable, and let $u < v$ satisfy $(u,v) \subseteq I$ .

Claim. If $f$ has the above-below germ pattern on $(u,v)$ , then $f$ is strictly decreasing on $(u,v)$ :

x < y \ \text{ in } (u,v) \ \Longrightarrow \ f(y) < f(x).

This is the mirror image of the increasing case. The hypothesis compares $f$ with the single value $f(x)$ immediately on each side of each point $x$ , and the conclusion compares all pairs. The proof is the definable-connectedness argument applied to the definable set $\{z : f(z) < f(x)\}$ for a fixed $x$ : it has finitely many boundary points, the right half of the germ pattern produces a point of it immediately to the right of any point already reached, and the left half shows it is inherited at a point from the points immediately to its left.

Formalization note. UniformAboveBelow is the predicate of the accompanying definitions and DecOnInterval the strict-decrease predicate of the mission's window-loci definitions.

Preamble

import Definitions.Def_Monotonicity_Theorem_Uniform_Germs

Formal statement

theorem Monotonicity_Theorem.decreasing_of_uniform_above_below_on_interval {R : Type} (D : DenseLinearOrderNoEndpoints R)
    (M : OMinimalStructure D) {I B : Set (Power R 1)} (f : DefinableFunction M I B)
    (u v : R) (huv : D.lt u v)
    (hsub : (openInterval D (Endpoint.finite u) (Endpoint.finite v)).Subset I)
    (hU : UniformAboveBelow D f u v) :
    DecOnInterval f u v := by sorry

Source

Lou van den Dries, Tame Topology and O-minimal Structures, LMS Lecture Note Series 248, CUP 1998, Chapter 3, Section 1, proof of the Monotonicity Theorem (the step showing that an injective definable function is strictly monotone on a subinterval).

View graph