Definition of `strict_mono`

Stream: maths

[Chris Hughes]

Today I was surprised to find that a strict_mono function on a partial order does not necessarily satisfy a ≤ b ↔ f a ≤ f b. Currently the definition of strict_mono is a < b -> f a < f b. This makes sense on a linear order, but seems to make less sense on a partial order than a ≤ b ↔ f a ≤ f b. < really isn't used that much on partial orders anyway. Shall we change the definition to a ≤ b ↔ f a ≤ f b?

[Mario Carneiro]

Isn't that called something like "order embedding" already?

[Chris Hughes]

They're not quite the same thing on a preorder, because strict mono doesn't imply injective on a preorder.

[Chris Hughes]

In any case, I don't think we were using strict_mono for anything that wasn't an order embedding anyway currently, so I don't think we need the current definition.

[Yury G. Kudryashov]

What do textbooks say?

[Yury G. Kudryashov]

I mean, if most textbooks use the same definition (I don't know), then I vote for using a different name.