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 sets
is bounded above (resp., below), i.e., the set of upper (resp., lower) bounds ofs
is nonempty;IsLeast s a
,IsGreatest s a
:a
is a least (resp., greatest) element ofs
; 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) ofs
; for a partial order, it is unique if exists. We also prove various lemmas about monotonicity, behaviour under∪∪
,∩∩
,insert
, and provide formulas for∅∅
,univ
, and intervals.
Definitions #
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)
A set s
is not bounded above if and only if for each x
there exists y ∈ s∈ s
such that x
is not greater than or equal to y
. This version only assumes Preorder
structure and uses
¬(y ≤ x)¬(y ≤ x)≤ x)
. A version for linear orders is called not_bddAbove_iff
.
A set s
is not bounded below if and only if for each x
there exists y ∈ s∈ s
such that x
is not less than or equal to y
. This version only assumes Preorder
structure and uses
¬(x ≤ y)¬(x ≤ y)≤ y)
. A version for linear orders is called not_bddBelow_iff
.
A set s
is not bounded above if and only if for each x
there exists y ∈ s∈ s
that is greater
than x
. A version for preorders is called not_bddAbove_iff'
.
A set s
is not bounded below if and only if for each x
there exists y ∈ s∈ s
that is less
than x
. A version for preorders is called not_bddBelow_iff'
.
If a
is the least element of a set s
, then subtype s
is an order with bottom element.
Equations
- IsLeast.orderBot h = OrderBot.mk (_ : ∀ (x : { a // a ∈ s }), ⊥ ≤ x)
If a
is the greatest element of a set s
, then subtype s
is an order with top element.
Equations
- IsGreatest.orderTop h = OrderTop.mk (_ : ∀ (x : { a // a ∈ s }), x ≤ ⊤)
Monotonicity #
If a
is a greatest lower bound for sets s
and p
, then it is a greater lower bound for any
set t
, s ⊆ t ⊆ p⊆ t ⊆ p⊆ p
.
Conversions #
If s
has a greatest element, then it is bounded above.
Union and intersection #
If a
is the greatest lower bound of s
and b
is the greatest lower bound of t
,
then a ⊓ b⊓ b
is the greatest lower bound of s ∪ t∪ t
.
If a
is the greatest element of s
and b
is the greatest element of t
,
then max a b
is the greatest element of s ∪ t∪ t
.
Singleton #
Bounded intervals #
Univ #
Empty set #
insert #
Adding a point to a set preserves its boundedness above.
Adding a point to a set preserves its boundedness below.
Pair #
Lower/upper bounds #
(In)equalities with the least upper bound and the greatest lower bound #
Images of upper/lower bounds under monotone functions #
The image under a monotone function on a set t
of a subset which has an upper bound in t
is bounded above.
The image under a monotone function on a set t
of a subset which has a lower bound in t
is bounded below.
A monotone map sends a greatest element of a set to a greatest element of its image.
The image under an antitone function of a set which is bounded above is bounded below.
The image under an antitone function of a set which is bounded below is bounded above.
An antitone map sends a greatest element of a set to a least element of its image.
An antitone map sends a least element of a set to a greatest element of its image.
A monotone map sends a greatest element of a set to a greatest element of its image.
See also Monotone.map_bddAbove
.
See also Monotone.map_bddBelow
.