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 Std.Total.

TODO

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

References

• [Gierz et al, A Compendium of Continuous Lattices][GierzEtAl1980]

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

• Directed r f = ∀ (x y : ι), ∃ (z : ι), r (f x) (f z) ∧ r (f y) (f z)

def DirectedOn {α : 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

• DirectedOn r s = ∀ x ∈ s, ∀ y ∈ s, ∃ z ∈ s, r x z ∧ r y z

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 s → Directed r Subtype.val

Alias of the forward direction of directedOn_iff_directed.

theorem directedOn_range {α : Type u} {ι : Sort w} {r : α → α → Prop} {f : ι → α} : Directed r f ↔ DirectedOn r (Set.range f)

theorem Directed.directedOn_range {α : Type u} {ι : Sort w} {r : α → α → Prop} {f : ι → α} : Directed r f → DirectedOn r (Set.range f)

Alias of the forward direction of directedOn_range.

theorem directedOn_image {α : Type u} {β : Type v} {r : α → α → Prop} {s : Set β} {f : β → α} : DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s

theorem DirectedOn.mono' {α : Type u} {r r' : α → α → Prop} {s : Set α} (hs : DirectedOn r s) (h : ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b → r' a b) : DirectedOn r' s

theorem DirectedOn.mono {α : Type u} {r r' : α → α → Prop} {s : Set α} (h : DirectedOn r s) (H : ∀ ⦃a b : α⦄, r a b → r' a b) : DirectedOn r' s

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 s : α → α → Prop} {ι : Sort u_1} {f : ι → α} (H : ∀ (a b : α), r a b → s a b) (h : Directed r f) : Directed s 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 : Directed r f) : Directed rb (g ∘ f)

theorem DirectedOn.mono_comp {α : Type u} {β : Type v} {r : α → α → Prop} {rb : β → β → Prop} {g : α → β} {s : Set α} (hg : ∀ ⦃x y : α⦄, r x y → rb (g x) (g y)) (hf : DirectedOn r s) : DirectedOn rb (g '' s)

theorem directedOn_onFun_iff {α : Type u} {β : Type v} {r : α → α → Prop} {f : β → α} {s : Set β} : DirectedOn (Function.onFun r f) s ↔ DirectedOn r (f '' s)

theorem directedOn_of_sup_mem {α : Type u} [SemilatticeSup α] {S : Set α} (H : ∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊔ 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 ∈ S → j ∈ S → i ⊓ j ∈ S) : DirectedOn (fun (x1 x2 : α) => x1 ≥ x2) S

A set stable by infimum is ≥-directed.

theorem Std.Total.directed {α : Type u} {ι : Sort w} {r : α → α → Prop} [Total r] (f : ι → α) : Directed r f

theorem Std.Total.directedOn {α : Type u} {r : α → α → Prop} [Total r] (s : Set α) : DirectedOn r s

class IsDirected (α : Type u_1) (r : α → α → Prop) : 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

@[reducible, inline]

abbrev IsDirectedOrder (α : Type u_1) [LE α] : Prop

A class for an IsDirected relation ≤.

Equations

• IsDirectedOrder α = IsDirected α fun (x1 x2 : α) => x1 ≤ x2

@[reducible, inline]

abbrev IsCodirectedOrder (α : Type u_1) [LE α] : Prop

A class for an IsDirected relation ≥.

Equations

• IsCodirectedOrder α = IsDirected α fun (x1 x2 : α) => x2 ≤ x1

theorem directed_of {α : Type u} (r : α → α → Prop) [IsDirected α r] (a b : α) : ∃ (c : α), r a c ∧ r b c

theorem directed_of₃ {α : Type u} (r : α → α → Prop) [IsDirected α r] [IsTrans α r] (a b c : α) : ∃ (d : α), r a d ∧ r b d ∧ r c d

theorem directed_id {α : Type u} {r : α → α → Prop} [IsDirected α r] : Directed r id

theorem directed_id_iff {α : Type u} {r : α → α → Prop} : Directed r id ↔ IsDirected α r

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 Std.Total.to_isDirected {α : Type u} {r : α → α → Prop} [Total r] : IsDirected α r

theorem isDirected_mono {α : Type u} {r : α → α → Prop} (s : α → α → Prop) [IsDirected α r] (h : ∀ ⦃a b : α⦄, r a b → s a b) : IsDirected α s

theorem exists_ge_ge {α : Type u} [LE α] [IsDirectedOrder α] (a b : α) : ∃ (c : α), a ≤ c ∧ b ≤ c

