Directed indexed families and sets #
This file defines directed indexed families and directed sets. An indexed family/set is directed iff each pair of elements has a shared upper bound.
Main declarations #
- directed : ∀ (a b : α), ∃ (c : α), r a c ∧ r b c
is_directed α r states that for any elements
b there exists an element
c such that
r a c and
r b c.