Skip to content
Axiomatic Wiki
Lemma·L49

The embedding preserves and reflects order

A natural number is at most another exactly when their integer images compare the same way.

For : with from D057 and from D062.
In words
One natural number is at most another exactly when their images under the embedding compare the same way as integers.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).

Proof

  1. 1
    means , which by D062 is . By D027 this is exactly .
∎

Remarks

Together with L42 and L46, this completes the picture: is an injective, order-preserving ring homomorphism, so sits inside as a faithful copy of the naturals, ordered the same way.
Wikipedia ↗Int.ofNat_le ↗

Used by

T31T32T34T35
Propose an edit1 published revision