Homotopy Type Theory strongly extensional function > history (Rev #1)



Given a sequentially Cauchy complete Archimedean ordered field \mathbb{R}, a function f:f:\mathbb{R} \to \mathbb{R} is strongly extensional if for every x:x:\mathbb{R} and y:y:\mathbb{R}, |f(x)f(y)|>0\vert f(x) - f(y) \vert \gt 0 implies that |xy|>0\vert x - y \vert \gt 0.

In particular, this definition applies to Dedekind real numbers, which is used for proving Brouwer's theorem? in real-cohesive homotopy type theory.

See also


Revision on June 12, 2022 at 04:13:23 by Anonymous?. See the history of this page for a list of all contributions to it.