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 \ldots 2^{32} - 1\}$ into $\mathbb{N}$).