nLab locally nonzero function

Definition

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

Examples

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

• Every real polynomial function apart from the zero polynomial function is locally nonzero.

See also

• intermediate value theorem

• monotonic function

• real polynomial function

• locally nonconstant function

References

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