feat(data/set/intervals): define `set.ord_connected` (#3647)
A set `s : set α`, `[preorder α]` is `ord_connected` if for
any `x y ∈ s` we have `[x, y] ⊆ s`. For real numbers this property
is equivalent to each of the properties `convex s`
and `is_preconnected s`. We define it for any `preorder`, prove some
basic properties, and migrate lemmas like `convex_I??` and
`is_preconnected_I??` to this API.
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
