Homotopy Type Theory intermediate value theorem > history (changes)

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

Definition

< intermediate value theorem

Discontinuous intermediate value theorem

Let f:f:\mathbb{R} \to \mathbb{R} be a continuous mapping on the space of Dedekind real numbers, and let c:p *()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:a, b:\mathbb{R} such that p *(f)(p *(a))<c<p *(f)(p *(b))p_*(f)(p_*(a)) \lt c \lt p_*(f)(p_*(b)), then there exists a point x:x:\mathbb{R} such that p *(f)(p *(x))=cp_*(f)(p_*(x)) = c

Approximate intermediate value theorem

Let f:f:\mathbb{R} \to \mathbb{R} be a continuous mapping on the Dedekind real numbers, and let c:c:\mathbb{R} be a Dedekind real number. If we assume axiom R-flat, then if there exist points a,b:a, b:\mathbb{R} such that f(a))<c<f(b))f(a)) \lt c \lt f(b)), then for all terms ϵ>0\epsilon \gt 0 there exists a point x:x:\mathbb{R} such that |f(x))c|<ϵ\vert f(x)) - c \vert \lt \epsilon

See also

References

Last revised on June 14, 2022 at 13:34:42. See the history of this page for a list of all contributions to it.