Mathlib.Order.Bounds.Defs

Module docstring

{"# 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. "}

upperBounds definition

(s : Set α) : Set α

Full source

/-- The set of upper bounds of a set. -/
def upperBounds (s : Set α) : Set α :=
  { x | ∀ ⦃a⦄, a ∈ s → a ≤ x }

Set of upper bounds

Informal description

For a set $s$ in a type $\alpha$ with a preorder, the set of upper bounds of $s$ consists of all elements $x \in \alpha$ such that for every $a \in s$, $a \leq x$.

lowerBounds definition

(s : Set α) : Set α

Full source

/-- The set of lower bounds of a set. -/
def lowerBounds (s : Set α) : Set α :=
  { x | ∀ ⦃a⦄, a ∈ s → x ≤ a }

Set of lower bounds of a set

Informal description

For a set $ s $ in a partially ordered type $ \alpha $, the set of lower bounds of $ s $ consists of all elements $ x \in \alpha $ such that $ x \leq a $ for every $ a \in s $.

BddAbove definition

(s : Set α)

Full source

/-- A set is bounded above if there exists an upper bound. -/
def BddAbove (s : Set α) :=
  (upperBounds s).Nonempty

Bounded above set

Informal description

A set $s$ in a type $\alpha$ with a preorder is called bounded above if there exists an element $x \in \alpha$ such that $a \leq x$ for all $a \in s$. In other words, the set of upper bounds of $s$ is nonempty.

BddBelow definition

(s : Set α)

Full source

/-- A set is bounded below if there exists a lower bound. -/
def BddBelow (s : Set α) :=
  (lowerBounds s).Nonempty

Bounded below set

Informal description

A set $ s $ in a partially ordered type $ \alpha $ is called bounded below if there exists an element $ x \in \alpha $ such that $ x \leq a $ for every $ a \in s $. In other words, the set of lower bounds of $ s $ is nonempty.

IsLeast definition

(s : Set α) (a : α) : Prop

Full source

/-- `a` is a least element of a set `s`; for a partial order, it is unique if exists. -/
def IsLeast (s : Set α) (a : α) : Prop :=
  a ∈ sa ∈ s ∧ a ∈ lowerBounds s

Least element of a set

Informal description

An element $ a $ of a partially ordered type $ \alpha $ is called a least element of a set $ s \subseteq \alpha $ if $ a $ belongs to $ s $ and $ a $ is a lower bound for $ s $, i.e., $ a \leq x $ for all $ x \in s $. In a partial order, such an element is unique if it exists.

IsGreatest definition

(s : Set α) (a : α) : Prop

Full source

/-- `a` is a greatest element of a set `s`; for a partial order, it is unique if exists. -/
def IsGreatest (s : Set α) (a : α) : Prop :=
  a ∈ sa ∈ s ∧ a ∈ upperBounds s

Greatest element of a set

Informal description

An element $a$ is the greatest element of a set $s$ in a partially ordered type $\alpha$ if $a$ belongs to $s$ and $a$ is an upper bound for $s$, meaning $x \leq a$ for all $x \in s$.

IsLUB definition

(s : Set α) : α → Prop

Full source

/-- `a` is a least upper bound of a set `s`; for a partial order, it is unique if exists. -/
def IsLUB (s : Set α) : α → Prop :=
  IsLeast (upperBounds s)

Least upper bound (supremum) of a set

Informal description

An element $ a $ of a partially ordered type $ \alpha $ is called a least upper bound (or supremum) of a set $ s \subseteq \alpha $ if $ a $ is the least element of the set of upper bounds of $ s $. That is, $ a $ is an upper bound for $ s $ (i.e., $ x \leq a $ for all $ x \in s $) and is less than or equal to any other upper bound of $ s $. In a partial order, such an element is unique if it exists.

IsGLB definition

(s : Set α) : α → Prop

Full source

/-- `a` is a greatest lower bound of a set `s`; for a partial order, it is unique if exists. -/
def IsGLB (s : Set α) : α → Prop :=
  IsGreatest (lowerBounds s)

Greatest lower bound (infimum) of a set

Informal description

An element $ a $ of a partially ordered type $ \alpha $ is called a greatest lower bound (or infimum) of a set $ s \subseteq \alpha $ if $ a $ is the greatest element of the set of lower bounds of $ s $. That is, $ a $ is a lower bound for $ s $ (i.e., $ a \leq x $ for all $ x \in s $) and is greater than or equal to any other lower bound of $ s $. In a partial order, such an element is unique if it exists.

IsCofinal definition

(s : Set α) : Prop

Full source

/-- A set is cofinal when for every `x : α` there exists `y ∈ s` with `x ≤ y`. -/
def IsCofinal (s : Set α) : Prop :=
  ∀ x, ∃ y ∈ s, x ≤ y

Cofinal subset

Informal description

A subset $s$ of a type $\alpha$ with a preorder is called *cofinal* if for every element $x \in \alpha$, there exists an element $y \in s$ such that $x \leq y$.