ord.connected allows empty sets

Stream: maths

[Antoine Chambert-Loir]

For a preorder α and s : set α, the definition of set.ord_connected s in says that s is an interval in α.
I feel that the chosen terminology is not consistent with the corresponding notion in topology.connected where it is required that
connected sets are nonempty.

[Kevin Buzzard]

I guess that with the order topology they're not in general connected even if they're nonempty. Maybe connected is a bad word to use here?

[Antoine Chambert-Loir]

Yes, there is the issue about connectedness in topology, but my point was to suggest that we define this asset.ord_preconnected
(and maybe define set.ord_connected for preconnected+nonempty.

Other possible words would be interval or convex. (See the commentary below set.ord_preconnected in the file.)

[Antoine Chambert-Loir]

(There are less than 150 occurrences of the subwordord_preconnected in mathlib, in less than 10 files.)

[Floris van Doorn]

I think set.is_interval would be my preferred terminology.

[Reid Barton]

FWIW in o-minimal structures "interval" has a more specific meaning requiring it to be specified by endpoints, e.g., $\{\,a \in \mathbb{Q} \mid a^2 < 2 \,\}$ is not called an "interval"

[Antoine Chambert-Loir]

In his book on Tame topology and o-minimal geometry, van den Dries only uses “interval” for open intervals (with named endpoints) and speaks of the the other ones as “convex”. However, in that context, I've seen some authors introducing the lower/upper bounds of an interval (in the classical sense) as types (not necessarily represented in the structure).

[Floris van Doorn]

Now I'm starting to like this terminology less :)

[Reid Barton]

For me "convex" always felt like the obvious name, though I understand that it's also not literally convex in the sense of having an algebraic convex-linear-combination structure (since α might not have any algebraic structure at all)

[Kyle Miller]

Maybe set.ord_convex would make it invoke convexity without promising literal convexity?

[Antoine Chambert-Loir]

There is a notion of convexity in ordered abelian groups.
My feeling is that what we have here is really intervals, with bounds which can be defined in the structure or not, hence the interest of having them, as compared to Icc, Ico, etc. which force us to state the bounds and whether they belong or not to the interval.

[Kyle Miller]

Isn't set.ord_connected that it contains every interval, not that it is itself an interval?

class ord_connected (s : set α) : Prop :=
(out' ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s) : Icc x y ⊆ s)

For example, this set of sets doesn't seem to be an interval in any sense:

example : set.ord_connected {s : set ℕ | 1 ∈ s ∨ 2 ∈ s} :=
⟨begin
  intros x hx y hy z hz,
  simp at hz,
  cases hx,
  cases hy; exact or.inl (hz.1 hx),
  cases hy; exact or.inr (hz.1 hx),
end⟩

[Yaël Dillies]

mmmmm/

[Yaël Dillies]

Sorry, my pocket wrote that.