StrictMono.le_iff_le for sets

Stream: Is there code for X?

[Emilie (Shad Amethyst)]

I can't seem to find an existing formalization around functions that preserve order in both ways that I could use on sets. I can see that StrictMono has le_iff_le, which requires a LinearOrder, while strictMono_of_le_iff_le does not. This hints to me that StrictMono is a weaker statement than $\forall (x, y) \in \alpha^2, x \le y \leftrightarrow f(x) \le f(y)$.
So I wonder if there already is some work done around that statement, and if not, whether it would be interesting to formalize it in lean, knowing that it will be equal to StrictMono when ≤ is total

[Yaël Dillies]

docs#OrderEmbedding

[Yury G. Kudryashov]

Note: you need double dollars around $\LaTeX$ formulas on Zulip.