\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{intermediate value theorem}

\hypertarget{the_intermediate_value_theorem}{}\section*{{The intermediate value theorem}}\label{the_intermediate_value_theorem}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{statements}{Statements}\dotfill \pageref*{statements} \linebreak
\noindent\hyperlink{proofs}{Proofs}\dotfill \pageref*{proofs} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

The \emph{intermediate value theorem} (IVT) is a fundamental principle of [[analysis]] which allows one to find a desired value by [[interpolation]]. It says that a [[continuous function]] $f \colon [0,1] \to \mathbb{R}$ from an [[interval]] to the [[real numbers]] (all with its [[Euclidean space|Euclidean]] [[topological space|topology]]) takes all values in between $f(0)$ and $f(1)$.

The IVT in its general form was not used by [[Euclid]]. Although it is hard to doubt that Euclid believed that, for any given angle, there was an angle with one-third the measure, this angle cannot be constructed by the methods available to Euclid, so he would never refer to it (see at \emph{[[Euclidean geometry]]}). In contrast, [[Archimedes]] made general arguments in which a quantity is approached from above and below, allowing him not only to trisect the angle but also to calculate [[pi|π]].

As normally stated, the IVT is not valid in [[constructive mathematics]], although there are constructively valid versions.

I've decided that I don't really like how I've been writing this, and I'm working on a new version. (Aside from its intrinsic interest and practical usefulness, this is such a classic example of the differences between classical and constructive analysis that I want to get it right.) That shouldn't stop anybody from putting here what \emph{they} find useful, but I thought that a warning might be in order. ---[[Toby Bartels]]

\hypertarget{statements}{}\subsection*{{Statements}}\label{statements}

\begin{theorem}
\label{classical}\hypertarget{classical}{}
(classical IVT, assuming [[excluded middle]])

Let $f\colon [0,1] \to \mathbb{R}$ be a [[continuous function]] from the [[unit interval]] to the [[real line]], and suppose that $f(0) \lt 0$ while $f(1) \gt 0$. Then there exists a point $c$ in the unit interval such that $f(c) = 0$.

\end{theorem}
\begin{proof}
By \href{connected+topological+space}{this example} the interval $[0,1]$ is a [[connected topological space]] (this is where [[excluded middle]] is used).

By \href{connected+topological+space}{this prop.} also its [[image]] $f([0,1]) \subset \mathbb{R}$ is connected. By \href{connected+topological+space}{this example} that image is itself an interval. This implies the claim.

\end{proof}
\begin{theorem}
\label{conclusion}\hypertarget{conclusion}{}
(constructive IVT with weakened conclusion)

Let $f\colon [0,1] \to \mathbb{R}$ be a [[uniformly continuous map|uniformly continuous function]] from the [[unit interval]] to the [[real line]], and suppose that $f(0) \lt 0$ while $f(1) \gt 0$. Then for every positive number $\epsilon$ there exists a point $c_\epsilon$ in the unit interval such that ${|f(c_\epsilon)|} \lt \epsilon$.

\end{theorem}
\begin{theorem}
\label{hypothesis}\hypertarget{hypothesis}{}
(constructive IVT with strengthened hypothesis, assuming [[weak countable choice]])

Let $f\colon [0,1] \to \mathbb{R}$ be a [[uniformly continuous map|uniformly continuous function]] from the [[unit interval]] to the [[real line]], and suppose that $f(0) \lt 0$ while $f(1) \gt 0$. Suppose further that, for any points $a,b$ in the unit interval with $a \lt b$, there exists a point $c_{a,b}$ such that $a \lt c_{a,b} \lt b$ and ${|f(c_{a,b})|} \gt 0$. (In other words, the non-[[zero set]] $\{ c : {|f(c)|} \gt 0 \}$ is [[dense subspace|dense]].) Then there exists a point $c$ in the unit interval such that $f(c) = 0$.

\end{theorem}
In the constructive versions, we have changed from a continuous function to a uniformly continuous one just to be safe; while some varieties of constructive analysis accept the theorem that any continous function on $[0,1]$ is uniformly continous, others do not, and some even refute it. In any case, even the classical version only applies to uniformly continuous functions, even though the classical mathematician is free to leave out the word `uniformly' and so usually does. The more significant change is to either weaken the conclusion to an \emph{approximate} zero, or to strengthen the hypothesis to forbid functions that `hover' near zero on some subinterval; even interpreted classically, these are prima facie weaker results.

There are obvious generalisations in which the domain $[0,1]$ is generalised to any compact interval, in which the signs of $f(0)$ and $f(1)$ are swapped, and in which the desired value $f(c) = 0$ is generalised to any real number. They may be proved either by modifying a proof of the main theorem or as a corollary by linearly transforming the input and output of $f$.

\hypertarget{proofs}{}\subsection*{{Proofs}}\label{proofs}

