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 r f: Predicate stating that the indexed family
DirectedOn r s: Predicate stating that the set
IsDirected α r: Prop-valued mixin stating that
r-directed. Follows the style of the unbundled relation classes such as
ScottContinuous: Predicate stating that a function between preorders preserves
IsLUBon directed sets.
- [Gierz et al, A Compendium of Continuous Lattices][GierzEtAl1980]