# 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.
• ScottContinuous: Predicate stating that a function between preorders preserves IsLUB on directed sets.

## TODO #

Define connected orders (the transitive symmetric closure of ≤ is everything) and show that (co)directed orders are connected.

## References #

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)
Instances For
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
• = xs, ys, zs, r x z r y z
Instances For
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} {ι : Sort w} {r : ααProp} {f : ια} :
theorem Directed.directedOn_range {α : Type u} {ι : Sort w} {r : ααProp} {f : ια} :
Directed r fDirectedOn r ()

Alias of the forward direction of directedOn_range.

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 s∀ ⦃b : α⦄, 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 directedOn_of_sup_mem {α : Type u} [] {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} [] [] {e : ιβ} {f : ια} (hf : Directed (fun (x x_1 : α) => x x_1) f) (he : ) :
Directed (fun (x x_1 : α) => x x_1) ()
theorem directedOn_of_inf_mem {α : Type u} [] {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.

theorem IsTotal.directed {α : Type u} {ι : Sort w} {r : ααProp} [IsTotal α r] (f : ια) :
class IsDirected (α : Type u_1) (r : ααProp) :

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

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

For every pair of elements a and b there is a c such that r a c and r b c

Instances
theorem IsDirected.directed {α : Type u_1} {r : ααProp} [self : ] (a : α) (b : α) :
∃ (c : α), r a c r b c

For every pair of elements a and b there is a c such that r a c and r b c

theorem directed_of {α : Type u} (r : ααProp) [] (a : α) (b : α) :
∃ (c : α), r a c r b c
theorem directed_id {α : Type u} {r : ααProp} [] :
theorem directed_id_iff {α : Type u} {r : ααProp} :
theorem directedOn_univ {α : Type u} {r : ααProp} [] :
DirectedOn r Set.univ
theorem directedOn_univ_iff {α : Type u} {r : ααProp} :
DirectedOn r Set.univ
@[instance 100]
instance IsTotal.to_isDirected {α : Type u} {r : ααProp} [IsTotal α r] :
Equations
• =
theorem isDirected_mono {α : Type u} {r : ααProp} (s : ααProp) [] (h : ∀ ⦃a b : α⦄, r a bs a b) :
theorem exists_ge_ge {α : Type u} [LE α] [IsDirected α fun (x x_1 : α) => x x_1] (a : α) (b : α) :
∃ (c : α), a c b c
theorem exists_le_le {α : Type u} [LE α] [IsDirected α fun (x x_1 : α) => x x_1] (a : α) (b : α) :
ca, c b
instance OrderDual.isDirected_ge {α : Type u} [LE α] [IsDirected α fun (x x_1 : α) => x x_1] :
IsDirected αᵒᵈ fun (x x_1 : αᵒᵈ) => x x_1
Equations
• = inst
instance OrderDual.isDirected_le {α : Type u} [LE α] [IsDirected α fun (x x_1 : α) => x x_1] :
IsDirected αᵒᵈ fun (x x_1 : αᵒᵈ) => x x_1
Equations
• = inst
theorem directed_of_isDirected_le {α : Type u} {β : Type v} [LE α] [IsDirected α fun (x x_1 : α) => x x_1] {f : αβ} {r : ββProp} (H : ∀ ⦃i j : α⦄, i jr (f i) (f j)) :

A monotone function on an upwards-directed type is directed.

theorem Monotone.directed_le {α : Type u} {β : Type v} [] [IsDirected α fun (x x_1 : α) => x x_1] [] {f : αβ} :
Directed (fun (x x_1 : β) => x x_1) f
theorem Antitone.directed_ge {α : Type u} {β : Type v} [] [IsDirected α fun (x x_1 : α) => x x_1] [] {f : αβ} (hf : ) :
Directed (fun (x x_1 : β) => x x_1) f
theorem directed_of_isDirected_ge {α : Type u} {β : Type v} [LE α] [IsDirected α fun (x x_1 : α) => x x_1] {r : ββProp} {f : αβ} (hf : ∀ (a₁ a₂ : α), a₁ a₂r (f a₂) (f a₁)) :

An antitone function on a downwards-directed type is directed.

theorem Monotone.directed_ge {α : Type u} {β : Type v} [] [IsDirected α fun (x x_1 : α) => x x_1] [] {f : αβ} (hf : ) :
Directed (fun (x x_1 : β) => x x_1) f
theorem Antitone.directed_le {α : Type u} {β : Type v} [] [IsDirected α fun (x x_1 : α) => x x_1] [] {f : αβ} (hf : ) :
Directed (fun (x x_1 : β) => x x_1) f
theorem DirectedOn.insert {α : Type u} {r : ααProp} (h : ) (a : α) {s : Set α} (hd : ) (ha : bs, cs, r a c r b c) :
theorem directedOn_singleton {α : Type u} {r : ααProp} (h : ) (a : α) :
theorem directedOn_pair {α : Type u} {r : ααProp} (h : ) {a : α} {b : α} (hab : r a b) :
DirectedOn r {a, b}
theorem directedOn_pair' {α : Type u} {r : ααProp} (h : ) {a : α} {b : α} (hab : r a b) :
DirectedOn r {b, a}
theorem IsMin.isBot {α : Type u} [] {a : α} [IsDirected α fun (x x_1 : α) => x x_1] (h : ) :
theorem IsMax.isTop {α : Type u} [] {a : α} [IsDirected α fun (x x_1 : α) => x x_1] (h : ) :
theorem DirectedOn.is_bot_of_is_min {α : Type u} [] {s : Set α} (hd : DirectedOn (fun (x x_1 : α) => x x_1) s) {m : α} (hm : m s) (hmin : as, a mm a) (a : α) :
a sm a
theorem DirectedOn.is_top_of_is_max {α : Type u} [] {s : Set α} (hd : DirectedOn (fun (x x_1 : α) => x x_1) s) {m : α} (hm : m s) (hmax : as, m aa m) (a : α) :
a sa m
theorem isTop_or_exists_gt {α : Type u} [] [IsDirected α fun (x x_1 : α) => x x_1] (a : α) :
∃ (b : α), a < b
theorem isBot_or_exists_lt {α : Type u} [] [IsDirected α fun (x x_1 : α) => x x_1] (a : α) :
∃ (b : α), b < a
theorem isBot_iff_isMin {α : Type u} [] {a : α} [IsDirected α fun (x x_1 : α) => x x_1] :
theorem isTop_iff_isMax {α : Type u} [] {a : α} [IsDirected α fun (x x_1 : α) => x x_1] :
theorem exists_lt_of_directed_ge (β : Type v) [] [IsDirected β fun (x x_1 : β) => x x_1] [] :
∃ (a : β) (b : β), a < b
theorem exists_lt_of_directed_le (β : Type v) [] [IsDirected β fun (x x_1 : β) => x x_1] [] :
∃ (a : β) (b : β), a < b
theorem constant_of_monotone_antitone {α : Type u} (β : Type v) [] [] {f : αβ} [IsDirected α fun (x x_1 : α) => x x_1] (hf : ) (hf' : ) (a : α) (b : α) :
f a = f b

If f is monotone and antitone on a directed order, then f is constant.

theorem constant_of_monotoneOn_antitoneOn {α : Type u} (β : Type v) [] [] {f : αβ} {s : Set α} (hf : ) (hf' : ) (hs : DirectedOn (fun (x x_1 : α) => x x_1) s) ⦃a : α :
a s∀ ⦃b : α⦄, b sf a = f b

If f is monotone and antitone on a directed set s, then f is constant on s.

@[instance 100]
instance SemilatticeSup.to_isDirected_le {α : Type u} [] :
IsDirected α fun (x x_1 : α) => x x_1
Equations
• =
@[instance 100]
instance SemilatticeInf.to_isDirected_ge {α : Type u} [] :
IsDirected α fun (x x_1 : α) => x x_1
Equations
• =
@[instance 100]
instance OrderTop.to_isDirected_le {α : Type u} [LE α] [] :
IsDirected α fun (x x_1 : α) => x x_1
Equations
• =
@[instance 100]
instance OrderBot.to_isDirected_ge {α : Type u} [LE α] [] :
IsDirected α fun (x x_1 : α) => x x_1
Equations
• =