Zulip Chat Archive

Stream: maths

Topic: ord.connected allows empty sets


Antoine Chambert-Loir (Nov 14 2021 at 22:52):

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 (Nov 14 2021 at 23:57):

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 (Nov 15 2021 at 00:22):

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 (Nov 15 2021 at 00:26):

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

Floris van Doorn (Nov 15 2021 at 10:34):

I think set.is_interval would be my preferred terminology.

Reid Barton (Nov 15 2021 at 13:16):

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

Antoine Chambert-Loir (Nov 15 2021 at 14:43):

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 (Nov 15 2021 at 14:44):

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

Reid Barton (Nov 15 2021 at 14:54):

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 (Nov 15 2021 at 16:13):

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

Antoine Chambert-Loir (Nov 15 2021 at 18:45):

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 (Nov 15 2021 at 19:23):

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 (Nov 15 2021 at 20:33):

mmmmm/

Yaël Dillies (Nov 15 2021 at 20:44):

Sorry, my pocket wrote that.


Last updated: Dec 20 2023 at 11:08 UTC