Monotone.lt_of_lt

Stream: Is there code for X?

[Violeta Hernández]

Really simple lemma (with a really simple proof): if f is a monotone function between linear orders, then f x < f y implies x < y.

[Violeta Hernández]

Oh wait I found it through some quick loogling, it's docs#Monotone.reflect_lt

[Violeta Hernández]

Not the name I would have expected

[Antoine Chambert-Loir]

It likely comes from category theory where the concept of reflecting isomorphisms is important.

[Junyan Xu]

There is docs#PosMulReflectLT, docs#MulLeftReflectLE etc. too. Interestingly the former uses extends while the latter is an abbrev (of ContravariantClass); I'd guess this is either for performance reasons or an oversight from some refactor ...