Editing Nonstandard calculus (section)

==Extreme value theorem==

To show that a real continuous function ''f'' on [0,1] has a maximum, let ''N'' be an infinite [[hyperinteger]].  The interval [0,&nbsp;1] has a natural hyperreal extension.  The function ''f'' is also naturally extended to hyperreals between 0 and 1.  Consider the partition of the hyperreal interval [0,1] 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''.  In the standard setting (when ''N'' is finite), a point with the maximal value of ''f'' 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> for all ''i''&nbsp;=&nbsp;0,&nbsp;…,&nbsp;''N'' (an alternative explanation is that every [[hyperfinite set]] admits a maximum).  Consider the real point

:<math>c= {\rm 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 '''st'''(''x''<sub>''i''</sub>)&nbsp;= ''x''.  Applying '''st''' to the inequality <math>f(x_{i_0})\geq f(x_i)</math>, <math>{\rm st}(f(x_{i_0}))\geq {\rm st}(f(x_i))</math>.  By continuity of ''f'',
:<math>{\rm st}(f(x_{i_0}))= f({\rm st} (x_{i_0}))=f(c)</math>.
Hence ''f''(''c'')&nbsp;≥ ''f''(''x''), for all ''x'', proving ''c'' to be a maximum of the real function ''f''.<ref>{{harvtxt |Keisler|1986|p=164}}</ref>