mathlib documentation

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 #

source
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)
source
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
source
theorem directed_on_iff_directed {α : Type u} {r : α → α → Prop} {s : set α} :
directed_on r s ↔ directed r coe
source
theorem directed_on.directed_coe {α : Type u} {r : α → α → Prop} {s : set α} :
directed_on r s → directed r coe

Alias of directed_on_iff_directed.

source
theorem directed_on_image {α : Type u} {β : Type v} {r : α → α → Prop} {s : set β} {f : β → α} :
directed_on r (f '' s) ↔ directed_on (f ⁻¹'o r) s
source
theorem directed_on.mono {α : Type u} {r : α → α → Prop} {s : set α} (h : directed_on r s) {r' : α → α → Prop} (H : ∀ {a b : α}, r a b → r' a b) :
directed_on r' s
source
theorem directed_comp {α : Type u} {β : Type v} {r : α → α → Prop} {ι : Sort u_1} {f : ι → β} {g : β → α} :
directed r (g ∘ f) ↔ directed (g ⁻¹'o r) f
source
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
source
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)
source
theorem directed_of_sup {α : Type u} {β : Type v} [semilattice_sup α] {f : α → β} {r : β → β → Prop} (H : ∀ ⦃i j : α⦄, i ≤ j → r (f i) (f j)) :
directed r f

A monotone function on a sup-semilattice is directed.

source
theorem monotone.directed_le {α : Type u} {β : Type v} [semilattice_sup α] [preorder β] {f : α → β} :
monotone f → directed has_le.le f
source
theorem directed.extend_bot {α : Type u} {β : Type v} {ι : Sort w} [preorder α] [order_bot α] {e : ι → β} {f : ι → α} (hf : directed has_le.le f) (he : function.injective e) :
directed has_le.le (function.extend e f ⊥)
source
theorem directed_of_inf {α : Type u} {β : Type v} [semilattice_inf α] {r : β → β → Prop} {f : α → β} (hf : ∀ (a₁ a₂ : α), a₁ ≤ a₂ → r (f a₂) (f a₁)) :
directed r f

An antitone function on an inf-semilattice is directed.

source
@[class]
structure is_directed (α : Type u_1) (r : α → α → Prop) :
Prop
  • directed : ∀ (a b : α), ∃ (c : α), r a c ∧ r b c

is_directed α r states that for any elements a, b there exists an element c such that r a c and r b c.

Instances
source
theorem directed_of {α : Type u} (r : α → α → Prop) [is_directed α r] (a b : α) :
∃ (c : α), r a c ∧ r b c
source
theorem directed_id {α : Type u} {r : α → α → Prop} [is_directed α r] :
directed r id
source
theorem directed_id_iff {α : Type u} {r : α → α → Prop} :
directed r id ↔ is_directed α r
source
theorem directed_on_univ {α : Type u} {r : α → α → Prop} [is_directed α r] :
directed_on r set.univ
source
theorem directed_on_univ_iff {α : Type u} {r : α → α → Prop} :
directed_on r set.univ ↔ is_directed α r
source
@[protected, instance]
def is_total.to_is_directed {α : Type u} {r : α → α → Prop} [is_total α r] :
is_directed α r
source
theorem is_directed_mono {α : Type u} {r : α → α → Prop} (s : α → α → Prop) [is_directed α r] (h : ∀ ⦃a b : α⦄, r a b → s a b) :
is_directed α s
source
theorem exists_ge_ge {α : Type u} [has_le α] [is_directed α has_le.le] (a b : α) :
∃ (c : α), a ≤ c ∧ b ≤ c
source
theorem exists_le_le {α : Type u} [has_le α] [is_directed α (function.swap has_le.le)] (a b : α) :
∃ (c : α), c ≤ a ∧ c ≤ b
source
@[protected, instance]
def order_dual.is_directed_ge {α : Type u} [has_le α] [is_directed α has_le.le] :
is_directed (order_dual α) (function.swap has_le.le)
source
@[protected, instance]
def order_dual.is_directed_le {α : Type u} [has_le α] [is_directed α (function.swap has_le.le)] :
is_directed (order_dual α) has_le.le
source
@[protected]
theorem is_min.is_bot {α : Type u} [preorder α] {a : α} [is_directed α (function.swap has_le.le)] (h : is_min a) :
is_bot a
source
@[protected]
theorem is_max.is_top {α : Type u} [preorder α] {a : α} [is_directed α has_le.le] (h : is_max a) :
is_top a
source
theorem is_bot_iff_is_min {α : Type u} [preorder α] {a : α} [is_directed α (function.swap has_le.le)] :
is_bot a ↔ is_min a
source
theorem is_top_iff_is_max {α : Type u} [preorder α] {a : α} [is_directed α has_le.le] :
is_top a ↔ is_max a
source
@[protected, instance]
def semilattice_sup.to_is_directed_le {α : Type u} [semilattice_sup α] :
is_directed α has_le.le
source
@[protected, instance]
def semilattice_inf.to_is_directed_ge {α : Type u} [semilattice_inf α] :
is_directed α (function.swap has_le.le)
source
@[protected, instance]
def order_top.to_is_directed_le {α : Type u} [has_le α] [order_top α] :
is_directed α has_le.le
source
@[protected, instance]
def order_bot.to_is_directed_ge {α : Type u} [has_le α] [order_bot α] :
is_directed α (function.swap has_le.le)