theorem exists_le_le {α : Type u} [LE α] [IsCodirectedOrder α] (a b : α) : ∃ c ≤ a, c ≤ b

instance OrderDual.isDirected_ge {α : Type u} [LE α] [IsDirectedOrder α] : IsCodirectedOrder αᵒᵈ

instance OrderDual.isDirected_le {α : Type u} [LE α] [IsCodirectedOrder α] : IsDirectedOrder αᵒᵈ

theorem directed_of_isDirected_le {α : Type u} {β : Type v} [LE α] [IsDirectedOrder α] {f : α → β} {r : β → β → Prop} (H : ∀ ⦃i j : α⦄, i ≤ j → r (f i) (f j)) : Directed r f

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

theorem directed_of_isDirected_ge {α : Type u} {β : Type v} [LE α] [IsCodirectedOrder α] {f : α → β} {r : β → β → Prop} (H : ∀ ⦃j i : α⦄, j ≤ i → r (f i) (f j)) : Directed r f

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

theorem Monotone.directed_le {α : Type u} {β : Type v} [Preorder α] [IsDirectedOrder α] [Preorder β] {f : α → β} : Monotone f → Directed (fun (x1 x2 : β) => x1 ≤ x2) f

theorem Monotone.directed_ge {α : Type u} {β : Type v} [Preorder α] [IsCodirectedOrder α] [Preorder β] {f : α → β} : Monotone f → Directed (fun (x1 x2 : β) => x2 ≤ x1) f

theorem Antitone.directed_le {α : Type u} {β : Type v} [Preorder α] [IsCodirectedOrder α] [Preorder β] {f : α → β} (hf : Antitone f) : Directed (fun (x1 x2 : β) => x1 ≤ x2) f

theorem Antitone.directed_ge {α : Type u} {β : Type v} [Preorder α] [IsDirectedOrder α] [Preorder β] {f : α → β} (hf : Antitone f) : Directed (fun (x1 x2 : β) => x2 ≤ x1) f

theorem directedOn_iff_isDirectedOrder {α : Type u} [LE α] {s : Set α} : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s ↔ IsDirectedOrder ↑s

theorem directedOn_iff_isCodirectedOrder {α : Type u} [LE α] {s : Set α} : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s ↔ IsCodirectedOrder ↑s

theorem DirectedOn.of_isDirectedOrder {α : Type u} [LE α] {s : Set α} : IsDirectedOrder ↑s → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s

Alias of the reverse direction of directedOn_iff_isDirectedOrder.

theorem DirectedOn.isDirectedOrder {α : Type u} [LE α] {s : Set α} : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s → IsDirectedOrder ↑s

Alias of the forward direction of directedOn_iff_isDirectedOrder.

theorem DirectedOn.isCodirectedOrder {α : Type u} [LE α] {s : Set α} : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s → IsCodirectedOrder ↑s

theorem DirectedOn.of_isCodirectedOrder {α : Type u} [LE α] {s : Set α} : IsCodirectedOrder ↑s → DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s

theorem DirectedOn.insert {α : Type u} {r : α → α → Prop} (h : Reflexive r) (a : α) {s : Set α} (hd : DirectedOn r s) (ha : ∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c) : DirectedOn r (insert a s)

theorem directedOn_singleton {α : Type u} {r : α → α → Prop} (h : Reflexive r) (a : α) : DirectedOn 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 IsMax.isTop {α : Type u} [Preorder α] {a : α} [IsDirectedOrder α] (h : IsMax a) : IsTop a

theorem IsMin.isBot {α : Type u} [Preorder α] {a : α} [IsCodirectedOrder α] (h : IsMin a) : IsBot 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 : ∀ a ∈ s, m ≤ a → a ≤ m) (a : α) : a ∈ s → a ≤ m

theorem DirectedOn.is_bot_of_is_min {α : Type u} [Preorder α] {s : Set α} (hd : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s) {m : α} (hm : m ∈ s) (hmin : ∀ a ∈ s, a ≤ m → m ≤ a) (a : α) : a ∈ s → m ≤ a

theorem isTop_or_exists_gt {α : Type u} [Preorder α] [IsDirectedOrder α] (a : α) : IsTop a ∨ ∃ (b : α), a < b

theorem isBot_or_exists_lt {α : Type u} [Preorder α] [IsCodirectedOrder α] (a : α) : IsBot a ∨ ∃ (b : α), b < a

theorem isTop_iff_isMax {α : Type u} [Preorder α] {a : α} [IsDirectedOrder α] : IsTop a ↔ IsMax a

