#Contents# * table of contents {:toc} ## Definition ## Given a [[sequentially Cauchy complete Archimedean ordered field]] $\mathbb{R}$, a function $f:\mathbb{R} \to \mathbb{R}$ is strongly extensional if for every $x:\mathbb{R}$ and $y:\mathbb{R}$, $\vert f(x) - f(y) \vert \gt 0$ implies that $\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 ## * [[axiom R-flat]] * [[Brouwer's theorem]] ## References ## * [[Mike Shulman]], Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 ([arXiv:1509.07584](https://arxiv.org/abs/1509.07584), [doi:10.1017/S0960129517000147](https://doi.org/10.1017/S0960129517000147))