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 family f is r-directed.
directed_on r s: Predicate stating that the set s is r-directed.
is_directed α r: Prop-valued mixin stating that α is r-directed. Follows the style of the unbundled relation classes such as is_total.
scott_continuous: Predicate stating that a function between preorders preserves is_lub on directed sets.

References #

Gierz et al, A Compendium of Continuous Lattices

source

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

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

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

source

theorem directed_on_iff_directed {α : Type u} {r : α → α → Prop} {s : set α} :

directed_on r s ↔ directed r coe

source

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.

source

theorem directed_on_range {α : Type u} {ι : Sort w} {r : α → α → Prop} {f : ι → α} :

directed r f ↔ directed_on r (set.range f)

source

theorem directed_on_image {α : Type u} {β : Type v} {r : α → α → Prop} {s : set β} {f : β → α} :

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

source

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

source

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

source

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

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

source

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

source

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

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.

source

theorem monotone.directed_le {α : Type u} {β : Type v} [semilattice_sup α] [preorder β] {f : α → β} :

monotone f → directed has_le.le f

source

theorem antitone.directed_ge {α : Type u} {β : Type v} [semilattice_sup α] [preorder β] {f : α → β} (hf : antitone f) :

directed ge f

source

theorem directed_on_of_sup_mem {α : Type u} [semilattice_sup α] {S : set α} (H : ∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊔ j ∈ S) :

directed_on has_le.le S

A set stable by supremum is ≤-directed.

source

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 ⊥)

source

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.

source

theorem monotone.directed_ge {α : Type u} {β : Type v} [semilattice_inf α] [preorder β] {f : α → β} (hf : monotone f) :

directed ge f

source

theorem antitone.directed_le {α : Type u} {β : Type v} [semilattice_inf α] [preorder β] {f : α → β} (hf : antitone f) :

directed has_le.le f

source

theorem directed_on_of_inf_mem {α : Type u} [semilattice_inf α] {S : set α} (H : ∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊓ j ∈ S) :

directed_on ge S

A set stable by infimum is ≥-directed.

source

theorem is_total.directed {α : Type u} {ι : Sort w} {r : α → α → Prop} [is_total α r] (f : ι → α) :

directed r f

source

@[class]

structure is_directed (α : Type u_1) (r : α → α → Prop) :

Prop

directed : ∀ (a b : α), ∃ (c : α), r a c ∧ r b c

is_directed α r states that for any elements a, b there exists an element c such that r a c and r b c.

Instances of this typeclass

source

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

∃ (c : α), r a c ∧ r b c

source

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

directed r id

source

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

directed r id ↔ is_directed α r

source

theorem directed_on_univ {α : Type u} {r : α → α → Prop} [is_directed α r] :

directed_on r set.univ

source

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

directed_on r set.univ ↔ is_directed α r

source

@[protected, instance]

def is_total.to_is_directed {α : Type u} {r : α → α → Prop} [is_total α r] :

is_directed α r

source

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

source

theorem exists_ge_ge {α : Type u} [has_le α] [is_directed α has_le.le] (a b : α) :

∃ (c : α), a ≤ c ∧ b ≤ c

source

theorem exists_le_le {α : Type u} [has_le α] [is_directed α ge] (a b : α) :

∃ (c : α), c ≤ a ∧ c ≤ b

source

@[protected, instance]

def order_dual.is_directed_ge {α : Type u} [has_le α] [is_directed α has_le.le] :

is_directed αᵒᵈ ge

source

@[protected, instance]

def order_dual.is_directed_le {α : Type u} [has_le α] [is_directed α ge] :

is_directed αᵒᵈ has_le.le

source

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)

source

theorem directed_on_singleton {α : Type u} {r : α → α → Prop} (h : reflexive r) (a : α) :

directed_on r {a}

source

theorem directed_on_pair {α : Type u} {r : α → α → Prop} (h : reflexive r) {a b : α} (hab : r a b) :

directed_on r {a, b}

source

theorem directed_on_pair' {α : Type u} {r : α → α → Prop} (h : reflexive r) {a b : α} (hab : r a b) :

directed_on r {b, a}

source

@[protected]

theorem is_min.is_bot {α : Type u} [preorder α] {a : α} [is_directed α ge] (h : is_min a) :

is_bot a

source

@[protected]

theorem is_max.is_top {α : Type u} [preorder α] {a : α} [is_directed α has_le.le] (h : is_max a) :

is_top a

source

theorem directed_on.is_bot_of_is_min {α : Type u} [preorder α] {s : set α} (hd : directed_on ge s) {m : α} (hm : m ∈ s) (hmin : ∀ (a : α), a ∈ s → a ≤ m → m ≤ a) (a : α) (H : a ∈ s) :

m ≤ a

source

theorem directed_on.is_top_of_is_max {α : Type u} [preorder α] {s : set α} (hd : directed_on has_le.le s) {m : α} (hm : m ∈ s) (hmax : ∀ (a : α), a ∈ s → m ≤ a → a ≤ m) (a : α) (H : a ∈ s) :

a ≤ m

source

theorem is_top_or_exists_gt {α : Type u} [preorder α] [is_directed α has_le.le] (a : α) :

is_top a ∨ ∃ (b : α), a < b

source

theorem is_bot_or_exists_lt {α : Type u} [preorder α] [is_directed α ge] (a : α) :

is_bot a ∨ ∃ (b : α), b < a

source

theorem is_bot_iff_is_min {α : Type u} [preorder α] {a : α} [is_directed α ge] :

is_bot a ↔ is_min a

source

theorem is_top_iff_is_max {α : Type u} [preorder α] {a : α} [is_directed α has_le.le] :

is_top a ↔ is_max a

source

theorem exists_lt_of_directed_ge (β : Type v) [partial_order β] [is_directed β ge] [nontrivial β] :

∃ (a b : β), a < b

source

theorem exists_lt_of_directed_le (β : Type v) [partial_order β] [is_directed β has_le.le] [nontrivial β] :

∃ (a b : β), a < b

source

@[protected, instance]

def semilattice_sup.to_is_directed_le {α : Type u} [semilattice_sup α] :

is_directed α has_le.le

source

@[protected, instance]

def semilattice_inf.to_is_directed_ge {α : Type u} [semilattice_inf α] :

is_directed α ge

source

@[protected, instance]

def order_top.to_is_directed_le {α : Type u} [has_le α] [order_top α] :

is_directed α has_le.le

source

@[protected, instance]

def order_bot.to_is_directed_ge {α : Type u} [has_le α] [order_bot α] :

is_directed α ge

source

def scott_continuous {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α → β) :

Prop

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)

source

@[protected]

theorem scott_continuous.monotone {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (h : scott_continuous f) :

monotone f