An element of [0,∞] that is at most some real number is itself a real number.
In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let , , and the order be as in The Extended Real Line, Its Order, and [0,∞] (i), The Extended Real Line, Its Order, and [0,∞] (ii) and The Extended Real Line, Its Order, and [0,∞] (iii).
If , and , then .
Loading…
No relations recorded yet.