The slack clauses follow by contradiction, taking half the gap as the slack; the approximation clauses obtain sup S and inf S from the completeness of the reals and argue that otherwise b would be an upper, respectively lower, bound beating the supremum or infimum.
Each result cited is universally quantified over the data in its own statement.
By The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §reals, is an ordered field, so its order is a total order (Ordered Fields §ordered-field). We use Rules of Arithmetic and Order in an Ordered Field for .
Slack above. Suppose for every real , and suppose that fails. Then by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §total-negation. Adding gives (Rules of Arithmetic and Order in an Ordered Field §order-sum). Let ; by Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares §halving, . Adding gives (Rules of Arithmetic and Order in an Ordered Field §order-sum; as ). Together with , Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares §mixed gives , contradicting Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §strict-irreflexive. Hence .
Slack below. Suppose for every real . Adding gives (Rules of Arithmetic and Order in an Ordered Field §order-sum; as ). So by Slack above, with the roles of and exchanged.
Vanishing. Suppose and for every real . Then by Slack above with , so by antisymmetry (Partial and Total Orders on a Set and the Associated Strict Relation §partial).
Strict above. Let be bounded above. As is a nonempty subset of that is bounded above, it has a supremum by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §supremum, so is defined. Let with . Suppose there were no with . Then for every , fails, so by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §total-negation. Thus is an upper bound of (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §bounds). Since is the least element of the set of upper bounds (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §supremum), . From and , Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares §mixed gives , contradicting Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §strict-irreflexive.
Epsilon above. Let be bounded above, so that is defined as in Strict above, and let be real with . Adding to gives (Rules of Arithmetic and Order in an Ordered Field §order-sum), so by Rules of Arithmetic and Order in an Ordered Field §order-sum. Apply Strict above with .
Strict below. Let be bounded below. As is a nonempty subset of that is bounded below, it has an infimum by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §infimum, so is defined. Let with . Suppose there were no with . Then for every , fails, so by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §total-negation. Thus is a lower bound of (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §bounds). Since is the greatest element of the set of lower bounds (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §supremum), . From and , Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares §mixed gives , contradicting Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §strict-irreflexive.
Epsilon below. Let be bounded below, so that is defined as in Strict below, and let be real with . Then by Rules of Arithmetic and Order in an Ordered Field §order-sum. Apply Strict below with .
Loading…