Homotopy Type Theory intermediate value theorem > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

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_{*}(ℝ)$ c:p_{*}(\mathbb{R}) c:\mathbb{R} be a term of the underlying homotopy type of the Dedekind real numbers. number. If we assumeaxiom R-flat, then if there exist points $a, b:\mathbb{R}$ such that $p_{*}(f)(p_{*}(a))<c<p_{*}(f)(p_{*}((b))$ p_*(f)(p_*(a)) f(a)) \lt c \lt p_*(f)(p_*((b)) f(b)), then for all terms $\epsilon \gt 0$ there exists a point $x:\mathbb{R}$ such that $|p_{*}(f)(p_{*}(x))-c|<ϵ$ \vert p_*(f)(p_*(x)) f(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 (

  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, doi:10.1017/S0960129517000147)

  arXiv:1509.07584 , doi:10.1017/S0960129517000147)

• Matthew Frank, Interpolating Between Choices for the Approximate Intermediate Value Theorem, Logical Methods in Computer Science Vol 16 (3) (July 14, 2020) (arXiv:1701.02227, doi=10.23638/LMCS-16(3:5)20202020))