A definable function is constant or injective on a subinterval

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$ be such that $(u,v) \subseteq I$.

Claim. There are $u_1 < v_1$ with $(u_1,v_1) \subseteq (u,v)$ such that $f$ is constant on $(u_1,v_1)$, or $f$ is injective on $(u_1,v_1)$:

This is the first half of the local core of the Monotonicity Theorem. The argument is a dichotomy on the fibres of $f$ over $(u,v)$. Each fibre $f^{-1}(c) \cap (u,v)$ is a definable subset of the line, so by o-minimality it is either finite or contains an interval. If some fibre contains an interval $(u_1,v_1) \subseteq (u,v)$, then $f$ is constant there and the first alternative holds.

Otherwise every fibre meeting $(u,v)$ is finite. Then the image $f\bigl((u,v)\bigr)$ is a definable infinite subset of the line, hence contains an interval $J$. Sending each $c \in J$ to the least element of the finite nonempty set $f^{-1}(c) \cap (u,v)$ gives a definable injection $g : J \to (u,v)$ with $f \circ g = \mathrm{id}_J$, so $f$ is injective on the definable infinite set $g(J)$. By o-minimality $g(J)$ contains an interval $(u_1,v_1)$, which may moreover be shrunk to lie inside $(u,v)$, and $f$ is injective there.

Formalization note. Injectivity on $(u_1,v_1)$ is stated pointwise for points of $I$ lying in $(u_1,v_1)$: if two such points have equal $f$-values then they are equal. Constancy is the predicate ConstOnInterval of the mission's window-loci definitions.