## Stream: maths

### Topic: directed sets

#### 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


#### 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.

#### Reid Barton (Sep 01 2018 at 11:13):

Beware also directed does not include nonempty

#### 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