Commit 2021-07-21 22:22 f118c146
View on Github →feat(order): if f x ≤ f y → x ≤ y, then f is injective (#8373)
I couldn't find this specific result, not assuming linear orders, anywhere and the Zulip thread didn't get any responses, so I decided to PR the result.