mathlib documentation

order.directed

def directed {α : Type u} {ι : Sort w} :
(α → α → Prop)(ι → α) → 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 directed_on {α : Type u} :
(α → α → Prop)set α → Prop

A subset of α is directed if there is an element of the set -above any pair of elements in the set.

Equations
theorem directed_on_iff_directed {α : Type u} {r : α → α → Prop} {s : set α} :

theorem directed_on_image {α : Type u} {β : Type v} {r : α → α → Prop} {s : set β} {f : β → α} :

theorem directed_on.mono {α : Type u} {r : α → α → Prop} {s : set α} (h : directed_on r s) {r' : α → α → Prop} :
(∀ {a b : α}, r a br' a b)directed_on 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 : ι → α} :
(∀ (a b : α), r a bs a b)directed r fdirected s f

theorem directed.mono_comp {α : Type u} {β : Type v} (r : α → α → Prop) {ι : Sort u_1} {rb : β → β → Prop} {g : α → β} {f : ι → α} :
(∀ ⦃x y : α⦄, r x yrb (g x) (g y))directed r fdirected rb (g f)

theorem directed_of_sup {α : Type u} {β : Type v} [semilattice_sup α] {f : α → β} {r : β → β → Prop} :
(∀ ⦃i j : α⦄, i jr (f i) (f j))directed r f

A monotone function on a sup-semilattice is directed.

theorem directed_of_inf {α : Type u} {β : Type v} [semilattice_inf α] {r : β → β → Prop} {f : α → β} :
(∀ (a₁ a₂ : α), a₁ a₂r (f a₂) (f a₁))directed r f

An antimonotone function on an inf-semilattice is directed.

@[class]
structure directed_order  :
Type uType u
  • to_preorder : 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