Definitions about upper/lower bounds

In this file we define:

• upperBounds, lowerBounds : the set of upper bounds (resp., lower bounds) of a set;
• BddAbove s, BddBelow s : the set s is bounded above (resp., below), i.e., the set of upper (resp., lower) bounds of s is nonempty;
• IsLeast s a, IsGreatest s a : a is a least (resp., greatest) element of s; for a partial order, it is unique if exists;
• IsLUB s a, IsGLB s a : a is a least upper bound (resp., a greatest lower bound) of s; for a partial order, it is unique if exists.
• IsCofinal s: for every a, there exists a member of s greater or equal to it.
• IsCofinalFor s t : for all a ∈ s there exists b ∈ t such that a ≤ b
• IsCoinitial s: for every a, there exists a member of s less than or equal to it.
• IsCoinitialFor s t : for all a ∈ s there exists b ∈ t such that b ≤ a
• SupSet α, InfSet α: typeclasses introducing the operation SupSet.sSup and InfSet.sInf (exported to the root namespace).
• OrderSupSet α, OrderInfSet α: typeclasses expressing that sSup (resp., sInf) returns the least upper bound (resp., the greatest lower bound) of a set whenever one exists.

def upperBounds {α : Type u_1} [LE α] (s : Set α) : Set α

The set of upper bounds of a set.

Equations

• upperBounds s = {x : α | ∀ ⦃a : α⦄, a ∈ s → a ≤ x}

def lowerBounds {α : Type u_1} [LE α] (s : Set α) : Set α

The set of lower bounds of a set.

Equations

• lowerBounds s = {x : α | ∀ ⦃a : α⦄, a ∈ s → x ≤ a}

def BddAbove {α : Type u_1} [LE α] (s : Set α) : Prop

A set is bounded above if there exists an upper bound.

Equations

• BddAbove s = (upperBounds s).Nonempty

def BddBelow {α : Type u_1} [LE α] (s : Set α) : Prop

A set is bounded below if there exists a lower bound.

Equations

• BddBelow s = (lowerBounds s).Nonempty

def IsLeast {α : Type u_1} [LE α] (s : Set α) (a : α) : Prop

a is a least element of a set s; for a partial order, it is unique if exists.

Equations

• IsLeast s a = (a ∈ s ∧ a ∈ lowerBounds s)

def IsGreatest {α : Type u_1} [LE α] (s : Set α) (a : α) : Prop

a is a greatest element of a set s; for a partial order, it is unique if exists.

Equations

• IsGreatest s a = (a ∈ s ∧ a ∈ upperBounds s)

def IsLUB {α : Type u_1} [LE α] (s : Set α) : α → Prop

a is a least upper bound of a set s; for a partial order, it is unique if exists.

Equations

• IsLUB s = IsLeast (upperBounds s)

def IsGLB {α : Type u_1} [LE α] (s : Set α) : α → Prop

a is a greatest lower bound of a set s; for a partial order, it is unique if exists.

Equations

• IsGLB s = IsGreatest (lowerBounds s)

def IsCofinalFor {α : Type u_1} [LE α] (s t : Set α) : Prop

A set s is said to be cofinal for a set t if, for all a ∈ s there exists b ∈ t such that a ≤ b.

Equations

• IsCofinalFor s t = ∀ ⦃a : α⦄, a ∈ s → ∃ (b : α), b ∈ t ∧ a ≤ b

def IsCoinitialFor {α : Type u_1} [LE α] (s t : Set α) : Prop

A set s is said to be coinitial for a set t if, for all a ∈ s there exists b ∈ t such that b ≤ a.

Equations

• IsCoinitialFor s t = ∀ ⦃a : α⦄, a ∈ s → ∃ (b : α), b ∈ t ∧ b ≤ a

def IsCofinal {α : Type u_1} [LE α] (s : Set α) : Prop

A set is cofinal when for every x : α there exists y ∈ s with x ≤ y.

Equations

• IsCofinal s = ∀ (x : α), ∃ (y : α), y ∈ s ∧ x ≤ y

def IsCoinitial {α : Type u_1} [LE α] (s : Set α) : Prop

A set is coinitial when for every x : α there exists y ∈ s with y ≤ x.

Equations

• IsCoinitial s = ∀ (x : α), ∃ (y : α), y ∈ s ∧ y ≤ x

class SupSet (α : Type u_2) : Type u_2

Class for the sSup operator

• sSup : Set α → α

  Supremum of a set

class InfSet (α : Type u_2) : Type u_2

Class for the sInf operator

• sInf : Set α → α

  Infimum of a set

class OrderSupSet (α : Type u_2) [LE α] extends SupSet α : Type u_2

OrderSupSet α expresses that α is equipped with the operation sSup that returns the least upper bound of a set whenever one exists.

• sSup : Set α → α
• isLUB_sSup_of_isLUB (s : Set α) (a : α) : IsLUB s a → IsLUB s (sSup s)

class OrderInfSet (α : Type u_2) [LE α] extends InfSet α : Type u_2

OrderInfSet α expresses that α is equipped with the operation sInf that returns the greatest lower bound of a set whenever one exists.

• sInf : Set α → α
• isGLB_sInf_of_isGLB (s : Set α) (a : α) : IsGLB s a → IsGLB s (sInf s)