Zulip Chat Archive

Stream: maths

Topic: is_interval

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.

Johan Commelin (Aug 31 2020 at 20:08):

is_preconnected doesn't require nonemptiness.

Johan Commelin (Aug 31 2020 at 20:08):

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

Johan Commelin (Aug 31 2020 at 20:08):

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

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

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

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

Reid Barton (Aug 31 2020 at 20:13):

oh I'm too slow

Heather Macbeth (Aug 31 2020 at 20:13):

Yep, it's perfect.

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.

Heather Macbeth (Aug 31 2020 at 20:14):

9 I guess, counting the nonexistent Iii.

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

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

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?

Heather Macbeth (Aug 31 2020 at 20:19):

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

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?

Anatole Dedecker (Aug 31 2020 at 20:21):

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

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

Anatole Dedecker (Aug 31 2020 at 20:22):

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

Heather Macbeth (Aug 31 2020 at 20:24):

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

Patrick Massot (Aug 31 2020 at 20:26):

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

Patrick Massot (Aug 31 2020 at 20:26):

But the general claim is probably wrong.

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.

Heather Macbeth (Aug 31 2020 at 20:28):

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

Patrick Massot (Aug 31 2020 at 20:31):

Sorry, I don't understand this message.

Heather Macbeth (Aug 31 2020 at 20:33):

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

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

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.