Zulip Chat Archive

Stream: maths

Topic: is_interval


view this post on Zulip Heather Macbeth (Aug 31 2020 at 20:03):

Asked by @Floris van Doorn on #3991, @Yury G. Kudryashov or @Patrick Massot or @Anatole Dedecker will know:

Do we have a name for the following property?

def is_interval (s : set α) : Prop :=  (x y  s) z, x < z  z < y  z  s

I'm not sure about the name is_connected might be another potential name, but that sounds very topological. It is at least the property shared by all intervals.

view this post on Zulip Johan Commelin (Aug 31 2020 at 20:08):

is_preconnected doesn't require nonemptiness.

view this post on Zulip Johan Commelin (Aug 31 2020 at 20:08):

But it is of course not stated in the way you give it.

view this post on Zulip Johan Commelin (Aug 31 2020 at 20:08):

So we would need an iff lemma to connect it to the formula you want

view this post on Zulip Heather Macbeth (Aug 31 2020 at 20:11):

Ah -- and linked to from docs#is_preconnected_interval there is docs#set.ord_connected, which perhaps is better

view this post on Zulip Patrick Massot (Aug 31 2020 at 20:12):

I was really confused because I started to look for this and could only find docs#is_order_connected. I almost had the right name...

view this post on Zulip Floris van Doorn (Aug 31 2020 at 20:12):

Ah ord_connected is basically the same as what I wrote. I think that would be a good condition

view this post on Zulip Reid Barton (Aug 31 2020 at 20:13):

oh I'm too slow

view this post on Zulip Heather Macbeth (Aug 31 2020 at 20:13):

Yep, it's perfect.

view this post on Zulip Heather Macbeth (Aug 31 2020 at 20:14):

There doesn't seem to exist the theorem Floris wrote? ord_connected if and only if one of the 8 types of intervals.

view this post on Zulip Heather Macbeth (Aug 31 2020 at 20:14):

9 I guess, counting the nonexistent Iii.

view this post on Zulip Anatole Dedecker (Aug 31 2020 at 20:14):

Patrick Massot said:

I was really confused because I started to look for this and could only find docs#is_order_connected. I almost had the right name...

Same here I knew it existed but I didn't remember the name

view this post on Zulip Anatole Dedecker (Aug 31 2020 at 20:15):

Heather Macbeth said:

There doesn't seem to exist the theorem Floris wrote? ord_connected if and only if one of the 8 types of intervals.

I've seen this lemma already I think

view this post on Zulip Floris van Doorn (Aug 31 2020 at 20:18):

Heather Macbeth said:

There doesn't seem to exist the theorem Floris wrote? ord_connected if and only if one of the 8 types of intervals.

But there are proofs that the 9 intervals (the 9th is called univ :) ) are ord_connected, which is the only direction we need for your application, right?

view this post on Zulip Heather Macbeth (Aug 31 2020 at 20:19):

That's right! But classification theorems are nice, even the trivial ones :)

view this post on Zulip Floris van Doorn (Aug 31 2020 at 20:20):

Agreed. but it's not true in an arbitrary linear order, right? Maybe for a conditionally complete linear order or something?

view this post on Zulip Anatole Dedecker (Aug 31 2020 at 20:21):

https://leanprover-community.github.io/mathlib_docs/topology/algebra/ordered.html#is_preconnected.mem_intervals

view this post on Zulip Anatole Dedecker (Aug 31 2020 at 20:21):

And https://leanprover-community.github.io/mathlib_docs/topology/algebra/ordered.html#is_preconnected_iff_ord_connected

view this post on Zulip Anatole Dedecker (Aug 31 2020 at 20:22):

But I haven't looked precisely, there might be some subtle difference

view this post on Zulip Heather Macbeth (Aug 31 2020 at 20:24):

Nice! We have Yury to thank it seems, #2943

view this post on Zulip Patrick Massot (Aug 31 2020 at 20:26):

This is a topological result, not purely about order relation.

view this post on Zulip Patrick Massot (Aug 31 2020 at 20:26):

