A nontrivial element of $F$ pushes a dyadic interval off itself

Let $f$ be an element of Thompson's group $F$, realised as an order isomorphism of the unit interval $[0,1]$, and suppose $f \neq 1$. Then there is a closed interval

with dyadic rational endpoints which $f$ moves completely off itself:

In the formal statement this disjointness is written pointwise: for every $z \in [0,1]$ with $a \le z \le b$ one has $f(z) \notin [a,b]$.

The statement is an existence assertion about a single nontrivial group element, and it is the geometric input to the simplicity argument for $[F,F]$: it produces an interval on which one may install auxiliary elements whose $f$-conjugates have disjoint support, so that the two families commute.

The mechanism is monotonicity. Since $f \neq 1$ there is a point $t \in [0,1]$ with $f(t) \neq t$. If $f(t) > t$, choose dyadic rationals $a, b$ with

then $a > 0$ because $t \ge 0$, and $b < 1$ because $f(t) \le 1$, while for $z \in [a,b]$ monotonicity gives $f(z) > f(t) > b$, so $f(z) \notin [a,b]$. If $f(t) < t$, choose dyadic $a, b$ with $f(t) < a < b < t$ and argue symmetrically: for $z \in [a,b]$ one has $z < t$, hence $f(z) < f(t) < a$.