Zulip Chat Archive

Stream: maths

Topic: betweenness


view this post on Zulip Chris Hughes (May 29 2019 at 14:02):

Do we have a concept of betweenness in mathlib for orders? i.e a is between x and y iff min x y ≤ a ∧ a ≤ max x y

view this post on Zulip Chris Hughes (May 29 2019 at 14:03):

I want it for partial orders though.

view this post on Zulip Mario Carneiro (May 29 2019 at 14:18):

It's not clear what the analogue is... how did this come up?

view this post on Zulip Mario Carneiro (May 29 2019 at 14:18):

Usually you know which of x or y is bigger and then x <= a <= y does mostly what you want

view this post on Zulip Mario Carneiro (May 29 2019 at 14:20):

Perhaps x ⊓ y ≤ a ≤ x ⊔ y?


Last updated: May 09 2021 at 10:11 UTC