(Pre)connected sets in reals are precisely the intervals

Stream: Is there code for X?

[Michael Lee]

Is there a result for this already? Or a refinement that the open (resp. closed) (pre)connected sets are precisely the open (resp. closed) intervals?

[Notification Bot]

This topic was moved here from #Is there code for X? > Connected sets in reals are precisely the intervals by Michael Lee.

[Rémy Degenne]

Real.convex_iff_isPreconnected

[Sébastien Gouëzel]

There is also docs#convex_iff_ordConnected

[Sébastien Gouëzel]

and docs#setOf_isPreconnected_eq_of_ordered
Which one is better for you depends on precisely what you want to do