Icc/Ioc/Ico/Ici/Iic intervals are not open

Stream: mathlib4

[Aaron Hill]

When using IsPreconnected.mem_intervals, I ended up proving that several different kinds of intervals are not open (in R, but this could probably be generalized). Would this make sense to PR to mathlib?

[Yury G. Kudryashov]

I think that these lemmas can go to a new file, probably with Not (IsClosed (Ioi _)) etc.

[Floris van Doorn]

Is there a reason to not just put them in file#Topology/Order/OrderClosed where docs#isOpen_Ioo is?
(note: that lemma probably has the right generality we want)

[Yury G. Kudryashov]

I expect them to be used less than isOpen_Ioo.

[Yury G. Kudryashov]

So, there is no reason to include them in a file many other files depend on.

[Yury G. Kudryashov]

But I like smaller files than many other people here, possibly because my laptop is slow.

[Violeta Hernández]

Yeah, I'm not a fan of granular files that only prove a handful of theorems. I get it when it's for imports reasons (e.g. something like SetTheory.Cardinal.Finsupp with the odd combination of Cardinal and Finsupp imports), but here it seems like the theorems would fit right besides isOpen_Ioo very well.

[Violeta Hernández]

I agree that these lemmas are less useful, but I think it's perfectly reasonable to assume the file with the theorems about Ioo, Iio, etc. being open would also contain results about the other types of intervals not being open.

[François G. Dorais]

The key idea here is gaps (i.e. a < b such that ]a,b[ is empty). Surely this has been considered elsewhere in Mathlib?

[Ruben Van de Velde]

Is that what something finite order is for?

[Yaël Dillies]

François G. Dorais said:

The key idea here is gaps (i.e. a < b such that ]a,b[ is empty). Surely this has been considered elsewhere in Mathlib?

docs#CovBy ?

[Yury G. Kudryashov]

See also docs#IsSuccLimit which is equivalent to NeBot (nhdsWithin x (Set.Iio x))

[Yury G. Kudryashov]

... and docs#IsSuccPrelimit