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 #

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

      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 : DirectedOn r s) (h : ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, 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 directedOn_of_sup_mem {α : Type u} [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} [Preorder α] [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 directedOn_of_inf_mem {α : Type u} [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.

      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 directed_of {α : Type u} (r : ααProp) [IsDirected α r] (a : α) (b : α) :
        ∃ (c : α), r a c r b c
        theorem directed_id {α : Type u} {r : ααProp} [IsDirected α r] :
        theorem directed_id_iff {α : Type u} {r : ααProp} :
        theorem directedOn_univ {α : Type u} {r : ααProp} [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} [IsTotal α r] :
        Equations
        theorem isDirected_mono {α : Type u} {r : ααProp} (s : ααProp) [IsDirected α r] (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 : α) :
        ∃ c ≤ a, 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
        instance OrderDual.isDirected_le {α : Type u} [LE α] [IsDirected α fun (x x_1 : α) => x x_1] :
        IsDirected αᵒᵈ fun (x x_1 : αᵒᵈ) => x x_1
        Equations
        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} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] [Preorder β] {f : αβ} :
        Monotone fDirected (fun (x x_1 : β) => x x_1) f
        theorem Antitone.directed_ge {α : Type u} {β : Type v} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] [Preorder β] {f : αβ} (hf : Antitone f) :
        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} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] [Preorder β] {f : αβ} (hf : Monotone f) :
        Directed (fun (x x_1 : β) => x x_1) f
        theorem Antitone.directed_le {α : Type u} {β : Type v} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] [Preorder β] {f : αβ} (hf : Antitone f) :
        Directed (fun (x x_1 : β) => x x_1) f
        theorem DirectedOn.insert {α : Type u} {r : ααProp} (h : Reflexive r) (a : α) {s : Set α} (hd : DirectedOn r s) (ha : bs, ∃ c ∈ s, r a c r b c) :
        theorem directedOn_singleton {α : Type u} {r : ααProp} (h : Reflexive r) (a : α) :
        theorem directedOn_pair {α : Type u} {r : ααProp} (h : Reflexive r) {a : α} {b : α} (hab : r a b) :
        DirectedOn r {a, b}
        theorem directedOn_pair' {α : Type u} {r : ααProp} (h : Reflexive r) {a : α} {b : α} (hab : r a b) :
        DirectedOn r {b, a}
        theorem IsMin.isBot {α : Type u} [Preorder α] {a : α} [IsDirected α fun (x x_1 : α) => x x_1] (h : IsMin a) :
        theorem IsMax.isTop {α : Type u} [Preorder α] {a : α} [IsDirected α fun (x x_1 : α) => x x_1] (h : IsMax a) :
        theorem DirectedOn.is_bot_of_is_min {α : Type u} [Preorder α] {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} [Preorder α] {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} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] (a : α) :
        IsTop a ∃ (b : α), a < b
        theorem isBot_or_exists_lt {α : Type u} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] (a : α) :
        IsBot a ∃ (b : α), b < a
        theorem isBot_iff_isMin {α : Type u} [Preorder α] {a : α} [IsDirected α fun (x x_1 : α) => x x_1] :
        theorem isTop_iff_isMax {α : Type u} [Preorder α] {a : α} [IsDirected α fun (x x_1 : α) => x x_1] :
        theorem exists_lt_of_directed_ge (β : Type v) [PartialOrder β] [IsDirected β fun (x x_1 : β) => x x_1] [Nontrivial β] :
        ∃ (a : β) (b : β), a < b
        theorem exists_lt_of_directed_le (β : Type v) [PartialOrder β] [IsDirected β fun (x x_1 : β) => x x_1] [Nontrivial β] :
        ∃ (a : β) (b : β), a < b
        instance SemilatticeSup.to_isDirected_le {α : Type u} [SemilatticeSup α] :
        IsDirected α fun (x x_1 : α) => x x_1
        Equations
        instance SemilatticeInf.to_isDirected_ge {α : Type u} [SemilatticeInf α] :
        IsDirected α fun (x x_1 : α) => x x_1
        Equations
        instance OrderTop.to_isDirected_le {α : Type u} [LE α] [OrderTop α] :
        IsDirected α fun (x x_1 : α) => x x_1
        Equations
        instance OrderBot.to_isDirected_ge {α : Type u} [LE α] [OrderBot α] :
        IsDirected α fun (x x_1 : α) => x x_1
        Equations