We will prove Theorem \ref{conclusion} in a constructive manner, which (besides satisfying the constructive mathematicians) demonstrates an algorithm for approximating the point $c$ as closely as desired. Theorems \ref{classical} and \ref{hypothesis} are then easy to prove (the latter constructively, the former not) as corollaries.

\begin{proof}
Since $f$ is uniformly continuous, there exists a positive number $\delta$ such that ${|f(x) - f(y)|} \lt \epsilon/2$ whenever ${|x - y|} \lt \delta$. Since $\delta$ is positive, there exists a [[natural number]] $n$ such that $\delta \gt 2^{-n}$. We will approximate $c_\epsilon$ in $n$ steps.

We will define finite [[sequences]] $(a_1,\ldots,a_n)$, $(b_1,\ldots,b_n)$, and $(c_1,\ldots,c_n)$ such that $a_k \lt c_k \lt b_k$ at each stage. To begin with, let $a_1 \coloneqq 0$ and $b_1 \coloneqq 1$. At each stage, let $c_k$ be the arithmetic mean of $a_k$ and $b_k$. By the [[comparison]] property of the [[linear order]] $\lt$, either $f(c_k) \gt -\epsilon/2$ or $f(c_k) \lt \epsilon/2$;

\begin{itemize}%
\item if the former, then let $a_{k+1} \coloneqq a_k$ and $b_{k+1} \coloneqq c_k$,
\item if the latter, then let $a_{k+1} \coloneqq c_k$ and $b_{k+1} \coloneqq b_k$.

\end{itemize}
Either way, we have $a_{k+1} \lt b_{k+1}$, so we can continue.

At each stage, we have

\begin{itemize}%
\item $f(a_k) \lt \epsilon/2$,
\item $f(b_k) \gt - \epsilon/2$,
\item $c_k - a_k = 2^k$,
\item $b_k - c_k = 2^k$.

\end{itemize}
Therefore, $-\epsilon \lt f(b_n) - \epsilon/2 \lt f(c_n) \lt f(a_k) + \epsilon/2 \lt \epsilon$, so $c_n$ is the $c_\epsilon$ desired.

\end{proof}
This is the \emph{bisection algorithm} in [[numerical analysis]]. Note that this algorithm always chooses $c_\epsilon$ to be a [[dyadic rational]]. Slight variations will allow $c_\epsilon$ to be drawn from any previously chosen [[dense subspace]] of $[0,1]$ (or this can be proved as a corollary).

\begin{proof}
Suppose that $f$ satisfies the additional hypothesis (and assume [[weak countable choice]]).

\ldots{}

\end{proof}
I'm not sure how to finish this, and maybe it's a mistake! Certainly the result follows from [[countable choice]], but I had thought that it followed from \emph{weak} countable choice. (The proof from countable choice is to continue the bisection algorithm for infinitely many steps and take $\lim_n c_n$.) There certainly ought to be a proof that uses only excluded middle (which implies $WCC$), since Theorem \ref{classical} needs only that.

\begin{proof}
By way of contradiction (applying the [[double negation]] law of [[classical logic]]), suppose that ${|f(c)|} \gt 0$ for every $c$ in $[0,1]$. Then the extra hypothesis of Theorem \ref{hypothesis} is certainly satisfied, so there exists some $c$ such that $f(c) = 0$ after all. (Constructively, this is enough to show that the classical theorem has no counterexample.)

\end{proof}
Of course, we can also prove Theorems \ref{classical} and \ref{hypothesis} directly by modifying the proof of Theorem \ref{conclusion} appropriately.

Other ways to identify $c$ (in Theorem \ref{classical} or \ref{hypothesis}) are as the [[supremum]] of $\{x \;|\; f(x) \lt 0\}$ and as the point (guaranteed by the [[extreme value theorem]]) where the minimum of ${|f|}$ is attained. (After accepting these non-constructive results, the proof that the value $c$ so found satisfies $f(c) = 0$, while perhaps non-trivial, is constructive without choice, given uniform continuity, or in the first case given only continuity at $c$.)

\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item [[Peter Schuster]]; Unique existence, approximate solutions, and countable choice; \href{http://dx.doi.org/10.1016/S0304-3975%2802%2900707-7}{doi}.


\item Matt F.; answer to Approximate intermediate value theorem in pure constructive mathematics; MathOverflow; \href{http://mathoverflow.net/q/255371}{web}.


\item [[Paul Taylor]]; The intermediate value theorem; A lambda calculus for real analysis, 14; \href{http://www.paultaylor.eu/ASD/lamcra/asdivt}{web}.



\end{itemize}
[[!redirects intermediate value theorem]] [[!redirects intermediate value theorems]] [[!redirects Intermediate Value Theorem]] [[!redirects IVT]]



\end{document}