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 family f is r-directed.
DirectedOn r s: Predicate stating that the set s is r-directed.
IsDirected α r: Prop-valued mixin stating that α is r-directed. Follows the style of the unbundled relation classes such as IsTotal.

source

ink

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

ink

def DirectedOn {α : 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

DirectedOn r s = ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → ∃ z, z ∈ s ∧ r x z ∧ r y z

source

ink

theorem directedOn_iff_directed {α : Type u} {r : α → α → Prop} {s : Set α} :

DirectedOn r s ↔ Directed r Subtype.val

source

ink

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.

source

ink

theorem directedOn_range {α : Type u} {β : Type v} {r : α → α → Prop} {f : β → α} :

Directed r f ↔ DirectedOn r (Set.range f)

source

ink

theorem directedOn_image {α : Type u} {β : Type v} {r : α → α → Prop} {s : Set β} {f : β → α} :

DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s

source

ink

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

source

ink

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

source

ink

theorem directed_comp {α : Type u} {β : Type v} {r : α → α → Prop} {ι : Sort u_1} {f : ι → β} {g : β → α} :

Directed r (g ∘ f) ↔ Directed (g ⁻¹'o r) f

source

ink

theorem Directed.mono {α : Type u} {r : α → α → Prop} {s : α → α → Prop} {ι : Sort u_1} {f : ι → α} (H : (a b : α) → r a b → s a b) (h : Directed r f) :

Directed s f

source

ink

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

ink

theorem directed_of_sup {α : Type u} {β : Type v} [inst : 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.

source

ink

theorem Monotone.directed_le {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst : Preorder β] {f : α → β} :

Monotone f → Directed (fun x x_1 => x ≤ x_1) f

source

ink

theorem Antitone.directed_ge {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst : Preorder β] {f : α → β} (hf : Antitone f) :

Directed (fun x x_1 => x ≥ x_1) f

source

ink

theorem directedOn_of_sup_mem {α : Type u} [inst : 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.

source

ink

theorem Directed.extend_bot {α : Type u} {β : Type v} {ι : Sort w} [inst : Preorder α] [inst : 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 ⊥)

source

ink

theorem directed_of_inf {α : Type u} {β : Type v} [inst : 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.

source

ink

theorem Monotone.directed_ge {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst : Preorder β] {f : α → β} (hf : Monotone f) :

Directed (fun x x_1 => x ≥ x_1) f

source

ink

theorem Antitone.directed_le {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst : Preorder β] {f : α → β} (hf : Antitone f) :

Directed (fun x x_1 => x ≤ x_1) f

source

ink

theorem directedOn_of_inf_mem {α : Type u} [inst : 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.

source

ink

class IsDirected (α : Type u_1) (r : α → α → Prop) :

Prop

For every pair of elements a and b there is a c such that r a c and r b c
directed : ∀ (a b : α), ∃ c, r a c ∧ r 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

source

ink

theorem directed_of {α : Type u} (r : α → α → Prop) [inst : IsDirected α r] (a : α) (b : α) :

∃ c, r a c ∧ r b c

source

ink

theorem directed_id {α : Type u} {r : α → α → Prop} [inst : IsDirected α r] :

Directed r id

source

ink

theorem directed_id_iff {α : Type u} {r : α → α → Prop} :

Directed r id ↔ IsDirected α r

source

ink

theorem directedOn_univ {α : Type u} {r : α → α → Prop} [inst : IsDirected α r] :

DirectedOn r Set.univ

source

ink

theorem directedOn_univ_iff {α : Type u} {r : α → α → Prop} :

DirectedOn r Set.univ ↔ IsDirected α r

source

ink

instance IsTotal.to_isDirected {α : Type u} {r : α → α → Prop} [inst : IsTotal α r] :

IsDirected α r

Equations

@IsTotal.to_isDirected = @IsTotal.to_isDirected.proof_1

source

ink

theorem isDirected_mono {α : Type u} {r : α → α → Prop} (s : α → α → Prop) [inst : IsDirected α r] (h : ⦃a b : α⦄ → r a b → s a b) :

IsDirected α s

source

ink

theorem exists_ge_ge {α : Type u} [inst : LE α] [inst : IsDirected α fun x x_1 => x ≤ x_1] (a : α) (b : α) :

∃ c, a ≤ c ∧ b ≤ c

source

ink

theorem exists_le_le {α : Type u} [inst : LE α] [inst : IsDirected α fun x x_1 => x ≥ x_1] (a : α) (b : α) :

∃ c, c ≤ a ∧ c ≤ b

source

ink

instance OrderDual.isDirected_ge {α : Type u} [inst : LE α] [inst : IsDirected α fun x x_1 => x ≤ x_1] :

IsDirected αᵒᵈ fun x x_1 => x ≥ x_1

Equations

@OrderDual.isDirected_ge = @OrderDual.isDirected_ge.proof_1

source

ink

instance OrderDual.isDirected_le {α : Type u} [inst : LE α] [inst : IsDirected α fun x x_1 => x ≥ x_1] :

IsDirected αᵒᵈ fun x x_1 => x ≤ x_1

Equations

@OrderDual.isDirected_le = @OrderDual.isDirected_le.proof_1

source

ink

theorem IsMin.isBot {α : Type u} [inst : Preorder α] {a : α} [inst : IsDirected α fun x x_1 => x ≥ x_1] (h : IsMin a) :

IsBot a

source

ink

theorem IsMax.isTop {α : Type u} [inst : Preorder α] {a : α} [inst : IsDirected α fun x x_1 => x ≤ x_1] (h : IsMax a) :

IsTop a

source

ink

theorem DirectedOn.is_bot_of_is_min {α : Type u} [inst : Preorder α] {s : Set α} (hd : DirectedOn (fun x x_1 => x ≥ x_1) s) {m : α} (hm : m ∈ s) (hmin : ∀ (a : α), a ∈ s → a ≤ m → m ≤ a) (a : α) :

a ∈ s → m ≤ a

source

ink

theorem DirectedOn.is_top_of_is_max {α : Type u} [inst : Preorder α] {s : Set α} (hd : DirectedOn (fun x x_1 => x ≤ x_1) s) {m : α} (hm : m ∈ s) (hmax : ∀ (a : α), a ∈ s → m ≤ a → a ≤ m) (a : α) :

a ∈ s → a ≤ m

source

ink

theorem isTop_or_exists_gt {α : Type u} [inst : Preorder α] [inst : IsDirected α fun x x_1 => x ≤ x_1] (a : α) :

IsTop a ∨ ∃ b, a < b

source

ink

theorem isBot_or_exists_lt {α : Type u} [inst : Preorder α] [inst : IsDirected α fun x x_1 => x ≥ x_1] (a : α) :

IsBot a ∨ ∃ b, b < a

source

ink

theorem isBot_iff_isMin {α : Type u} [inst : Preorder α] {a : α} [inst : IsDirected α fun x x_1 => x ≥ x_1] :

IsBot a ↔ IsMin a

source

ink

theorem isTop_iff_isMax {α : Type u} [inst : Preorder α] {a : α} [inst : IsDirected α fun x x_1 => x ≤ x_1] :

IsTop a ↔ IsMax a

source

ink

theorem exists_lt_of_directed_ge (β : Type v) [inst : PartialOrder β] [inst : IsDirected β fun x x_1 => x ≥ x_1] [inst : Nontrivial β] :

∃ a b, a < b

source

ink

theorem exists_lt_of_directed_le (β : Type v) [inst : PartialOrder β] [inst : IsDirected β fun x x_1 => x ≤ x_1] [inst : Nontrivial β] :

∃ a b, a < b

source

ink

instance SemilatticeSup.to_isDirected_le {α : Type u} [inst : SemilatticeSup α] :

IsDirected α fun x x_1 => x ≤ x_1

Equations

@SemilatticeSup.to_isDirected_le = @SemilatticeSup.to_isDirected_le.proof_1

source

ink

instance SemilatticeInf.to_isDirected_ge {α : Type u} [inst : SemilatticeInf α] :

IsDirected α fun x x_1 => x ≥ x_1

Equations

@SemilatticeInf.to_isDirected_ge = @SemilatticeInf.to_isDirected_ge.proof_1

source

ink

instance OrderTop.to_isDirected_le {α : Type u} [inst : LE α] [inst : OrderTop α] :

IsDirected α fun x x_1 => x ≤ x_1

Equations

@OrderTop.to_isDirected_le = @OrderTop.to_isDirected_le.proof_1

source

ink

instance OrderBot.to_isDirected_ge {α : Type u} [inst : LE α] [inst : OrderBot α] :

IsDirected α fun x x_1 => x ≥ x_1

Equations

@OrderBot.to_isDirected_ge = @OrderBot.to_isDirected_ge.proof_1