order.directed

# 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 f is r-directed.
• directed_on r s: Predicate stating that the set s is r-directed.
• is_directed α r: Prop-valued mixin stating that α is r-directed. Follows the style of the unbundled relation classes such as is_total.
• scott_continuous: Predicate stating that a function between preorders preserves is_lub on directed sets.

## References #

def directed {α : Type u} {ι : Sort w} (r : α α Prop) (f : ι α) :
Prop

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
• f = (x y : ι), (z : ι), r (f x) (f z) r (f y) (f z)
def directed_on {α : Type u} (r : α α Prop) (s : set α) :
Prop

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

Equations
theorem directed_on_iff_directed {α : Type u} {r : α α Prop} {s : set α} :
s
theorem directed_on.directed_coe {α : Type u} {r : α α Prop} {s : set α} :
s

Alias of the forward direction of directed_on_iff_directed.

theorem directed_on_range {α : Type u} {ι : Sort w} {r : α α Prop} {f : ι α} :
f (set.range f)
theorem directed_on_image {α : Type u} {β : Type v} {r : α α Prop} {s : set β} {f : β α} :
(f '' s) directed_on (f ⁻¹'o r) s
theorem directed_on.mono' {α : Type u} {r r' : α α Prop} {s : set α} (hs : s) (h : ⦃a : α⦄, a s ⦃b : α⦄, b s r a b r' a b) :
s
theorem directed_on.mono {α : Type u} {r r' : α α Prop} {s : set α} (h : s) (H : {a b : α}, r a b r' a b) :
s
theorem directed_comp {α : Type u} {β : Type v} {r : α α Prop} {ι : Sort u_1} {f : ι β} {g : β α} :
(g f) directed (g ⁻¹'o r) f
theorem directed.mono {α : Type u} {r s : α α Prop} {ι : Sort u_1} {f : ι α} (H : (a b : α), r a b s a b) (h : f) :
f
theorem directed.mono_comp {α : Type u} {β : Type v} (r : α α Prop) {ι : Sort u_1} {rb : β β Prop} {g : α β} {f : ι α} (hg : ⦃x y : α⦄, r x y rb (g x) (g y)) (hf : f) :
directed rb (g f)
theorem directed_of_sup {α : Type u} {β : Type v} {f : α β} {r : β β Prop} (H : ⦃i j : α⦄, i j r (f i) (f j)) :
f

A monotone function on a sup-semilattice is directed.

theorem monotone.directed_le {α : Type u} {β : Type v} [preorder β] {f : α β} :
theorem antitone.directed_ge {α : Type u} {β : Type v} [preorder β] {f : α β} (hf : antitone f) :
theorem directed_on_of_sup_mem {α : Type u} {S : set α} (H : ⦃i j : α⦄, i S j S i j S) :

A set stable by supremum is ≤-directed.

theorem directed.extend_bot {α : Type u} {β : Type v} {ι : Sort w} [preorder α] [order_bot α] {e : ι β} {f : ι α} (hf : f) (he : function.injective e) :
theorem directed_of_inf {α : Type u} {β : Type v} {r : β β Prop} {f : α β} (hf : (a₁ a₂ : α), a₁ a₂ r (f a₂) (f a₁)) :
f

An antitone function on an inf-semilattice is directed.

theorem monotone.directed_ge {α : Type u} {β : Type v} [preorder β] {f : α β} (hf : monotone f) :
theorem antitone.directed_le {α : Type u} {β : Type v} [preorder β] {f : α β} (hf : antitone f) :
theorem directed_on_of_inf_mem {α : Type u} {S : set α} (H : ⦃i j : α⦄, i S j S i j S) :

A set stable by infimum is ≥-directed.

theorem is_total.directed {α : Type u} {ι : Sort w} {r : α α Prop} [ r] (f : ι α) :
f
@[class]
structure is_directed (α : Type u_1) (r : α α Prop) :
Prop
• directed : (a b : α), (c : α), r a c r b c

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

Instances of this typeclass
theorem directed_of {α : Type u} (r : α α Prop) [ r] (a b : α) :
(c : α), r a c r b c
theorem directed_id {α : Type u} {r : α α Prop} [ r] :
theorem directed_id_iff {α : Type u} {r : α α Prop} :
r
theorem directed_on_univ {α : Type u} {r : α α Prop} [ r] :
theorem directed_on_univ_iff {α : Type u} {r : α α Prop} :
@[protected, instance]
def is_total.to_is_directed {α : Type u} {r : α α Prop} [ r] :
r
theorem is_directed_mono {α : Type u} {r : α α Prop} (s : α α Prop) [ r] (h : ⦃a b : α⦄, r a b s a b) :
s
theorem exists_ge_ge {α : Type u} [has_le α] (a b : α) :
(c : α), a c b c
theorem exists_le_le {α : Type u} [has_le α] [ ge] (a b : α) :
(c : α), c a c b
@[protected, instance]
def order_dual.is_directed_ge {α : Type u} [has_le α]  :
@[protected, instance]
def order_dual.is_directed_le {α : Type u} [has_le α] [ ge] :
theorem directed_on.insert {α : Type u} {r : α α Prop} (h : reflexive r) (a : α) {s : set α} (hd : s) (ha : (b : α), b s ( (c : α) (H : c s), r a c r b c)) :
s)
theorem directed_on_singleton {α : Type u} {r : α α Prop} (h : reflexive r) (a : α) :
{a}
theorem directed_on_pair {α : Type u} {r : α α Prop} (h : reflexive r) {a b : α} (hab : r a b) :
{a, b}
theorem directed_on_pair' {α : Type u} {r : α α Prop} (h : reflexive r) {a b : α} (hab : r a b) :
{b, a}
@[protected]
theorem is_min.is_bot {α : Type u} [preorder α] {a : α} [ ge] (h : is_min a) :
@[protected]
theorem is_max.is_top {α : Type u} [preorder α] {a : α} (h : is_max a) :
theorem directed_on.is_bot_of_is_min {α : Type u} [preorder α] {s : set α} (hd : s) {m : α} (hm : m s) (hmin : (a : α), a s a m m a) (a : α) (H : a s) :
m a
theorem directed_on.is_top_of_is_max {α : Type u} [preorder α] {s : set α} (hd : s) {m : α} (hm : m s) (hmax : (a : α), a s m a a m) (a : α) (H : a s) :
a m
theorem is_top_or_exists_gt {α : Type u} [preorder α] (a : α) :
(b : α), a < b
theorem is_bot_or_exists_lt {α : Type u} [preorder α] [ ge] (a : α) :
(b : α), b < a
theorem is_bot_iff_is_min {α : Type u} [preorder α] {a : α} [ ge] :
theorem is_top_iff_is_max {α : Type u} [preorder α] {a : α}  :
theorem exists_lt_of_directed_ge (β : Type v) [ ge] [nontrivial β] :
(a b : β), a < b
theorem exists_lt_of_directed_le (β : Type v) [nontrivial β] :
(a b : β), a < b
@[protected, instance]
@[protected, instance]
@[protected, instance]
def order_top.to_is_directed_le {α : Type u} [has_le α] [order_top α] :
@[protected, instance]
def order_bot.to_is_directed_ge {α : Type u} [has_le α] [order_bot α] :