Skip to main content
1 of 3

Is there a name for order-preserving functions f where "a <=b if and only if f a <= f b"?

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).