## Stream: maths

### Topic: Definition of strict_mono

#### Chris Hughes (Aug 02 2020 at 11:56):

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 (Aug 02 2020 at 14:22):

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

#### Chris Hughes (Aug 02 2020 at 14:43):

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

#### Chris Hughes (Aug 02 2020 at 14:51):

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 (Aug 03 2020 at 03:26):

What do textbooks say?

#### Yury G. Kudryashov (Aug 03 2020 at 03:27):

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

Last updated: May 19 2021 at 00:40 UTC