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.

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