# Documentation

Mathlib.Order.Directed

# 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 f is r-directed.
• DirectedOn r s: Predicate stating that the set s is r-directed.
• IsDirected α r: Prop-valued mixin stating that α is r-directed. Follows the style of the unbundled relation classes such as IsTotal.
def Directed {α : Type u} {ι : Sort w} (r : ααProp) (f : ια) :

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.

Equations
• Directed r f = ∀ (x y : ι), z, r (f x) (f z) r (f y) (f z)
def DirectedOn {α : Type u} (r : ααProp) (s : Set α) :

A subset of α is directed if there is an element of the set ≼-above any pair of elements in the set.

Equations
• = ∀ (x : α), x s∀ (y : α), y sz, z s r x z r y z
theorem directedOn_iff_directed {α : Type u} {r : ααProp} {s : Set α} :
Directed r Subtype.val
theorem DirectedOn.directed_val {α : Type u} {r : ααProp} {s : Set α} :
Directed r Subtype.val

Alias of the forward direction of directedOn_iff_directed.

theorem directedOn_range {α : Type u} {β : Type v} {r : ααProp} {f : βα} :
theorem directedOn_image {α : Type u} {β : Type v} {r : ααProp} {s : Set β} {f : βα} :
theorem DirectedOn.mono' {α : Type u} {r : ααProp} {r' : ααProp} {s : Set α} (hs : ) (h : a : α⦄ → a sb : α⦄ → b sr a br' a b) :
theorem DirectedOn.mono {α : Type u} {r : ααProp} {r' : ααProp} {s : Set α} (h : ) (H : {a b : α} → r a br' a b) :
theorem directed_comp {α : Type u} {β : Type v} {r : ααProp} {ι : Sort u_1} {f : ιβ} {g : βα} :
Directed r (g f) Directed (g ⁻¹'o r) f
theorem Directed.mono {α : Type u} {r : ααProp} {s : ααProp} {ι : Sort u_1} {f : ια} (H : (a b : α) → r a bs a b) (h : Directed r f) :
theorem Directed.mono_comp {α : Type u} {β : Type v} (r : ααProp) {ι : Sort u_1} {rb : ββProp} {g : αβ} {f : ια} (hg : x y : α⦄ → r x yrb (g x) (g y)) (hf : Directed r f) :
Directed rb (g f)
theorem directed_of_sup {α : Type u} {β : Type v} [inst : ] {f : αβ} {r : ββProp} (H : i j : α⦄ → i jr (f i) (f j)) :

A monotone function on a sup-semilattice is directed.

theorem Monotone.directed_le {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} :
Directed (fun x x_1 => x x_1) f
theorem Antitone.directed_ge {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) :
Directed (fun x x_1 => x x_1) f
theorem directedOn_of_sup_mem {α : Type u} [inst : ] {S : Set α} (H : ∀ ⦃i j : α⦄, i Sj Si j S) :
DirectedOn (fun x x_1 => x x_1) S

A set stable by supremum is ≤-directed.

theorem Directed.extend_bot {α : Type u} {β : Type v} {ι : Sort w} [inst : ] [inst : ] {e : ιβ} {f : ια} (hf : Directed (fun x x_1 => x x_1) f) (he : ) :
Directed (fun x x_1 => x x_1) ()
theorem directed_of_inf {α : Type u} {β : Type v} [inst : ] {r : ββProp} {f : αβ} (hf : (a₁ a₂ : α) → a₁ a₂r (f a₂) (f a₁)) :

An antitone function on an inf-semilattice is directed.

theorem Monotone.directed_ge {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) :
Directed (fun x x_1 => x x_1) f
theorem Antitone.directed_le {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) :
Directed (fun x x_1 => x x_1) f
theorem directedOn_of_inf_mem {α : Type u} [inst : ] {S : Set α} (H : ∀ ⦃i j : α⦄, i Sj Si j S) :
DirectedOn (fun x x_1 => x x_1) S

A set stable by infimum is ≥-directed.

class IsDirected (α : Type u_1) (r : ααProp) :
• For every pair of elements a and b there is a c such that r a c and r b c

directed : ∀ (a b : α), c, r a c r b c

IsDirected α r states that for any elements a, b there exists an element c such that r a c and r b c.

Instances
theorem directed_of {α : Type u} (r : ααProp) [inst : ] (a : α) (b : α) :
c, r a c r b c
theorem directed_id {α : Type u} {r : ααProp} [inst : ] :
theorem directed_id_iff {α : Type u} {r : ααProp} :
theorem directedOn_univ {α : Type u} {r : ααProp} [inst : ] :
DirectedOn r Set.univ
theorem directedOn_univ_iff {α : Type u} {r : ααProp} :
DirectedOn r Set.univ
instance IsTotal.to_isDirected {α : Type u} {r : ααProp} [inst : IsTotal α r] :
Equations
theorem isDirected_mono {α : Type u} {r : ααProp} (s : ααProp) [inst : ] (h : a b : α⦄ → r a bs a b) :
theorem exists_ge_ge {α : Type u} [inst : LE α] [inst : IsDirected α fun x x_1 => x x_1] (a : α) (b : α) :
c, a c b c
theorem exists_le_le {α : Type u} [inst : LE α] [inst : IsDirected α fun x x_1 => x x_1] (a : α) (b : α) :
c, c a c b
instance OrderDual.isDirected_ge {α : Type u} [inst : LE α] [inst : IsDirected α fun x x_1 => x x_1] :
IsDirected αᵒᵈ fun x x_1 => x x_1
Equations
instance OrderDual.isDirected_le {α : Type u} [inst : LE α] [inst : IsDirected α fun x x_1 => x x_1] :
IsDirected αᵒᵈ fun x x_1 => x x_1
Equations
theorem IsMin.isBot {α : Type u} [inst : ] {a : α} [inst : IsDirected α fun x x_1 => x x_1] (h : ) :
theorem IsMax.isTop {α : Type u} [inst : ] {a : α} [inst : IsDirected α fun x x_1 => x x_1] (h : ) :
theorem DirectedOn.is_bot_of_is_min {α : Type u} [inst : ] {s : Set α} (hd : DirectedOn (fun x x_1 => x x_1) s) {m : α} (hm : m s) (hmin : ∀ (a : α), a sa mm a) (a : α) :
a sm a
theorem DirectedOn.is_top_of_is_max {α : Type u} [inst : ] {s : Set α} (hd : DirectedOn (fun x x_1 => x x_1) s) {m : α} (hm : m s) (hmax : ∀ (a : α), a sm aa m) (a : α) :
a sa m
theorem isTop_or_exists_gt {α : Type u} [inst : ] [inst : IsDirected α fun x x_1 => x x_1] (a : α) :
b, a < b
theorem isBot_or_exists_lt {α : Type u} [inst : ] [inst : IsDirected α fun x x_1 => x x_1] (a : α) :
b, b < a
theorem isBot_iff_isMin {α : Type u} [inst : ] {a : α} [inst : IsDirected α fun x x_1 => x x_1] :
theorem isTop_iff_isMax {α : Type u} [inst : ] {a : α} [inst : IsDirected α fun x x_1 => x x_1] :
theorem exists_lt_of_directed_ge (β : Type v) [inst : ] [inst : IsDirected β fun x x_1 => x x_1] [inst : ] :
a b, a < b
theorem exists_lt_of_directed_le (β : Type v) [inst : ] [inst : IsDirected β fun x x_1 => x x_1] [inst : ] :
a b, a < b
instance SemilatticeSup.to_isDirected_le {α : Type u} [inst : ] :
IsDirected α fun x x_1 => x x_1
Equations
instance SemilatticeInf.to_isDirected_ge {α : Type u} [inst : ] :
IsDirected α fun x x_1 => x x_1
Equations
instance OrderTop.to_isDirected_le {α : Type u} [inst : LE α] [inst : ] :
IsDirected α fun x x_1 => x x_1
Equations
instance OrderBot.to_isDirected_ge {α : Type u} [inst : LE α] [inst : ] :
IsDirected α fun x x_1 => x x_1
Equations