CINXE.COM

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> intermediate value theorem (changes) in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="noindex,nofollow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><![CDATA[/*></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <![CDATA[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> intermediate value theorem (changes) </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/diff/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussion/13123/#Item_6" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <p class="show_diff"> Showing changes from revision #22 to #23: <ins class="diffins">Added</ins> | <del class="diffdel">Removed</del> | <del class="diffmod">Chan</del><ins class="diffmod">ged</ins> </p> <div class='rightHandSide'> <div class='toc clickDown' tabindex='0'> <h3 id='context'>Context</h3> <h4 id='analysis'>Analysis</h4> <div class='hide'> <p><strong><a class='existingWikiWord' href='/nlab/show/diff/analysis'>analysis</a></strong> (<a class='existingWikiWord' href='/nlab/show/diff/differential+calculus'>differential</a>/<a class='existingWikiWord' href='/nlab/show/diff/integral+calculus'>integral</a> <a class='existingWikiWord' href='/nlab/show/diff/calculus'>calculus</a>, <a class='existingWikiWord' href='/nlab/show/diff/functional+analysis'>functional analysis</a>, <a class='existingWikiWord' href='/nlab/show/diff/topology'>topology</a>)</p> <p><a class='existingWikiWord' href='/nlab/show/diff/epsilontic+analysis'>epsilontic analysis</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/infinitesimal+analysis'>infinitesimal analysis</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/computable+analysis'>computable analysis</a></p> <p><em><a class='existingWikiWord' href='/nlab/show/diff/Introduction+to+Topology+--+1'>Introduction</a></em></p> <h2 id='basic_concepts'>Basic concepts</h2> <p><a class='existingWikiWord' href='/nlab/show/diff/triangle+inequality'>triangle inequality</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/metric+space'>metric space</a>, <a class='existingWikiWord' href='/nlab/show/diff/norm'>normed vector space</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/ball'>open ball</a>, <a class='existingWikiWord' href='/nlab/show/diff/open+subspace'>open subset</a>, <a class='existingWikiWord' href='/nlab/show/diff/neighborhood'>neighbourhood</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/metric+topology'>metric topology</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/sequence'>sequence</a>, <a class='existingWikiWord' href='/nlab/show/diff/net'>net</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/convergence'>convergence</a>, <a class='existingWikiWord' href='/nlab/show/diff/convergence'>limit of a sequence</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/compact+space'>compactness</a>, <a class='existingWikiWord' href='/nlab/show/diff/sequentially+compact+topological+space'>sequential compactness</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/differentiation'>differentiation</a>, <a class='existingWikiWord' href='/nlab/show/diff/integral'>integration</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/topological+vector+space'>topological vector space</a></p> <h2 id='basic_facts'>Basic facts</h2> <p><a class='existingWikiWord' href='/nlab/show/diff/continuous+metric+space+valued+function+on+compact+metric+space+is+uniformly+continuous'>continuous metric space valued function on compact metric space is uniformly continuous</a></p> <p>…</p> <h2 id='theorems'>Theorems</h2> <p><a class='existingWikiWord' href='/nlab/show/diff/intermediate+value+theorem'>intermediate value theorem</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/extreme+value+theorem'>extreme value theorem</a></p> <p><a class='existingWikiWord' href='/nlab/show/diff/Heine-Borel+theorem'>Heine-Borel theorem</a></p> <p>…</p> </div> </div> </div> <h1 id='the_intermediate_value_theorem'>The intermediate value theorem</h1> <div class='maruku_toc'><ul><li><a href='#idea'>Idea</a></li><li><a href='#statements_and_proofs'>Statements and Proofs</a><ul><li><a href='#classical_ivt'>Classical IVT</a></li><li><a href='#constructive_ivt_with_weakened_conclusion'>Constructive IVT with weakened conclusion</a></li><li><a href='#constructive_ivt_with_strengthened_hypothesis'>Constructive IVT with strengthened hypothesis</a></li></ul></li><li><a href='#see_also'>See also</a></li><li><a href='#references'>References</a></li></ul></div> <h2 id='idea'>Idea</h2> <p>The <em>intermediate value theorem</em> (IVT) is a fundamental principle of <a class='existingWikiWord' href='/nlab/show/diff/analysis'>analysis</a> which allows one to find a desired value by <a class='existingWikiWord' href='/nlab/show/diff/interpolation'>interpolation</a>. It says that a <a class='existingWikiWord' href='/nlab/show/diff/continuous+map'>continuous function</a> <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_1' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo lspace='verythinmathspace'>:</mo><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy='false'>]</mo><mo>→</mo><mi>ℝ</mi></mrow><annotation encoding='application/x-tex'>f \colon [0,1] \to \mathbb{R}</annotation></semantics></math> from an <a class='existingWikiWord' href='/nlab/show/diff/interval'>interval</a> to the <a class='existingWikiWord' href='/nlab/show/diff/real+number'>real numbers</a> (all with its <a class='existingWikiWord' href='/nlab/show/diff/Euclidean+space'>Euclidean</a> <a class='existingWikiWord' href='/nlab/show/diff/topological+space'>topology</a>) takes all values in between <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_2' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mn>0</mn><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>f(0)</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_3' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mn>1</mn><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>f(1)</annotation></semantics></math>.</p> <p>The IVT in its general form was not used by <a class='existingWikiWord' href='/nlab/show/diff/Euclid'>Euclid</a>. 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 <em><a class='existingWikiWord' href='/nlab/show/diff/Euclidean+geometry'>Euclidean geometry</a></em>). In contrast, <a class='existingWikiWord' href='/nlab/show/diff/Archimedes'>Archimedes</a> 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 <a class='existingWikiWord' href='/nlab/show/diff/pi'>π</a>.</p> <p>As normally stated, the IVT is not valid in <a class='existingWikiWord' href='/nlab/show/diff/constructive+mathematics'>constructive mathematics</a>, although there are constructively valid versions. These versions either weaken the conclusion to an <em>approximate</em> zero, or to strengthen the hypothesis to require the functions satisfy additional properties or have other structures, such as locally nonconstancy and lifting to locators in functions in the given example below. Even interpreted classically, these are prima facie weaker results.</p> <h2 id='statements_and_proofs'>Statements and Proofs</h2> <h3 id='classical_ivt'>Classical IVT</h3> <div class='num_theorem' id='classical'> <h6 id='theorem'>Theorem</h6> <p>(classical IVT, assuming <a class='existingWikiWord' href='/nlab/show/diff/excluded+middle'>excluded middle</a>)</p> <p>Let <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_4' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo lspace='verythinmathspace'>:</mo><mo stretchy='false'>[</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy='false'>]</mo><mo>→</mo><mi>ℝ</mi></mrow><annotation encoding='application/x-tex'>f\colon [a,b] \to \mathbb{R}</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/continuous+map'>continuous function</a> from a <a class='existingWikiWord' href='/nlab/show/diff/compact+space'>compact</a> <a class='existingWikiWord' href='/nlab/show/diff/interval'>closed interval</a> to the <a class='existingWikiWord' href='/nlab/show/diff/real+number'>real line</a>, and suppose that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_5' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>a</mi><mo stretchy='false'>)</mo><mo><</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(a) \lt 0</annotation></semantics></math> while <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_6' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>b</mi><mo stretchy='false'>)</mo><mo>></mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(b) \gt 0</annotation></semantics></math>. Then there exists a point <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_7' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>c</mi></mrow><annotation encoding='application/x-tex'>c</annotation></semantics></math> in the unit interval such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_8' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>c</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(c) = 0</annotation></semantics></math>.</p> </div> <div class='proof'> <h6 id='proof'>Proof</h6> <p>Let <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_9' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>g</mi><mo>:</mo><mi>ℝ</mi><mo>→</mo><mi>ℝ</mi></mrow><annotation encoding='application/x-tex'>g:\mathbb{R} \to \mathbb{R}</annotation></semantics></math> be defined as <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_10' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>g</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>≔</mo><mo stretchy='false'>(</mo><mi>b</mi><mo>−</mo><mi>a</mi><mo stretchy='false'>)</mo><mi>x</mi><mo>+</mo><mi>a</mi></mrow><annotation encoding='application/x-tex'>g(x) \coloneqq (b - a) x + a</annotation></semantics></math><span> . Then<del class='diffmod'> there</del><ins class='diffmod'> we</ins><del class='diffmod'> exists</del><ins class='diffmod'> can</ins><ins class='diffins'> define</ins> a function</span><math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_11' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>h</mi><mo>:</mo><mo stretchy='false'>[</mo><del class='diffdel'><mn>1</mn></del><del class='diffdel'><mo>,</mo></del><mn>0</mn><ins class='diffins'><mo>,</mo></ins><ins class='diffins'><mn>1</mn></ins><mo stretchy='false'>]</mo><mo>→</mo><mi>ℝ</mi></mrow><annotation encoding='application/x-tex'><span><del class='diffmod'> h:[1,0]</del><ins class='diffmod'> h:[0,1]</ins> \to \mathbb{R}</span></annotation></semantics></math><span> <del class='diffmod'> such</del><ins class='diffmod'> by</ins><del class='diffdel'> that</del></span><math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_12' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><ins class='diffins'><mi>h</mi></ins><ins class='diffins'><mo>≔</mo></ins><mi>f</mi><del class='diffdel'><mo>=</mo></del><del class='diffdel'><mi>g</mi></del><mo>∘</mo><mi><span><del class='diffmod'> h</del><ins class='diffmod'> g</ins></span></mi></mrow><annotation encoding='application/x-tex'><span><ins class='diffins'> h</ins><ins class='diffins'> \coloneqq</ins> f<del class='diffdel'> =</del><del class='diffdel'> g</del> \circ<del class='diffmod'> h</del><ins class='diffmod'> g</ins></span></annotation></semantics></math>.</p> <p>By <a href='connected+topological+space'>this example</a> the interval <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_13' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>[0,1]</annotation></semantics></math> is a <a class='existingWikiWord' href='/nlab/show/diff/connected+space'>connected topological space</a> (this is where <a class='existingWikiWord' href='/nlab/show/diff/excluded+middle'>excluded middle</a> is used).</p> <p>By <a href='connected+topological+space'>this prop.</a> also its <a class='existingWikiWord' href='/nlab/show/diff/image'>image</a> <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_14' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy='false'>]</mo><mo stretchy='false'>)</mo><mo>⊂</mo><mi>ℝ</mi></mrow><annotation encoding='application/x-tex'>f([0,1]) \subset \mathbb{R}</annotation></semantics></math> is connected. By <a href='connected+topological+space'>this example</a> that image is itself an interval. This implies the claim is true for <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_15' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>h</mi></mrow><annotation encoding='application/x-tex'>h</annotation></semantics></math>. Since linear functions preserve the properties of an interval being compact and closed, if the claim is true for <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_16' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>h</mi></mrow><annotation encoding='application/x-tex'>h</annotation></semantics></math>, it is true for <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_17' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math>.</p> </div> <h3 id='constructive_ivt_with_weakened_conclusion'>Constructive IVT with weakened conclusion</h3> <div class='num_theorem' id='conclusion'> <h6 id='theorem_2'>Theorem</h6> <p>(constructive IVT with weakened conclusion)</p> <p>For real numbers <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_18' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi></mrow><annotation encoding='application/x-tex'>a</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_19' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>b</mi></mrow><annotation encoding='application/x-tex'>b</annotation></semantics></math>, let <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_20' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo lspace='verythinmathspace'>:</mo><mo stretchy='false'>[</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy='false'>]</mo><mo>→</mo><mi>ℝ</mi></mrow><annotation encoding='application/x-tex'>f\colon [a,b] \to \mathbb{R}</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/pointwise+continuous+function'>pointwise continuous function</a> from the <a class='existingWikiWord' href='/nlab/show/diff/interval'>closed interval</a> <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_21' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>[a, b]</annotation></semantics></math> to the <a class='existingWikiWord' href='/nlab/show/diff/real+number'>real line</a>, and supposed that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_22' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>a</mi><mo stretchy='false'>)</mo><mo><</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(a) \lt 0</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_23' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>b</mi><mo stretchy='false'>)</mo><mo>></mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(b) \gt 0</annotation></semantics></math>. Then for every positive number <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_24' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>\epsilon</annotation></semantics></math> there exists a point <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_25' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>c</mi> <mi>ϵ</mi></msub></mrow><annotation encoding='application/x-tex'>c_\epsilon</annotation></semantics></math> in the unit interval such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_26' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>c</mi> <mi>ϵ</mi></msub><mo stretchy='false'>)</mo><mo stretchy='false'>|</mo></mrow><mo><</mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>{|f(c_\epsilon)|} \lt \epsilon</annotation></semantics></math>.</p> </div> <div class='proof'> <h6 id='proof_of_theorem_'>Proof of Theorem <a class='maruku-ref' href='#conclusion'>2</a>⁠</h6> <p>This proof originally appeared in <a href='#Frank20'>Frank 2020</a>.</p> <p>Let us inductively define the following <a class='existingWikiWord' href='/nlab/show/diff/sequence'>sequences</a>:</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_27' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>a</mi> <mn>0</mn></msub><mo>≔</mo><mi>a</mi></mrow><annotation encoding='application/x-tex'>a_0 \coloneqq a</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_28' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>b</mi> <mn>0</mn></msub><mo>≔</mo><mi>b</mi></mrow><annotation encoding='application/x-tex'>b_0 \coloneqq b</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_29' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>c</mi> <mi>n</mi></msub><mo>≔</mo><mfrac><mrow><msub><mi>a</mi> <mi>n</mi></msub><mo>+</mo><msub><mi>b</mi> <mi>n</mi></msub></mrow><mn>2</mn></mfrac></mrow><annotation encoding='application/x-tex'>c_n \coloneqq \frac{a_n + b_n}{2}</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_30' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>d</mi> <mi>n</mi></msub><mo>≔</mo><mi>max</mi><mrow><mo>(</mo><mn>0</mn><mo>,</mo><mi>min</mi><mrow><mo>(</mo><mfrac><mn>1</mn><mn>2</mn></mfrac><mo>+</mo><mfrac><mrow><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>c</mi> <mi>ϵ</mi></msub><mo stretchy='false'>)</mo></mrow><mi>ϵ</mi></mfrac><mo>,</mo><mn>1</mn><mo>)</mo></mrow><mo>)</mo></mrow></mrow><annotation encoding='application/x-tex'>d_n \coloneqq \max\left(0, \min\left(\frac{1}{2} + \frac{f(c_\epsilon)}{\epsilon}, 1\right)\right)</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_31' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>a</mi> <mrow><mi>n</mi><mo>+</mo><mn>1</mn></mrow></msub><mo>=</mo><msub><mi>c</mi> <mi>n</mi></msub><mo>−</mo><mfrac><mrow><msub><mi>d</mi> <mi>n</mi></msub><mo stretchy='false'>(</mo><mi>b</mi><mo>−</mo><mi>a</mi><mo stretchy='false'>)</mo></mrow><mrow><msup><mn>2</mn> <mrow><mi>n</mi><mo>+</mo><mn>1</mn></mrow></msup></mrow></mfrac></mrow><annotation encoding='application/x-tex'>a_{n + 1} = c_n - \frac{d_n (b - a)}{2^{n + 1}}</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_32' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>a</mi> <mrow><mi>n</mi><mo>+</mo><mn>1</mn></mrow></msub><mo>=</mo><msub><mi>b</mi> <mi>n</mi></msub><mo>−</mo><mfrac><mrow><msub><mi>d</mi> <mi>n</mi></msub><mo stretchy='false'>(</mo><mi>b</mi><mo>−</mo><mi>a</mi><mo stretchy='false'>)</mo></mrow><mrow><msup><mn>2</mn> <mrow><mi>n</mi><mo>+</mo><mn>1</mn></mrow></msup></mrow></mfrac></mrow><annotation encoding='application/x-tex'>a_{n + 1} = b_n - \frac{d_n (b - a)}{2^{n + 1}}</annotation></semantics></math></div> <p>Then</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_33' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>b</mi> <mi>n</mi></msub><mo>−</mo><msub><mi>a</mi> <mi>n</mi></msub><mo>=</mo><mfrac><mrow><mi>b</mi><mo>−</mo><mi>a</mi></mrow><mrow><msup><mn>2</mn> <mi>n</mi></msup></mrow></mfrac></mrow><annotation encoding='application/x-tex'>b_n - a_n = \frac{b - a}{2^n}</annotation></semantics></math></div> <p>and the sequence <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_34' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>c</mi> <mi>n</mi></msub></mrow><annotation encoding='application/x-tex'>c_n</annotation></semantics></math> is a <a class='existingWikiWord' href='/nlab/show/diff/Cauchy+sequence'>Cauchy sequence</a>, because for <a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural numbers</a> <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_35' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>m</mi><mo><</mo><mi>n</mi></mrow><annotation encoding='application/x-tex'>m \lt n</annotation></semantics></math>,</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_36' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><msub><mi>c</mi> <mi>m</mi></msub><mo>−</mo><msub><mi>c</mi> <mi>n</mi></msub><mo stretchy='false'>|</mo><mo>≤</mo><mfrac><mrow><mi>b</mi><mo>−</mo><mi>a</mi></mrow><mrow><msup><mn>2</mn> <mi>m</mi></msup></mrow></mfrac></mrow><annotation encoding='application/x-tex'>\vert c_m - c_n \vert \leq \frac{b - a}{2^m}</annotation></semantics></math></div> <p>Lemma: For every natural number <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_37' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>m</mi></mrow><annotation encoding='application/x-tex'>m</annotation></semantics></math>, either 1. there exists a <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_38' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>j</mi><mo>≤</mo><mi>m</mi></mrow><annotation encoding='application/x-tex'>j \leq m</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_39' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>c</mi> <mi>j</mi></msub><mo stretchy='false'>)</mo><mo><</mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>\vert f(c_j) \lt \epsilon</annotation></semantics></math>, or 2. <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_40' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>a</mi> <mi>m</mi></msub><mo stretchy='false'>)</mo><mo><</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(a_m) \lt 0</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_41' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>b</mi> <mi>m</mi></msub><mo stretchy='false'>)</mo><mo>></mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(b_m) \gt 0</annotation></semantics></math>. This could be proved by induction on natural numbers:</p> <p>When <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_42' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>m</mi><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>m = 0</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_43' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>a</mi> <mn>0</mn></msub><mo stretchy='false'>)</mo><mo>=</mo><mi>f</mi><mo stretchy='false'>(</mo><mi>a</mi><mo stretchy='false'>)</mo><mo><</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(a_0) = f(a) \lt 0</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_44' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>b</mi> <mn>0</mn></msub><mo stretchy='false'>)</mo><mo>=</mo><mi>f</mi><mo stretchy='false'>(</mo><mi>b</mi><mo stretchy='false'>)</mo><mo>></mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(b_0) = f(b) \gt 0</annotation></semantics></math>.</p> <p>Now, assume that the above lemma is true for a particular <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_45' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>m</mi></mrow><annotation encoding='application/x-tex'>m</annotation></semantics></math>. If there exists a <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_46' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>j</mi><mo>≤</mo><mi>m</mi></mrow><annotation encoding='application/x-tex'>j \leq m</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_47' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>c</mi> <mi>j</mi></msub><mo stretchy='false'>)</mo><mo><</mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>\vert f(c_j) \lt \epsilon</annotation></semantics></math>, then there exists a <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_48' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>j</mi><mo>≤</mo><mi>m</mi><mo>+</mo><mn>1</mn></mrow><annotation encoding='application/x-tex'>j \leq m + 1</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_49' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>c</mi> <mi>j</mi></msub><mo stretchy='false'>)</mo><mo><</mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>\vert f(c_j) \lt \epsilon</annotation></semantics></math>. Otherwise, either <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_50' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>2</mn><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>c</mi> <mi>m</mi></msub><mo stretchy='false'>)</mo><mo><</mo><mo lspace='verythinmathspace' rspace='0em'>−</mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>2 f(c_m) \lt -\epsilon</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_51' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>2</mn><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>c</mi> <mi>m</mi></msub><mo stretchy='false'>)</mo><mo>></mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>2 f(c_m) \gt \epsilon</annotation></semantics></math>, or <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_52' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>c</mi> <mi>m</mi></msub><mo stretchy='false'>)</mo><mo stretchy='false'>|</mo><mo>></mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>\vert f(c_m) \vert \gt \epsilon</annotation></semantics></math>.</p> <ul> <li> <p>If <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_53' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>2</mn><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>c</mi> <mi>m</mi></msub><mo stretchy='false'>)</mo><mo><</mo><mo lspace='verythinmathspace' rspace='0em'>−</mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>2 f(c_m) \lt -\epsilon</annotation></semantics></math>, then we define</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_54' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>d</mi> <mi>m</mi></msub><mo>≔</mo><mn>1</mn></mrow><annotation encoding='application/x-tex'>d_m \coloneqq 1</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_55' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>a</mi> <mrow><mi>m</mi><mo>+</mo><mn>1</mn></mrow></msub><mo>≔</mo><msub><mi>a</mi> <mi>m</mi></msub></mrow><annotation encoding='application/x-tex'>a_{m + 1} \coloneqq a_m</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_56' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>b</mi> <mrow><mi>m</mi><mo>+</mo><mn>1</mn></mrow></msub><mo>≔</mo><msub><mi>c</mi> <mi>m</mi></msub></mrow><annotation encoding='application/x-tex'>b_{m + 1} \coloneqq c_m</annotation></semantics></math></div> <p>so that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_57' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>a</mi> <mrow><mi>m</mi><mo>+</mo><mn>1</mn></mrow></msub><mo><</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>a_{m + 1} \lt 0</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_58' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>b</mi> <mrow><mi>m</mi><mo>+</mo><mn>1</mn></mrow></msub><mo>></mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>b_{m + 1} \gt 0</annotation></semantics></math>.</p> </li> <li> <p>If <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_59' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>2</mn><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>c</mi> <mi>m</mi></msub><mo stretchy='false'>)</mo><mo>></mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>2 f(c_m) \gt \epsilon</annotation></semantics></math>, then we define</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_60' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>d</mi> <mi>m</mi></msub><mo>≔</mo><mn>1</mn></mrow><annotation encoding='application/x-tex'>d_m \coloneqq 1</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_61' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>a</mi> <mrow><mi>m</mi><mo>+</mo><mn>1</mn></mrow></msub><mo>≔</mo><msub><mi>c</mi> <mi>m</mi></msub></mrow><annotation encoding='application/x-tex'>a_{m + 1} \coloneqq c_m</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_62' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>b</mi> <mrow><mi>m</mi><mo>+</mo><mn>1</mn></mrow></msub><mo>≔</mo><msub><mi>b</mi> <mi>m</mi></msub></mrow><annotation encoding='application/x-tex'>b_{m + 1} \coloneqq b_m</annotation></semantics></math></div> <p>so that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_63' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>a</mi> <mrow><mi>m</mi><mo>+</mo><mn>1</mn></mrow></msub><mo><</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>a_{m + 1} \lt 0</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_64' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>b</mi> <mrow><mi>m</mi><mo>+</mo><mn>1</mn></mrow></msub><mo>></mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>b_{m + 1} \gt 0</annotation></semantics></math>.</p> </li> <li> <p>If <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_65' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>c</mi> <mi>m</mi></msub><mo stretchy='false'>)</mo><mo stretchy='false'>|</mo><mo>></mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>\vert f(c_m) \vert \gt \epsilon</annotation></semantics></math>, then there exists a <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_66' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>j</mi><mo>≤</mo><mi>m</mi><mo>+</mo><mn>1</mn></mrow><annotation encoding='application/x-tex'>j \leq m + 1</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_67' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>c</mi> <mi>j</mi></msub><mo stretchy='false'>)</mo><mo><</mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>\vert f(c_j) \lt \epsilon</annotation></semantics></math>.</p> </li> </ul> <p>Thus, the above lemma is true.</p> <p>Now, by pointwise continuity at <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_68' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>c</mi></mrow><annotation encoding='application/x-tex'>c</annotation></semantics></math>, let <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_69' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>δ</mi></mrow><annotation encoding='application/x-tex'>\delta</annotation></semantics></math> be such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_70' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>x</mi><mo>−</mo><mi>y</mi><mo stretchy='false'>|</mo><mo><</mo><mi>δ</mi></mrow><annotation encoding='application/x-tex'>\vert x - y \vert \lt \delta</annotation></semantics></math> implies <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_71' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>−</mo><mi>f</mi><mo stretchy='false'>(</mo><mi>y</mi><mo stretchy='false'>)</mo><mo stretchy='false'>|</mo><mo><</mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>\vert f(x) - f(y)\vert \lt \epsilon</annotation></semantics></math>. Choose a natural number <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_72' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>m</mi></mrow><annotation encoding='application/x-tex'>m</annotation></semantics></math> such that</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_73' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>c</mi><mo>−</mo><msub><mi>c</mi> <mi>m</mi></msub><mo stretchy='false'>|</mo><mo><</mo><mfrac><mi>δ</mi><mn>2</mn></mfrac></mrow><annotation encoding='application/x-tex'>\vert c - c_m \vert \lt \frac{\delta}{2}</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_74' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mfrac><mrow><mo stretchy='false'>|</mo><mi>b</mi><mo>−</mo><mi>a</mi><mo stretchy='false'>|</mo></mrow><mrow><msup><mn>2</mn> <mrow><mi>m</mi><mo>+</mo><mn>1</mn></mrow></msup></mrow></mfrac><mo><</mo><mfrac><mi>δ</mi><mn>2</mn></mfrac></mrow><annotation encoding='application/x-tex'>\frac{\vert b - a \vert}{2^{m + 1}} \lt \frac{\delta}{2}</annotation></semantics></math></div> <p>If there exists a <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_75' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>j</mi><mo>≤</mo><mi>m</mi></mrow><annotation encoding='application/x-tex'>j \leq m</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_76' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>c</mi> <mi>j</mi></msub><mo stretchy='false'>)</mo><mo><</mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>\vert f(c_j) \lt \epsilon</annotation></semantics></math>, then the intermediate value is true. Otherwise, <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_77' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>a</mi> <mi>m</mi></msub><mo stretchy='false'>)</mo><mo><</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(a_m) \lt 0</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_78' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>b</mi> <mi>m</mi></msub><mo stretchy='false'>)</mo><mo>></mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(b_m) \gt 0</annotation></semantics></math>, and so</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_79' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>c</mi><mo>−</mo><msub><mi>c</mi> <mi>m</mi></msub><mo stretchy='false'>|</mo><mo><</mo><mo stretchy='false'>|</mo><mi>c</mi><mo>−</mo><msub><mi>c</mi> <mi>m</mi></msub><mo stretchy='false'>|</mo><mo>+</mo><mo stretchy='false'>|</mo><msub><mi>c</mi> <mi>m</mi></msub><mo>−</mo><msub><mi>a</mi> <mi>m</mi></msub><mo stretchy='false'>|</mo><mo><</mo><mi>δ</mi></mrow><annotation encoding='application/x-tex'>\vert c - c_m \vert \lt \vert c - c_m \vert + \vert c_m - a_m \vert \lt \delta</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_80' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>c</mi><mo>−</mo><msub><mi>c</mi> <mi>m</mi></msub><mo stretchy='false'>|</mo><mo><</mo><mo stretchy='false'>|</mo><mi>c</mi><mo>−</mo><msub><mi>c</mi> <mi>m</mi></msub><mo stretchy='false'>|</mo><mo>+</mo><mo stretchy='false'>|</mo><msub><mi>c</mi> <mi>m</mi></msub><mo>−</mo><msub><mi>b</mi> <mi>m</mi></msub><mo stretchy='false'>|</mo><mo><</mo><mi>δ</mi></mrow><annotation encoding='application/x-tex'>\vert c - c_m \vert \lt \vert c - c_m \vert + \vert c_m - b_m \vert \lt \delta</annotation></semantics></math></div> <p>and so that means that</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_81' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><mi>c</mi><mo stretchy='false'>)</mo><mo>−</mo><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>a</mi> <mi>m</mi></msub><mo stretchy='false'>)</mo><mo stretchy='false'>|</mo><mo><</mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>\vert f(c) - f(a_m) \vert \lt \epsilon</annotation></semantics></math></div><div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_82' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><mi>c</mi><mo stretchy='false'>)</mo><mo>−</mo><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>b</mi> <mi>m</mi></msub><mo stretchy='false'>)</mo><mo stretchy='false'>|</mo><mo><</mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>\vert f(c) - f(b_m) \vert \lt \epsilon</annotation></semantics></math></div> <p>which means that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_83' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><mi>c</mi><mo stretchy='false'>)</mo><mo stretchy='false'>|</mo><mo><</mo><mi>ϵ</mi></mrow><annotation encoding='application/x-tex'>\vert f(c) \vert \lt \epsilon</annotation></semantics></math>.</p> </div> <p>If <a class='existingWikiWord' href='/nlab/show/diff/excluded+middle'>excluded middle</a> is true, then the classical IVT follows from the above theorem:</p> <div class='proof'> <h6 id='proof_of_theorem__2'>Proof of Theorem <a class='maruku-ref' href='#classical'>1</a>⁠</h6> <p>By way of contradiction (applying the <a class='existingWikiWord' href='/nlab/show/diff/double+negation'>double negation</a> law of <a class='existingWikiWord' href='/nlab/show/diff/classical+logic'>classical logic</a>), suppose that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_84' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><mi>c</mi><mo stretchy='false'>)</mo><mo stretchy='false'>|</mo></mrow><mo>></mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>{|f(c)|} \gt 0</annotation></semantics></math> for every <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_85' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>c</mi></mrow><annotation encoding='application/x-tex'>c</annotation></semantics></math> in <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_86' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>[0,1]</annotation></semantics></math>. Then the extra hypothesis of Theorem <a class='maruku-ref' href='#hypothesis'>5</a> is certainly satisfied, so there exists some <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_87' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>c</mi></mrow><annotation encoding='application/x-tex'>c</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_88' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>c</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(c) = 0</annotation></semantics></math> after all. (Constructively, this is enough to show that the classical theorem has no counterexample.)</p> </div> <p>There is also another constructively valid version of the IVT, where the conclusion is classically the contrapositive of the classical IVT, but which is weaker constructively since the reverse contrapositive rule does not hold constructively:</p> <div class='num_theorem'> <h6 id='theorem_3'>Theorem</h6> <p>Let <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_89' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo lspace='verythinmathspace'>:</mo><mo stretchy='false'>[</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy='false'>]</mo><mo>→</mo><mi>ℝ</mi></mrow><annotation encoding='application/x-tex'>f\colon [a,b] \to \mathbb{R}</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/continuous+map'>continuous function</a> from a <a class='existingWikiWord' href='/nlab/show/diff/compact+space'>compact</a> <a class='existingWikiWord' href='/nlab/show/diff/interval'>closed interval</a> to the <a class='existingWikiWord' href='/nlab/show/diff/real+number'>real line</a>, and suppose that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_90' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo><mo><</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(x) \lt 0</annotation></semantics></math> or <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_91' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>x</mi><mo stretchy='false'>)</mo><mo>></mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(x) \gt 0</annotation></semantics></math> for all <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_92' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>∈</mo><mo stretchy='false'>[</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>x \in [a,b]</annotation></semantics></math>. Then <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_93' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math> is either everywhere positive or everywhere negative.</p> </div> <p>This appeared in <a href='#Bauer16'>Bauer 2016</a>.</p> <h3 id='constructive_ivt_with_strengthened_hypothesis'>Constructive IVT with strengthened hypothesis</h3> <div class='num_theorem' id='hypothesis'> <h6 id='theorem_4'>Theorem</h6> <p>(constructive IVT with strengthened hypothesis, assuming the interval endpoints and the zero have <a class='existingWikiWord' href='/nlab/show/diff/locator'>locators</a> and that the function is <a class='existingWikiWord' href='/nlab/show/diff/locally+nonzero+function'>locally nonzero</a>)</p> <p>For real numbers <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_94' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi></mrow><annotation encoding='application/x-tex'>a</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_95' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>b</mi></mrow><annotation encoding='application/x-tex'>b</annotation></semantics></math> with <a class='existingWikiWord' href='/nlab/show/diff/locator'>locators</a>, let <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_96' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo lspace='verythinmathspace'>:</mo><mo stretchy='false'>[</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy='false'>]</mo><mo>→</mo><mi>ℝ</mi></mrow><annotation encoding='application/x-tex'>f\colon [a,b] \to \mathbb{R}</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/pointwise+continuous+function'>pointwise continuous function</a> from the <a class='existingWikiWord' href='/nlab/show/diff/interval'>closed interval</a> <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_97' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>[a, b]</annotation></semantics></math> to the <a class='existingWikiWord' href='/nlab/show/diff/real+number'>real line</a> that is a <a class='existingWikiWord' href='/nlab/show/diff/locally+nonzero+function'>locally nonzero function</a> and that <a class='existingWikiWord' href='/nlab/show/diff/lifting+a+function'>lifts to locators</a>, and suppose that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_98' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>a</mi><mo stretchy='false'>)</mo><mo>≤</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(a) \leq 0</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_99' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>b</mi><mo stretchy='false'>)</mo><mo>≥</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(b) \geq 0</annotation></semantics></math>. Then, there exists a point <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_100' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>c</mi></mrow><annotation encoding='application/x-tex'>c</annotation></semantics></math> in <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_101' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>[a, b]</annotation></semantics></math> with a locator such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_102' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>c</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(c) = 0</annotation></semantics></math>.</p> </div> <div class='proof'> <h6 id='proof_of_theorem__3'>Proof of Theorem <a class='maruku-ref' href='#hypothesis'>5</a>⁠</h6> <p>This proof originally appeared in <a href='#Booij18'>Booij 2018</a></p> <p>…</p> </div> <div class='num_theorem' id='hypothesis'> <h6 id='theorem_5'>Theorem</h6> <p>(constructive IVT with strengthened hypothesis, assuming <a class='existingWikiWord' href='/nlab/show/diff/countable+choice'>weak countable choice</a> and that the function is <a class='existingWikiWord' href='/nlab/show/diff/locally+nonzero+function'>locally nonzero</a>)</p> <p>Assuming <a class='existingWikiWord' href='/nlab/show/diff/countable+choice'>weak countable choice</a>, for real numbers <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_103' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi></mrow><annotation encoding='application/x-tex'>a</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_104' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>b</mi></mrow><annotation encoding='application/x-tex'>b</annotation></semantics></math>, let <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_105' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo lspace='verythinmathspace'>:</mo><mo stretchy='false'>[</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy='false'>]</mo><mo>→</mo><mi>ℝ</mi></mrow><annotation encoding='application/x-tex'>f\colon [a,b] \to \mathbb{R}</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/pointwise+continuous+function'>pointwise continuous function</a> from the <a class='existingWikiWord' href='/nlab/show/diff/interval'>closed interval</a> <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_106' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>[a, b]</annotation></semantics></math> to the <a class='existingWikiWord' href='/nlab/show/diff/real+number'>real line</a> that is a <a class='existingWikiWord' href='/nlab/show/diff/locally+nonzero+function'>locally nonzero function</a>, and suppose that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_107' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>a</mi><mo stretchy='false'>)</mo><mo>≤</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(a) \leq 0</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_108' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>b</mi><mo stretchy='false'>)</mo><mo>≥</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(b) \geq 0</annotation></semantics></math>. Then, there exists a point <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_109' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>c</mi></mrow><annotation encoding='application/x-tex'>c</annotation></semantics></math> in <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_110' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>[</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>[a, b]</annotation></semantics></math> with a locator such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_111' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>c</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(c) = 0</annotation></semantics></math>.</p> </div> <div class='num_theorem' id='hypothesis'> <h6 id='theorem_6'>Theorem</h6> <p>(constructive IVT with strengthened hypothesis, assuming <a class='existingWikiWord' href='/nlab/show/diff/countable+choice'>weak countable choice</a> and that the function is <a class='existingWikiWord' href='/nlab/show/diff/uniformly+continuous+map'>uniformly continuous</a>)</p> <p>Let <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_112' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo lspace='verythinmathspace'>:</mo><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy='false'>]</mo><mo>→</mo><mi>ℝ</mi></mrow><annotation encoding='application/x-tex'>f\colon [0,1] \to \mathbb{R}</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/uniformly+continuous+map'>uniformly continuous function</a> from the <a class='existingWikiWord' href='/nlab/show/diff/interval'>unit interval</a> to the <a class='existingWikiWord' href='/nlab/show/diff/real+number'>real line</a>, and suppose that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_113' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mn>0</mn><mo stretchy='false'>)</mo><mo><</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(0) \lt 0</annotation></semantics></math> while <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_114' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mn>1</mn><mo stretchy='false'>)</mo><mo>></mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(1) \gt 0</annotation></semantics></math>. Suppose further that, for any points <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_115' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi><mo>,</mo><mi>b</mi></mrow><annotation encoding='application/x-tex'>a,b</annotation></semantics></math> in the unit interval with <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_116' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi><mo><</mo><mi>b</mi></mrow><annotation encoding='application/x-tex'>a \lt b</annotation></semantics></math>, there exists a point <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_117' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>c</mi> <mrow><mi>a</mi><mo>,</mo><mi>b</mi></mrow></msub></mrow><annotation encoding='application/x-tex'>c_{a,b}</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_118' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>a</mi><mo><</mo><msub><mi>c</mi> <mrow><mi>a</mi><mo>,</mo><mi>b</mi></mrow></msub><mo><</mo><mi>b</mi></mrow><annotation encoding='application/x-tex'>a \lt c_{a,b} \lt b</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_119' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><msub><mi>c</mi> <mrow><mi>a</mi><mo>,</mo><mi>b</mi></mrow></msub><mo stretchy='false'>)</mo><mo stretchy='false'>|</mo></mrow><mo>></mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>{|f(c_{a,b})|} \gt 0</annotation></semantics></math>. (In other words, the non-<a class='existingWikiWord' href='/nlab/show/diff/zero+locus'>zero set</a> <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_120' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>{</mo><mi>c</mi><mo>:</mo><mrow><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><mi>c</mi><mo stretchy='false'>)</mo><mo stretchy='false'>|</mo></mrow><mo>></mo><mn>0</mn><mo stretchy='false'>}</mo></mrow><annotation encoding='application/x-tex'>\{ c : {|f(c)|} \gt 0 \}</annotation></semantics></math> is <a class='existingWikiWord' href='/nlab/show/diff/dense+subspace'>dense</a>.) Then there exists a point <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_121' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>c</mi></mrow><annotation encoding='application/x-tex'>c</annotation></semantics></math> in the unit interval such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_122' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>c</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(c) = 0</annotation></semantics></math>.</p> </div> <div class='num_theorem' id='hypothesis'> <h6 id='theorem_7'>Theorem</h6> <p>(constructive IVT with strengthened hypothesis, assuming that the function is <a class='existingWikiWord' href='/nlab/show/diff/monotone+function'>strictly monotonic</a> with <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_123' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>0</mn></mrow><annotation encoding='application/x-tex'>0</annotation></semantics></math> strictly between <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_124' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mn>0</mn><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>f(0)</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_125' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mn>1</mn><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>f(1)</annotation></semantics></math>)</p> <p>Let <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_126' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo lspace='verythinmathspace'>:</mo><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy='false'>]</mo><mo>→</mo><mi>ℝ</mi></mrow><annotation encoding='application/x-tex'>f\colon [0,1] \to \mathbb{R}</annotation></semantics></math> be a <a class='existingWikiWord' href='/nlab/show/diff/monotone+function'>strictly monotonic</a> from the <a class='existingWikiWord' href='/nlab/show/diff/interval'>unit interval</a> to the <a class='existingWikiWord' href='/nlab/show/diff/real+number'>real line</a>, and suppose that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_127' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mn>0</mn><mo stretchy='false'>)</mo><mo><</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(0) \lt 0</annotation></semantics></math> while <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_128' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mn>1</mn><mo stretchy='false'>)</mo><mo>></mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(1) \gt 0</annotation></semantics></math>. Then there exists a point <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_129' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>c</mi></mrow><annotation encoding='application/x-tex'>c</annotation></semantics></math> in the unit interval such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_130' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi><mo stretchy='false'>(</mo><mi>c</mi><mo stretchy='false'>)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding='application/x-tex'>f(c) = 0</annotation></semantics></math>.</p> </div> <p>\begin{proof} We construct <a class='existingWikiWord' href='/nlab/show/diff/Dedekind+cut'>Dedekind cuts</a> <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_131' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>L</mi><mo>=</mo><mo stretchy='false'>{</mo><mi>y</mi><mo>∈</mo><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy='false'>]</mo><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><mi>y</mi><mo stretchy='false'>)</mo><mo><</mo><mn>0</mn><mo stretchy='false'>}</mo></mrow><annotation encoding='application/x-tex'>L = \{y \in [0,1] \vert f(y) \lt 0\}</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_132' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi><mo>=</mo><mo stretchy='false'>{</mo><mi>z</mi><mo>∈</mo><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy='false'>]</mo><mo stretchy='false'>|</mo><mi>f</mi><mo stretchy='false'>(</mo><mi>z</mi><mo stretchy='false'>)</mo><mo>></mo><mn>0</mn><mo stretchy='false'>}</mo></mrow><annotation encoding='application/x-tex'>U = \{z \in [0,1] \vert f(z) \gt 0\}</annotation></semantics></math> and by the Dedekind completeness of the real numbers, there is a unique <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_133' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>x</mi><mo>∈</mo><mo stretchy='false'>[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy='false'>]</mo></mrow><annotation encoding='application/x-tex'>x \in [0, 1]</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_4a0f22737d988572b3948f3f7a79a9d438166e7c_134' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>y</mi><mo><</mo><mi>x</mi><mo><</mo><mi>z</mi></mrow><annotation encoding='application/x-tex'>y \lt x \lt z</annotation></semantics></math>. \end{proof}</p> <h2 id='see_also'>See also</h2> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/extreme+value+theorem'>extreme value theorem</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/fundamental+theorem+of+algebra'>fundamental theorem of algebra</a></li> </ul> <h2 id='references'>References</h2> <ul> <li> <p><span class='newWikiWord'>Peter Schuster<a href='/nlab/new/Peter+Schuster'>?</a></span>; Unique existence, approximate solutions, and countable choice; <a href='http://dx.doi.org/10.1016/S0304-3975%2802%2900707-7'>doi</a>.</p> </li> <li> <p>Matt F.; answer to Approximate intermediate value theorem in pure constructive mathematics; MathOverflow; <a href='http://mathoverflow.net/q/255371'>web</a>.</p> </li> <li id='Frank20'> <p><span class='newWikiWord'>Matthew Frank<a href='/nlab/new/Matthew+Frank'>?</a></span>, <em>Interpolating Between Choices for the Approximate Intermediate Value Theorem</em> (<a href='https://arxiv.org/abs/1701.02227'>arxiv:1701.02227</a>), Logical Methods in Computer Science, July 14, 2020, Volume 16, Issue 3 - <a href='https://doi.org/10.23638/LMCS-16%283:5%292020'>doi:10.23638/LMCS-16(3:5)2020</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Paul+Taylor'>Paul Taylor</a>; The intermediate value theorem; A lambda calculus for real analysis, 14; <a href='http://www.paultaylor.eu/ASD/lamcra/asdivt'>web</a>.</p> </li> <li id='Booij18'> <p><a class='existingWikiWord' href='/nlab/show/diff/Auke+Booij'>Auke Booij</a>, <em>Extensional constructive real analysis via locators</em>, (<a href='https://arxiv.org/abs/1805.06781'>abs:1805.06781</a>)</p> </li> <li id='Bauer16'> <p><a class='existingWikiWord' href='/nlab/show/diff/Andrej+Bauer'>Andrej Bauer</a>, <em>Five Stages of Accepting Constructive Mathematics</em>, Bulletin of the American Mathematical Society, Volume 54, Number 3, July 2017, Pages 481–498. (<a href='http://dx.doi.org/10.1090/bull/1556'>doi:10.1090/bull/1556</a>, <a href='https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf'>pdf</a>)</p> </li> </ul> <p>On the intermediate value theorem in <a class='existingWikiWord' href='/nlab/show/diff/cohesive+homotopy+type+theory'>cohesive homotopy type theory</a>, see:</p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/Mike+Shulman'>Mike Shulman</a>, <em>Brouwer’s fixed-point theorem in real-cohesive homotopy type theory</em>, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (<a href='https://arxiv.org/abs/1509.07584'>arXiv:1509.07584</a>, <a href='https://doi.org/10.1017/S0960129517000147'>doi:10.1017/S0960129517000147</a>)</li> </ul> <p> </p> </div> <div class="revisedby"> <p> Last revised on February 19, 2024 at 12:40:51. See the <a href="/nlab/history/intermediate+value+theorem" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/intermediate+value+theorem" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/13123/#Item_6">Discuss</a><span class="backintime"><a href="/nlab/revision/diff/intermediate+value+theorem/22" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/intermediate+value+theorem" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Hide changes</a><a href="/nlab/history/intermediate+value+theorem" accesskey="S" class="navlink" id="history" rel="nofollow">History (22 revisions)</a> <a href="/nlab/show/intermediate+value+theorem/cite" style="color: black">Cite</a> <a href="/nlab/print/intermediate+value+theorem" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/intermediate+value+theorem" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>