Let be a continuous mapping on the space of Dedekind real numbers, and let 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 such that , then there exists a point such that
Approximate intermediate value theorem
Let be a continuous mapping on the Dedekind real numbers, and let be a term of the underlying homotopy type of the Dedekind real numbers. If we assume axiom R-flat, then if there exist points such that , then for all terms there exists a point such that