nLab locally nonconstant function

Definition

A function $f:\mathbb{R}_D \to \mathbb{R}_D$ is locally nonconstant if for all Dedekind real numbers $x \lt y$ and $t \in \mathbb{R}_D$, there exists a Dedekind real number $z \in \mathbb{R}_D$ with $x \lt z \lt y$ and $\vert f(z) - t \vert \gt 0$.

Examples

• Every monotonic function on the Dedekind real numbers is locally nonconstant.

• Every real polynomial function apart from the constant functions is locally nonconstant.

See also

• intermediate value theorem

• monotonic function

• real polynomial function

• locally nonzero function

References

• Auke Booij, Extensional constructive real analysis via locators, (arXiv:1805.06781)