Editing Extreme value theorem (section)

===Proof using the hyperreals===
{{Math proof
|name=Proof of Extreme Value Theorem
|proof=In the setting of [[non-standard calculus]], let ''N''&thinsp; be an infinite [[hyperinteger]].  The interval [0,&nbsp;1] has a natural hyperreal extension.  Consider its partition into ''N'' subintervals of equal [[infinitesimal]] length 1/''N'', with partition points ''x<sub>i</sub>''&nbsp;= ''i''&nbsp;/''N'' as ''i'' "runs" from 0 to ''N''.  The function ''&fnof;''&thinsp; is also naturally extended to a function ''&fnof;''* defined on the hyperreals between 0 and 1.  Note that in the standard setting (when ''N''&thinsp; is finite), a point with the maximal value of ''&fnof;'' can always be chosen among the ''N''+1 points ''x<sub>i</sub>'', by induction.  Hence, by the [[transfer principle]], there is a hyperinteger ''i''<sub>0</sub> such that 0&nbsp;≤ ''i''<sub>0</sub>&nbsp;≤ ''N'' and <math>f^*(x_{i_0})\geq f^*(x_i)</math>&thinsp; for all ''i''&nbsp;=&nbsp;0,&nbsp;...,&nbsp;''N''.  Consider the real point
<math display="block">c = \mathbf{st}(x_{i_0})</math>
where '''st''' is the [[standard part function]].  An arbitrary real point ''x'' lies in a suitable sub-interval of the partition, namely <math>x\in [x_i,x_{i+1}]</math>, so that&thinsp; '''st'''(''x<sub>i</sub>'')&nbsp;= ''x''.  Applying '''st''' to the inequality <math>f^*(x_{i_0})\geq f^*(x_i)</math>, we obtain <math>\mathbf{st}(f^*(x_{i_0}))\geq \mathbf{st}(f^*(x_i))</math>.  By continuity of ''&fnof;''&thinsp; we have
:<math>\mathbf{st}(f^*(x_{i_0}))= f(\mathbf{st}(x_{i_0}))=f(c)</math>.
Hence ''&fnof;''(''c'')&nbsp;≥ ''&fnof;''(''x''), for all real ''x'', proving ''c'' to be a maximum of ''&fnof;''.<ref>{{cite book |last=Keisler |first=H. Jerome |title=Elementary Calculus : An Infinitesimal Approach |publisher=Prindle, Weber & Schmidt |location=Boston |year=1986 |isbn=0-87150-911-3 |url=https://www.math.wisc.edu/~keisler/chapter_3e.pdf#page=60 |page=164 }}</ref>
[[Q.E.D.|∎]]
}}