Overspill lemma
= Overspill lemma
If a definable property in a <nonstandard model of Peano arithmetic> holds of every standard natural number, then it holds of some nonstandard element. Equivalently, a definable set containing the entire <standard cut of a nonstandard model of arithmetic> must overspill beyond it.
This is the arithmetic case of <overspill>, which also applies to internal subsets of nonstandard extensions in analysis.