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} :
(∀ {a b : α}, r a b → r' a b) → directed_on r' s
theorem
directed.mono_comp
{α : Type u}
{β : Type v}
(r : α → α → Prop)
{ι : Sort u_1}
{rb : β → β → Prop}
{g : α → β}
{f : ι → α} :
theorem
directed_of_sup
{α : Type u}
{β : Type v}
[semilattice_sup α]
{f : α → β}
{r : β → β → Prop} :
A monotone function on a sup-semilattice is directed.
theorem
directed_of_inf
{α : Type u}
{β : Type v}
[semilattice_inf α]
{r : β → β → Prop}
{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]