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.
A subset of α is directed if there is an element of the set ≼-above any
pair of elements in the set.
theorem
directed_on_iff_directed
{α : Type u}
{r : α → α → Prop}
{s : set α} :
directed_on r s ↔ directed r coe
theorem
directed_on_image
{α : Type u}
{β : Type v}
{r : α → α → Prop}
{s : set β}
{f : β → α} :
directed_on r (f '' s) ↔ directed_on (f ⁻¹'o r) s
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
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) :
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.
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 antimonotone function on an inf-semilattice is directed.
@[class]
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]