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 #

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
    • DirectedOn r s = xs, ys, zs, 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 (x1 x2 : α) => x1 x2) 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 (x1 x2 : α) => x1 x2) f) (he : Function.Injective e) :
      Directed (fun (x1 x2 : α) => x1 x2) (Function.extend e f )
      theorem directedOn_of_inf_mem {α : Type u} [SemilatticeInf α] {S : Set α} (H : ∀ ⦃i j : α⦄, i Sj Si j S) :
      DirectedOn (fun (x1 x2 : α) => x1 x2) 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 : IsDirected α r] (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) [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 100]
        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 (x1 x2 : α) => x1 x2] (a : α) (b : α) :
        ∃ (c : α), a c b c
        theorem exists_le_le {α : Type u} [LE α] [IsDirected α fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
        ca, c b
        instance OrderDual.isDirected_ge {α : Type u} [LE α] [IsDirected α fun (x1 x2 : α) => x1 x2] :
        IsDirected αᵒᵈ fun (x1 x2 : αᵒᵈ) => x1 x2
        Equations
        • = inst
        instance OrderDual.isDirected_le {α : Type u} [LE α] [IsDirected α fun (x1 x2 : α) => x1 x2] :
        IsDirected αᵒᵈ fun (x1 x2 : αᵒᵈ) => x1 x2
        Equations
        • = inst
        theorem directed_of_isDirected_le {α : Type u} {β : Type v} [LE α] [IsDirected α fun (x1 x2 : α) => x1 x2] {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 (x1 x2 : α) => x1 x2] [Preorder β] {f : αβ} :
        Monotone fDirected (fun (x1 x2 : β) => x1 x2) f
        theorem Antitone.directed_ge {α : Type u} {β : Type v} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Preorder β] {f : αβ} (hf : Antitone f) :
        Directed (fun (x1 x2 : β) => x1 x2) f
        theorem directed_of_isDirected_ge {α : Type u} {β : Type v} [LE α] [IsDirected α fun (x1 x2 : α) => x1 x2] {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 (x1 x2 : α) => x1 x2] [Preorder β] {f : αβ} (hf : Monotone f) :
        Directed (fun (x1 x2 : β) => x1 x2) f
        theorem Antitone.directed_le {α : Type u} {β : Type v} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Preorder β] {f : αβ} (hf : Antitone f) :
        Directed (fun (x1 x2 : β) => x1 x2) f
        theorem DirectedOn.insert {α : Type u} {r : ααProp} (h : Reflexive r) (a : α) {s : Set α} (hd : DirectedOn r s) (ha : bs, cs, 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 (x1 x2 : α) => x1 x2] (h : IsMin a) :
        theorem IsMax.isTop {α : Type u} [Preorder α] {a : α} [IsDirected α fun (x1 x2 : α) => x1 x2] (h : IsMax a) :
        theorem DirectedOn.is_bot_of_is_min {α : Type u} [Preorder α] {s : Set α} (hd : DirectedOn (fun (x1 x2 : α) => x1 x2) 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 (x1 x2 : α) => x1 x2) s) {m : α} (hm : m s) (hmax : as, m aa m) (a : α) :
        a sa m
        theorem isTop_or_exists_gt {α : Type u} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (a : α) :
        IsTop a ∃ (b : α), a < b
        theorem isBot_or_exists_lt {α : Type u} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (a : α) :
        IsBot a ∃ (b : α), b < a
        theorem isBot_iff_isMin {α : Type u} [Preorder α] {a : α} [IsDirected α fun (x1 x2 : α) => x1 x2] :
        theorem isTop_iff_isMax {α : Type u} [Preorder α] {a : α} [IsDirected α fun (x1 x2 : α) => x1 x2] :
        theorem exists_lt_of_directed_ge (β : Type v) [PartialOrder β] [Nontrivial β] [IsDirected β fun (x1 x2 : β) => x1 x2] :
        ∃ (a : β) (b : β), a < b
        theorem exists_lt_of_directed_le (β : Type v) [PartialOrder β] [Nontrivial β] [IsDirected β fun (x1 x2 : β) => x1 x2] :
        ∃ (a : β) (b : β), a < b
        theorem IsMin.not_isMax {β : Type v} [PartialOrder β] [Nontrivial β] [IsDirected β fun (x1 x2 : β) => x1 x2] {b : β} (hb : IsMin b) :
        theorem IsMin.not_isMax' {β : Type v} [PartialOrder β] [Nontrivial β] [IsDirected β fun (x1 x2 : β) => x1 x2] {b : β} (hb : IsMin b) :
        theorem IsMax.not_isMin {β : Type v} [PartialOrder β] [Nontrivial β] [IsDirected β fun (x1 x2 : β) => x1 x2] {b : β} (hb : IsMax b) :
        theorem IsMax.not_isMin' {β : Type v} [PartialOrder β] [Nontrivial β] [IsDirected β fun (x1 x2 : β) => x1 x2] {b : β} (hb : IsMax b) :
        theorem constant_of_monotone_antitone {α : Type u} {β : Type v} [PartialOrder β] [Preorder α] {f : αβ} [IsDirected α fun (x1 x2 : α) => x1 x2] (hf : Monotone f) (hf' : Antitone f) (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} [PartialOrder β] [Preorder α] {f : αβ} {s : Set α} (hf : MonotoneOn f s) (hf' : AntitoneOn f s) (hs : DirectedOn (fun (x1 x2 : α) => x1 x2) 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} [SemilatticeSup α] :
        IsDirected α fun (x1 x2 : α) => x1 x2
        Equations
        • =
        @[instance 100]
        instance SemilatticeInf.to_isDirected_ge {α : Type u} [SemilatticeInf α] :
        IsDirected α fun (x1 x2 : α) => x1 x2
        Equations
        • =
        @[instance 100]
        instance OrderTop.to_isDirected_le {α : Type u} [LE α] [OrderTop α] :
        IsDirected α fun (x1 x2 : α) => x1 x2
        Equations
        • =
        @[instance 100]
        instance OrderBot.to_isDirected_ge {α : Type u} [LE α] [OrderBot α] :
        IsDirected α fun (x1 x2 : α) => x1 x2
        Equations
        • =