Zulip Chat Archive

Stream: maths

Topic: directed sets


view this post on Zulip Scott Morrison (Sep 01 2018 at 10:11):

I was expecting to find a type [directed α], to go along with preorder, partial_order, etc. Instead I can only find these:

/-- A family of elements of α is directed (with respect to a relation `≼` on α)
  if there is a member of the family `≼`-above any pair in the family.  -/
def directed {ι : Sort v} (f : ι → α) := ∀x y, ∃z, f z ≼ f x ∧ f z ≼ f y
/-- A subset of α is directed if there is an element of the set `≼`-above any
  pair of elements in the set. -/
def directed_on (s : set α) := ∀ (x ∈ s) (y ∈ s), ∃z ∈ s, z ≼ x ∧ z ≼ y

view this post on Zulip Scott Morrison (Sep 01 2018 at 10:11):

Am I just mean to use directed (id α)? It seems strange that the simplest thing isn't there.

view this post on Zulip Reid Barton (Sep 01 2018 at 11:13):

Beware also directed does not include nonempty

view this post on Zulip Reid Barton (Sep 01 2018 at 11:14):

AFAIK, those are the only directed set-related things in mathlib


Last updated: May 11 2021 at 16:22 UTC