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 #

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
theorem directedOn_iff_directed {α : Type u} {r : ααProp} {s : Set α} :
DirectedOn r s Directed r Subtype.val
theorem DirectedOn.directed_val {α : Type u} {r : ααProp} {s : Set α} :
DirectedOn r sDirected 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 : DirectedOn r s) (h : a : α⦄ → a sb : α⦄ → b sr a br' a b) :
theorem DirectedOn.mono {α : Type u} {r : ααProp} {r' : ααProp} {s : Set α} (h : DirectedOn r s) (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 : SemilatticeSup α] {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 : SemilatticeSup α] [inst : Preorder β] {f : αβ} :
Monotone fDirected (fun x x_1 => x x_1) f
theorem Antitone.directed_ge {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst : Preorder β] {f : αβ} (hf : Antitone f) :
Directed (fun x x_1 => x x_1) f
theorem directedOn_of_sup_mem {α : Type u} [inst : SemilatticeSup α] {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 : Preorder α] [inst : OrderBot α] {e : ιβ} {f : ια} (hf : Directed (fun x x_1 => x x_1) f) (he : Function.Injective e) :
Directed (fun x x_1 => x x_1) (Function.extend e f )
theorem directed_of_inf {α : Type u} {β : Type v} [inst : SemilatticeInf α] {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 : SemilatticeInf α] [inst : Preorder β] {f : αβ} (hf : Monotone f) :
Directed (fun x x_1 => x x_1) f
theorem Antitone.directed_le {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst : Preorder β] {f : αβ} (hf : Antitone f) :
Directed (fun x x_1 => x x_1) f
theorem directedOn_of_inf_mem {α : Type u} [inst : SemilatticeInf α] {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 : IsDirected α r] (a : α) (b : α) :
    c, r a c r b c
    theorem directed_id {α : Type u} {r : ααProp} [inst : IsDirected α r] :
    theorem directed_id_iff {α : Type u} {r : ααProp} :
    theorem directedOn_univ {α : Type u} {r : ααProp} [inst : IsDirected α r] :
    DirectedOn r Set.univ
    theorem directedOn_univ_iff {α : Type u} {r : ααProp} :
    DirectedOn r Set.univ IsDirected α r
    instance IsTotal.to_isDirected {α : Type u} {r : ααProp} [inst : IsTotal α r] :
    Equations
    theorem isDirected_mono {α : Type u} {r : ααProp} (s : ααProp) [inst : IsDirected α r] (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 : Preorder α] {a : α} [inst : IsDirected α fun x x_1 => x x_1] (h : IsMin a) :
    theorem IsMax.isTop {α : Type u} [inst : Preorder α] {a : α} [inst : IsDirected α fun x x_1 => x x_1] (h : IsMax a) :
    theorem DirectedOn.is_bot_of_is_min {α : Type u} [inst : Preorder α] {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 : Preorder α] {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 : Preorder α] [inst : IsDirected α fun x x_1 => x x_1] (a : α) :
    IsTop a b, a < b
    theorem isBot_or_exists_lt {α : Type u} [inst : Preorder α] [inst : IsDirected α fun x x_1 => x x_1] (a : α) :
    IsBot a b, b < a
    theorem isBot_iff_isMin {α : Type u} [inst : Preorder α] {a : α} [inst : IsDirected α fun x x_1 => x x_1] :
    theorem isTop_iff_isMax {α : Type u} [inst : Preorder α] {a : α} [inst : IsDirected α fun x x_1 => x x_1] :
    theorem exists_lt_of_directed_ge (β : Type v) [inst : PartialOrder β] [inst : IsDirected β fun x x_1 => x x_1] [inst : Nontrivial β] :
    a b, a < b
    theorem exists_lt_of_directed_le (β : Type v) [inst : PartialOrder β] [inst : IsDirected β fun x x_1 => x x_1] [inst : Nontrivial β] :
    a b, a < b