This is something only slightly stronger than monotonicity. I think that in category theory this would be a fully faithful functor, but I'm not sure if there is a standard name for this in order theory.

For context, I'm working in a theorem prover (Isabelle) and this is a property of the function which converts words to natural numbers (embedding {0 ... 2^32 - 1} into **N**).