But the general claim is probably wrong.

view this post on Zulip Patrick Massot (Aug 31 2020 at 20:26):

I know I asked Yury to prove this lemma because it was on the undergrad todo list.

view this post on Zulip Heather Macbeth (Aug 31 2020 at 20:28):

Yes, I guess in (0,1)(2,3)(0,1)\cup (2,3), the set (2,3)(2,3) is not an interval

view this post on Zulip Patrick Massot (Aug 31 2020 at 20:31):

Sorry, I don't understand this message.

view this post on Zulip Heather Macbeth (Aug 31 2020 at 20:33):

Did I make a mistake in my counterexample? ]0,1[]2,3[]0,1[\cup ]2, 3[ in French notation.

view this post on Zulip Patrick Massot (Aug 31 2020 at 20:34):

I don't understand the claim, but I should go sleeping (I also haven't forget that I initiated a discussion about fancy composition and didn't find time to come back to it at a time when I can think seriously).

view this post on Zulip Heather Macbeth (Aug 31 2020 at 20:36):

I claimed that if the ordered space is the union of Ioo 0 1 and Ioo 2 3 (taken from the real numbers), and the set s is Ioo 2 3, then s satisfies ord_connected but is not an interval.

view this post on Zulip Heather Macbeth (Aug 31 2020 at 20:36):

But operating on low sleep here too :)

view this post on Zulip Kenny Lau (Aug 31 2020 at 20:37):

as in it isn't Ioo or a friend thereof?

view this post on Zulip Patrick Massot (Aug 31 2020 at 20:38):

Oh, that's sneaky.

view this post on Zulip Patrick Massot (Aug 31 2020 at 20:38):

No, it's not Ioo because 2 and 3 don't exist there.

view this post on Zulip Kenny Lau (Aug 31 2020 at 20:38):

and the point is that it ins't an Ioi either

view this post on Zulip Patrick Massot (Aug 31 2020 at 20:38):

I also had to stare at my screen for 30 seconds to see that.

view this post on Zulip Patrick Massot (Aug 31 2020 at 20:39):

Yes, it's not Ioi either, because of the other piece.

view this post on Zulip Patrick Massot (Aug 31 2020 at 20:40):

And now I'll go and meditate this in my bed.

view this post on Zulip Patrick Massot (Aug 31 2020 at 20:41):

Kids go back to school tomorrow, it's time to resume having a structured life.

view this post on Zulip Anatole Dedecker (Aug 31 2020 at 20:45):

That's a clever counterexample

view this post on Zulip Reid Barton (Aug 31 2020 at 20:59):

in fact, I think it fails in every ordered field other than R\mathbb{R}

view this post on Zulip Kevin Buzzard (Aug 31 2020 at 21:57):

How about is_convex?

view this post on Zulip Kevin Buzzard (Aug 31 2020 at 21:58):

(for a name)

view this post on Zulip Reid Barton (Aug 31 2020 at 22:12):

or if that's too overloaded, perhaps order_convex

view this post on Zulip Heather Macbeth (Aug 31 2020 at 22:49):

But there already is a name, right? docs#set.ord_connected

view this post on Zulip Reid Barton (Aug 31 2020 at 22:50):

Yes but it's too similar to is_order_connected, as Patrick and I found.

view this post on Zulip Heather Macbeth (Aug 31 2020 at 22:54):

I see. Personally I think "convex" should be reserved for objects with addition, though.

view this post on Zulip Adam Topaz (Aug 31 2020 at 22:56):

What about probability measures? They form a convex set :grinning_face_with_smiling_eyes:

view this post on Zulip Reid Barton (Aug 31 2020 at 22:56):

oh right, and the other problem with the name is something ord_connected doesn't have to be connected in the order topology

view this post on Zulip Heather Macbeth (Aug 31 2020 at 22:56):

Adam Topaz said:

What about probability measures? They form a convex set :grinning_face_with_smiling_eyes:

Well, or affine spaces.


Last updated: May 06 2021 at 19:30 UTC