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

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For