theorem isBot_iff_isMin {α : Type u} [Preorder α] {a : α} [IsCodirectedOrder α] : IsBot a ↔ IsMin a

theorem Monotone.forall_le_of_antitone {α : Type u} {β : Type v} [Preorder α] [IsDirectedOrder α] [Preorder β] {f g : α → β} (hf : Monotone f) (hg : Antitone g) (h : f ≤ g) (m n : α) : f m ≤ g n

If f is monotone, g is antitone, and f ≤ g, then for all a, b we have f a ≤ g b.

theorem exists_lt_of_directed_ge (β : Type v) [PartialOrder β] [Nontrivial β] [IsCodirectedOrder β] : ∃ (a : β) (b : β), a < b

theorem exists_lt_of_directed_le (β : Type v) [PartialOrder β] [Nontrivial β] [IsDirectedOrder β] : ∃ (a : β) (b : β), b < a

theorem IsMax.not_isMin {β : Type v} [PartialOrder β] [Nontrivial β] [IsDirectedOrder β] {b : β} (hb : IsMax b) : ¬IsMin b

theorem IsMin.not_isMax {β : Type v} [PartialOrder β] [Nontrivial β] [IsCodirectedOrder β] {b : β} (hb : IsMin b) : ¬IsMax b

theorem IsMin.not_isMax' {β : Type v} [PartialOrder β] [Nontrivial β] [IsDirectedOrder β] {b : β} (hb : IsMin b) : ¬IsMax b

theorem IsMax.not_isMin' {β : Type v} [PartialOrder β] [Nontrivial β] [IsCodirectedOrder β] {b : β} (hb : IsMax b) : ¬IsMin b

theorem constant_of_monotone_antitone {α : Type u} {β : Type v} [PartialOrder β] [Preorder α] {f : α → β} [IsDirectedOrder α] (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 ∈ s → f a = f b

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

@[instance 100]

instance SemilatticeSup.instIsDirectedOrder {α : Type u} [SemilatticeSup α] : IsDirectedOrder α

@[instance 100]

instance SemilatticeInf.instIsCodirectedOrder {α : Type u} [SemilatticeInf α] : IsCodirectedOrder α

@[instance 100]

instance OrderTop.instIsDirectedOrder {α : Type u} [LE α] [OrderTop α] : IsDirectedOrder α

@[instance 100]

instance OrderBot.instIsCodirectedOrder {α : Type u} [LE α] [OrderBot α] : IsCodirectedOrder α

theorem DirectedOn.proj {ι : Type u_1} {α : ι → Type u_2} {r : (i : ι) → α i → α i → Prop} {d : Set ((i : ι) → α i)} (hd : DirectedOn (fun (x y : (i : ι) → α i) => ∀ (i : ι), r i (x i) (y i)) d) (i : ι) : DirectedOn (r i) ((fun (a : (i : ι) → α i) => a i) '' d)

theorem DirectedOn.pi {ι : Type u_1} {α : ι → Type u_2} {r : (i : ι) → α i → α i → Prop} {d : (i : ι) → Set (α i)} (hd : ∀ (i : ι), DirectedOn (r i) (d i)) : DirectedOn (fun (x y : (i : ι) → α i) => ∀ (i : ι), r i (x i) (y i)) (Set.univ.pi d)

theorem DirectedOn.fst {α : Type u} {β : Type v} {r : α → α → Prop} {r₂ : β → β → Prop} {d : Set (α × β)} (hd : DirectedOn (fun (p q : α × β) => r p.1 q.1 ∧ r₂ p.2 q.2) d) : DirectedOn (fun (x1 x2 : α) => r x1 x2) (Prod.fst '' d)

theorem DirectedOn.snd {α : Type u} {β : Type v} {r : α → α → Prop} {r₂ : β → β → Prop} {d : Set (α × β)} (hd : DirectedOn (fun (p q : α × β) => r p.1 q.1 ∧ r₂ p.2 q.2) d) : DirectedOn (fun (x1 x2 : β) => r₂ x1 x2) (Prod.snd '' d)

theorem DirectedOn.prod {α : Type u} {β : Type v} {r : α → α → Prop} {r₂ : β → β → Prop} {d₁ : Set α} {d₂ : Set β} (h₁ : DirectedOn (fun (x1 x2 : α) => r x1 x2) d₁) (h₂ : DirectedOn (fun (x1 x2 : β) => r₂ x1 x2) d₂) : DirectedOn (fun (p q : α × β) => r p.1 q.1 ∧ r₂ p.2 q.2) (d₁ ×ˢ d₂)