nLab locally nonconstant function

Contents

Contents

Definition

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

Examples

See also

References

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

Last revised on June 2, 2022 at 16:22:42. See the history of this page for a list of all contributions to it.