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 #
Directed r f
: Predicate stating that the indexed familyf
isr
-directed.DirectedOn r s
: Predicate stating that the sets
isr
-directed.IsDirected α r
: Prop-valued mixin stating thatα
isr
-directed. Follows the style of the unbundled relation classes such asIsTotal
.ScottContinuous
: Predicate stating that a function between preorders preservesIsLUB
on directed sets.
References #
- [Gierz et al, A Compendium of Continuous Lattices][GierzEtAl1980]
theorem
directedOn_iff_directed
{α : Type u}
{r : α → α → Prop}
{s : Set α}
:
DirectedOn r s ↔ Directed r Subtype.val
theorem
DirectedOn.directed_val
{α : Type u}
{r : α → α → Prop}
{s : Set α}
:
DirectedOn r s → Directed r Subtype.val
Alias of the forward direction of directedOn_iff_directed
.
theorem
directedOn_range
{α : Type u}
{ι : Sort w}
{r : α → α → Prop}
{f : ι → α}
:
Directed r f ↔ DirectedOn r (Set.range f)
theorem
Directed.directedOn_range
{α : Type u}
{ι : Sort w}
{r : α → α → Prop}
{f : ι → α}
:
Directed r f → DirectedOn r (Set.range f)
Alias of the forward direction of directedOn_range
.
theorem
directedOn_image
{α : Type u}
{β : Type v}
{r : α → α → Prop}
{s : Set β}
{f : β → α}
:
DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s
theorem
DirectedOn.mono'
{α : Type u}
{r : α → α → Prop}
{r' : α → α → Prop}
{s : Set α}
(hs : DirectedOn r s)
(h : ⦃a : α⦄ → a ∈ s → ⦃b : α⦄ → b ∈ s → r a b → r' a b)
:
DirectedOn r' s
theorem
DirectedOn.mono
{α : Type u}
{r : α → α → Prop}
{r' : α → α → Prop}
{s : Set α}
(h : DirectedOn r s)
(H : {a b : α} → r a b → r' a b)
:
DirectedOn r' s
theorem
directed_of_sup
{α : Type u}
{β : Type v}
[SemilatticeSup α]
{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}
[SemilatticeSup α]
[Preorder β]
{f : α → β}
:
theorem
Antitone.directed_ge
{α : Type u}
{β : Type v}
[SemilatticeSup α]
[Preorder β]
{f : α → β}
(hf : Antitone f)
:
theorem
directedOn_of_sup_mem
{α : Type u}
[SemilatticeSup α]
{S : Set α}
(H : ∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊔ j ∈ S)
:
DirectedOn (fun x x_1 => x ≤ x_1) S
A set stable by supremum is ≤
-directed.
theorem
Directed.extend_bot
{α : Type u}
{β : Type v}
{ι : Sort w}
[Preorder α]
[OrderBot α]
{e : ι → β}
{f : ι → α}
(hf : Directed (fun x x_1 => x ≤ x_1) f)
(he : Function.Injective e)
:
Directed (fun x x_1 => x ≤ x_1) (Function.extend e f ⊥)
theorem
directed_of_inf
{α : Type u}
{β : Type v}
[SemilatticeInf α]
{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}
[SemilatticeInf α]
[Preorder β]
{f : α → β}
(hf : Monotone f)
:
theorem
Antitone.directed_le
{α : Type u}
{β : Type v}
[SemilatticeInf α]
[Preorder β]
{f : α → β}
(hf : Antitone f)
:
theorem
directedOn_of_inf_mem
{α : Type u}
[SemilatticeInf α]
{S : Set α}
(H : ∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊓ j ∈ S)
:
DirectedOn (fun x x_1 => x ≥ x_1) S
A set stable by infimum is ≥
-directed.
- directed : ∀ (a b : α), ∃ c, r a c ∧ r b c
For every pair of elements
a
andb
there is ac
such thatr a c
andr b c
IsDirected α r
states that for any elements a
, b
there exists an element c
such that
r a c
and r b c
.
Instances
theorem
directed_of
{α : Type u}
(r : α → α → Prop)
[IsDirected α r]
(a : α)
(b : α)
:
∃ c, r a c ∧ r b c
theorem
isDirected_mono
{α : Type u}
{r : α → α → Prop}
(s : α → α → Prop)
[IsDirected α r]
(h : ⦃a b : α⦄ → r a b → s a b)
:
IsDirected α s
instance
OrderDual.isDirected_ge
{α : Type u}
[LE α]
[IsDirected α fun x x_1 => x ≤ x_1]
:
IsDirected αᵒᵈ fun x x_1 => x ≥ x_1
instance
OrderDual.isDirected_le
{α : Type u}
[LE α]
[IsDirected α fun x x_1 => x ≥ x_1]
:
IsDirected αᵒᵈ fun x x_1 => x ≤ x_1
theorem
DirectedOn.insert
{α : Type u}
{r : α → α → Prop}
(h : Reflexive r)
(a : α)
{s : Set α}
(hd : DirectedOn r s)
(ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r a c ∧ r b c)
:
DirectedOn r (insert a s)
theorem
directedOn_singleton
{α : Type u}
{r : α → α → Prop}
(h : Reflexive r)
(a : α)
:
DirectedOn r {a}
theorem
directedOn_pair
{α : Type u}
{r : α → α → Prop}
(h : Reflexive r)
{a : α}
{b : α}
(hab : r a b)
:
DirectedOn r {a, b}
theorem
directedOn_pair'
{α : Type u}
{r : α → α → Prop}
(h : Reflexive r)
{a : α}
{b : α}
(hab : r a b)
:
DirectedOn r {b, a}
theorem
IsMin.isBot
{α : Type u}
[Preorder α]
{a : α}
[IsDirected α fun x x_1 => x ≥ x_1]
(h : IsMin a)
:
IsBot a
theorem
IsMax.isTop
{α : Type u}
[Preorder α]
{a : α}
[IsDirected α fun x x_1 => x ≤ x_1]
(h : IsMax a)
:
IsTop a
theorem
isTop_or_exists_gt
{α : Type u}
[Preorder α]
[IsDirected α fun x x_1 => x ≤ x_1]
(a : α)
:
theorem
isBot_or_exists_lt
{α : Type u}
[Preorder α]
[IsDirected α fun x x_1 => x ≥ x_1]
(a : α)
:
theorem
exists_lt_of_directed_ge
(β : Type v)
[PartialOrder β]
[IsDirected β fun x x_1 => x ≥ x_1]
[Nontrivial β]
:
∃ a b, a < b
theorem
exists_lt_of_directed_le
(β : Type v)
[PartialOrder β]
[IsDirected β fun x x_1 => x ≤ x_1]
[Nontrivial β]
:
∃ a b, a < b
instance
SemilatticeSup.to_isDirected_le
{α : Type u}
[SemilatticeSup α]
:
IsDirected α fun x x_1 => x ≤ x_1
instance
SemilatticeInf.to_isDirected_ge
{α : Type u}
[SemilatticeInf α]
:
IsDirected α fun x x_1 => x ≥ x_1
instance
OrderTop.to_isDirected_le
{α : Type u}
[LE α]
[OrderTop α]
:
IsDirected α fun x x_1 => x ≤ x_1
instance
OrderBot.to_isDirected_ge
{α : Type u}
[LE α]
[OrderBot α]
:
IsDirected α fun x x_1 => x ≥ x_1