## Definition ## ### Discontinuous intermediate value theorem ### Let $f:\mathbb{R} \to \mathbb{R}$ be a continuous mapping on the space of Dedekind real numbers, and let $c:p_{*}(\mathbb{R})$ be a term of the underlying homotopy type of the Dedekind real numbers. If we assume [[excluded middle]], [[axiom R-flat]], and the [[analytic Markov's principle]], then if there exist points $a, b:\mathbb{R}$ such that $p_*(f)(p_*(a)) \lt c \lt p_*(f)(p_*(b))$, then there exists a point $x:\mathbb{R}$ such that $p_*(f)(p_*(x)) = c$ ### Approximate intermediate value theorem ### Let $f:\mathbb{R} \to \mathbb{R}$ be a continuous mapping on the Dedekind real numbers, and let $c:p_{*}(\mathbb{R})$ be a term of the underlying homotopy type of the Dedekind real numbers. If we assume [[axiom R-flat]], then if there exist points $a, b:\mathbb{R}$ such that $p_*(f)(p_*(a)) \lt c \lt p_*(f)(p_*((b))$, then for all terms $\epsilon \gt 0$ there exists a point $x:\mathbb{R}$ such that $\vert p_*(f)(p_*(x)) - c \vert \lt \epsilon$ ## See also ## * [[axiom R-flat]] ## 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))