directed sets

Stream: maths

[Scott Morrison]

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]

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

[Reid Barton]

Beware also directed does not include nonempty

[Reid Barton]

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