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
• IsCoinitialFor s t : for all a ∈ s there exists b ∈ t such that b ≤ a

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

The set of upper bounds of a set.

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

The set of lower bounds of a set.

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

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

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

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

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.

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.

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.

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.

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.

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.

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

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