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 #

• 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.
• directed_order α: Typeclass extending preorder for stating that α is ≤-directed.
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
• s = ∀ (x : α), x s∀ (y : α), y s(∃ (z : α) (H : z s), r x z r y z)
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 directed_on_iff_directed.

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 : α → α → Prop} {s : set α} (h : s) {r' : α → α → Prop} (H : ∀ {a b : α}, r a br' 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 bs 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 yrb (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 jr (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 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.

@[class]
structure directed_order (α : Type u) :
Type u
• to_preorder :
• directed : ∀ (i j : α), ∃ (k : α), i k j k

A preorder is a directed_order if for any two elements i, j there is an element k such that i ≤ k and j ≤ k.

Instances
@[instance]
def linear_order.to_directed_order (α : Type u_1) [linear_order α] :
Equations