Directed indexed families and sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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
directed_on r s: Predicate stating that the set
is_directed α r: Prop-valued mixin stating that
r-directed. Follows the style of the
unbundled relation classes such as
scott_continuous: Predicate stating that a function between preorders preserves
is_lub on directed sets.
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.
- directed r f = ∀ (x y : ι), ∃ (z : ι), r (f x) (f z) ∧ r (f y) (f z)
A subset of α is directed if there is an element of the set
pair of elements in the set.
A monotone function on a sup-semilattice is directed.
A set stable by supremum is
An antitone function on an inf-semilattice is directed.
A set stable by infimum is
- 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.
Instances of this typeclass