Directed indexed families and sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 familyfisr-directed.directed_on r s: Predicate stating that the setsisr-directed.is_directed α r: Prop-valued mixin stating thatαisr-directed. Follows the style of the unbundled relation classes such asis_total.scott_continuous: Predicate stating that a function between preorders preservesis_lubon directed sets.
References #
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.
theorem
directed_on_iff_directed
{α : Type u}
{r : α → α → Prop}
{s : set α} :
directed_on r s ↔ directed r coe
theorem
directed_on.directed_coe
{α : Type u}
{r : α → α → Prop}
{s : set α} :
directed_on r s → directed r coe
Alias of the forward direction of directed_on_iff_directed.
theorem
directed_on_range
{α : Type u}
{ι : Sort w}
{r : α → α → Prop}
{f : ι → α} :
directed r f ↔ directed_on r (set.range f)
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 r' : α → α → Prop}
{s : set α}
(hs : directed_on r s)
(h : ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b → r' a b) :
directed_on r' s
theorem
directed_on.mono
{α : Type u}
{r r' : α → α → Prop}
{s : set α}
(h : directed_on r s)
(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
monotone.directed_le
{α : Type u}
{β : Type v}
[semilattice_sup α]
[preorder β]
{f : α → β} :
theorem
antitone.directed_ge
{α : Type u}
{β : Type v}
[semilattice_sup α]
[preorder β]
{f : α → β}
(hf : antitone f) :
theorem
directed_on_of_sup_mem
{α : Type u}
[semilattice_sup α]
{S : set α}
(H : ∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊔ j ∈ S) :
A set stable by supremum is ≤-directed.
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 ⊥)
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.
theorem
monotone.directed_ge
{α : Type u}
{β : Type v}
[semilattice_inf α]
[preorder β]
{f : α → β}
(hf : monotone f) :
theorem
antitone.directed_le
{α : Type u}
{β : Type v}
[semilattice_inf α]
[preorder β]
{f : α → β}
(hf : antitone f) :
theorem
directed_on_of_inf_mem
{α : Type u}
[semilattice_inf α]
{S : set α}
(H : ∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊓ j ∈ S) :
A set stable by infimum is ≥-directed.
@[class]
is_directed α r states that for any elements a, b there exists an element c such that
r a c and r b c.
theorem
directed_on_univ_iff
{α : Type u}
{r : α → α → Prop} :
directed_on r set.univ ↔ is_directed α r
@[protected, instance]
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
@[protected, instance]
@[protected, instance]
theorem
directed_on.insert
{α : Type u}
{r : α → α → Prop}
(h : reflexive r)
(a : α)
{s : set α}
(hd : directed_on r s)
(ha : ∀ (b : α), b ∈ s → (∃ (c : α) (H : c ∈ s), r a c ∧ r b c)) :
directed_on r (has_insert.insert a s)
theorem
directed_on_singleton
{α : Type u}
{r : α → α → Prop}
(h : reflexive r)
(a : α) :
directed_on r {a}
theorem
directed_on_pair
{α : Type u}
{r : α → α → Prop}
(h : reflexive r)
{a b : α}
(hab : r a b) :
directed_on r {a, b}
theorem
directed_on_pair'
{α : Type u}
{r : α → α → Prop}
(h : reflexive r)
{a b : α}
(hab : r a b) :
directed_on r {b, a}
@[protected]
theorem
is_min.is_bot
{α : Type u}
[preorder α]
{a : α}
[is_directed α ge]
(h : is_min a) :
is_bot a
@[protected]
theorem
is_max.is_top
{α : Type u}
[preorder α]
{a : α}
[is_directed α has_le.le]
(h : is_max a) :
is_top a
theorem
exists_lt_of_directed_le
(β : Type v)
[partial_order β]
[is_directed β has_le.le]
[nontrivial β] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
A function between preorders is said to be Scott continuous if it preserves is_lub on directed
sets. It can be shown that a function is Scott continuous if and only if it is continuous wrt the
Scott topology.
The dual notion
∀ ⦃d : set α⦄, d.nonempty → directed_on (≥) d → ∀ ⦃a⦄, is_glb d a → is_glb (f '' d) (f a)
does not appear to play a significant role in the literature, so is omitted here.
Equations
- scott_continuous f = ∀ ⦃d : set α⦄, d.nonempty → directed_on has_le.le d → ∀ ⦃a : α⦄, is_lub d a → is_lub (f '' d) (f a)
@[protected]
theorem
scott_continuous.monotone
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(h : scott_continuous f) :
monotone f