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
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