Upper / lower bounds #
In this file we define:
upper_bounds,lower_bounds: the set of upper bounds (resp., lower bounds) of a set;bdd_above s,bdd_below s: the setsis bounded above (resp., below), i.e., the set of upper (resp., lower) bounds ofsis nonempty;is_least s a,is_greatest s a:ais a least (resp., greatest) element ofs; for a partial order, it is unique if exists;is_lub s a,is_glb s a:ais 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 #
The set of upper bounds of a set.
Equations
- upper_bounds s = {x : α | ∀ ⦃a : α⦄, a ∈ s → a ≤ x}
The set of lower bounds of a set.
Equations
- lower_bounds s = {x : α | ∀ ⦃a : α⦄, a ∈ s → x ≤ a}
a is a greatest element of a set s; for a partial order, it is unique if exists
Equations
- is_greatest s a = (a ∈ s ∧ a ∈ upper_bounds s)
a is a greatest lower bound of a set s; for a partial order, it is unique if exists.
Equations
- is_glb s = is_greatest (lower_bounds s)
theorem
mem_upper_bounds
{α : Type u}
[preorder α]
{s : set α}
{a : α} :
a ∈ upper_bounds s ↔ ∀ (x : α), x ∈ s → x ≤ a
theorem
mem_lower_bounds
{α : Type u}
[preorder α]
{s : set α}
{a : α} :
a ∈ lower_bounds s ↔ ∀ (x : α), x ∈ s → a ≤ x
A set s is not bounded above if and only if for each x there exists y ∈ s such that x
is not greater than or equal to y. This version only assumes preorder structure and uses
¬(y ≤ x). A version for linear orders is called not_bdd_above_iff.
A set s is not bounded below if and only if for each x there exists y ∈ s such that x
is not less than or equal to y. This version only assumes preorder structure and uses
¬(x ≤ y). A version for linear orders is called not_bdd_below_iff.
A set s is not bounded above if and only if for each x there exists y ∈ s that is greater
than x. A version for preorders is called not_bdd_above_iff'.
A set s is not bounded below if and only if for each x there exists y ∈ s that is less
than x. A version for preorders is called not_bdd_below_iff'.
Monotonicity #
theorem
upper_bounds_mono_mem
{α : Type u}
[preorder α]
{s : set α}
⦃a b : α⦄
(hab : a ≤ b) :
a ∈ upper_bounds s → b ∈ upper_bounds s
theorem
lower_bounds_mono_mem
{α : Type u}
[preorder α]
{s : set α}
⦃a b : α⦄
(hab : a ≤ b) :
b ∈ lower_bounds s → a ∈ lower_bounds s
theorem
upper_bounds_mono
{α : Type u}
[preorder α]
⦃s t : set α⦄
(hst : s ⊆ t)
⦃a b : α⦄
(hab : a ≤ b) :
a ∈ upper_bounds t → b ∈ upper_bounds s
theorem
lower_bounds_mono
{α : Type u}
[preorder α]
⦃s t : set α⦄
(hst : s ⊆ t)
⦃a b : α⦄
(hab : a ≤ b) :
b ∈ lower_bounds t → a ∈ lower_bounds s
theorem
is_greatest.mono
{α : Type u}
[preorder α]
{s t : set α}
{a b : α}
(ha : is_greatest s a)
(hb : is_greatest t b)
(hst : s ⊆ t) :
a ≤ b
theorem
subset_lower_bounds_upper_bounds
{α : Type u}
[preorder α]
(s : set α) :
s ⊆ lower_bounds (upper_bounds s)
theorem
subset_upper_bounds_lower_bounds
{α : Type u}
[preorder α]
(s : set α) :
s ⊆ upper_bounds (lower_bounds s)
theorem
set.nonempty.bdd_above_lower_bounds
{α : Type u}
[preorder α]
{s : set α}
(hs : s.nonempty) :
theorem
set.nonempty.bdd_below_upper_bounds
{α : Type u}
[preorder α]
{s : set α}
(hs : s.nonempty) :
Conversions #
theorem
is_greatest.is_lub
{α : Type u}
[preorder α]
{s : set α}
{a : α}
(h : is_greatest s a) :
is_lub s a
theorem
is_lub.upper_bounds_eq
{α : Type u}
[preorder α]
{s : set α}
{a : α}
(h : is_lub s a) :
upper_bounds s = set.Ici a
theorem
is_glb.lower_bounds_eq
{α : Type u}
[preorder α]
{s : set α}
{a : α}
(h : is_glb s a) :
lower_bounds s = set.Iic a
theorem
is_least.lower_bounds_eq
{α : Type u}
[preorder α]
{s : set α}
{a : α}
(h : is_least s a) :
lower_bounds s = set.Iic a
theorem
is_greatest.upper_bounds_eq
{α : Type u}
[preorder α]
{s : set α}
{a : α}
(h : is_greatest s a) :
upper_bounds s = set.Ici a
theorem
is_lub_le_iff
{α : Type u}
[preorder α]
{s : set α}
{a b : α}
(h : is_lub s a) :
a ≤ b ↔ b ∈ upper_bounds s
theorem
le_is_glb_iff
{α : Type u}
[preorder α]
{s : set α}
{a b : α}
(h : is_glb s a) :
b ≤ a ↔ b ∈ lower_bounds s
If s has a greatest element, then it is bounded above.
theorem
is_greatest.nonempty
{α : Type u}
[preorder α]
{s : set α}
{a : α}
(h : is_greatest s a) :
s.nonempty
Union and intersection #
@[simp]
theorem
upper_bounds_union
{α : Type u}
[preorder α]
{s t : set α} :
upper_bounds (s ∪ t) = upper_bounds s ∩ upper_bounds t
@[simp]
theorem
lower_bounds_union
{α : Type u}
[preorder α]
{s t : set α} :
lower_bounds (s ∪ t) = lower_bounds s ∩ lower_bounds t
theorem
union_upper_bounds_subset_upper_bounds_inter
{α : Type u}
[preorder α]
{s t : set α} :
upper_bounds s ∪ upper_bounds t ⊆ upper_bounds (s ∩ t)
theorem
union_lower_bounds_subset_lower_bounds_inter
{α : Type u}
[preorder α]
{s t : set α} :
lower_bounds s ∪ lower_bounds t ⊆ lower_bounds (s ∩ t)
theorem
is_greatest_union_iff
{α : Type u}
[preorder α]
{s t : set α}
{a : α} :
is_greatest (s ∪ t) a ↔ is_greatest s a ∧ a ∈ upper_bounds t ∨ a ∈ upper_bounds s ∧ is_greatest t a
If s and t are bounded above sets in a semilattice_sup, then so is s ∪ t.
The union of two sets is bounded above if and only if each of the sets is.
The union of two sets is bounded above if and only if each of the sets is.
theorem
is_lub.union
{γ : Type w}
[semilattice_sup γ]
{a b : γ}
{s t : set γ}
(hs : is_lub s a)
(ht : is_lub t b) :
If a is the least upper bound of s and b is the least upper bound of t,
then a ⊔ b is the least upper bound of s ∪ t.
theorem
is_glb.union
{γ : Type w}
[semilattice_inf γ]
{a₁ a₂ : γ}
{s t : set γ}
(hs : is_glb s a₁)
(ht : is_glb t a₂) :
If a is the greatest lower bound of s and b is the greatest lower bound of t,
then a ⊓ b is the greatest lower bound of s ∪ t.
theorem
is_least.union
{γ : Type w}
[linear_order γ]
{a b : γ}
{s t : set γ}
(ha : is_least s a)
(hb : is_least t b) :
If a is the least element of s and b is the least element of t,
then min a b is the least element of s ∪ t.
theorem
is_greatest.union
{γ : Type w}
[linear_order γ]
{a b : γ}
{s t : set γ}
(ha : is_greatest s a)
(hb : is_greatest t b) :
is_greatest (s ∪ t) (max a b)
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.
theorem
is_lub.inter_Ici_of_mem
{γ : Type w}
[linear_order γ]
{s : set γ}
{a b : γ}
(ha : is_lub s a)
(hb : b ∈ s) :
theorem
is_glb.inter_Iic_of_mem
{γ : Type w}
[linear_order γ]
{s : set γ}
{a b : γ}
(ha : is_glb s a)
(hb : b ∈ s) :
theorem
upper_bounds_Iio
{γ : Type w}
[linear_order γ]
[densely_ordered γ]
{a : γ} :
upper_bounds (set.Iio a) = set.Ici a
theorem
lower_bounds_Ioi
{γ : Type w}
[linear_order γ]
[densely_ordered γ]
{a : γ} :
lower_bounds (set.Ioi a) = set.Iic a
Singleton #
@[simp]
@[simp]
Bounded intervals #
theorem
is_greatest_Icc
{α : Type u}
[preorder α]
{a b : α}
(h : a ≤ b) :
is_greatest (set.Icc a b) b
theorem
upper_bounds_Icc
{α : Type u}
[preorder α]
{a b : α}
(h : a ≤ b) :
upper_bounds (set.Icc a b) = set.Ici b
theorem
lower_bounds_Icc
{α : Type u}
[preorder α]
{a b : α}
(h : a ≤ b) :
lower_bounds (set.Icc a b) = set.Iic a
theorem
is_greatest_Ioc
{α : Type u}
[preorder α]
{a b : α}
(h : a < b) :
is_greatest (set.Ioc a b) b
theorem
upper_bounds_Ioc
{α : Type u}
[preorder α]
{a b : α}
(h : a < b) :
upper_bounds (set.Ioc a b) = set.Ici b
theorem
lower_bounds_Ico
{α : Type u}
[preorder α]
{a b : α}
(h : a < b) :
lower_bounds (set.Ico a b) = set.Iic a
theorem
lower_bounds_Ioo
{γ : Type w}
[semilattice_sup γ]
[densely_ordered γ]
{a b : γ}
(hab : a < b) :
lower_bounds (set.Ioo a b) = set.Iic a
theorem
lower_bound_Ioc
{γ : Type w}
[semilattice_sup γ]
[densely_ordered γ]
{a b : γ}
(hab : a < b) :
lower_bounds (set.Ioc a b) = set.Iic a
theorem
upper_bounds_Ioo
{γ : Type w}
[semilattice_inf γ]
[densely_ordered γ]
{a b : γ}
(hab : a < b) :
upper_bounds (set.Ioo a b) = set.Ici b
theorem
upper_bounds_Ico
{γ : Type w}
[semilattice_inf γ]
[densely_ordered γ]
{a b : γ}
(hab : a < b) :
upper_bounds (set.Ico a b) = set.Ici b
Univ #
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Empty set #
theorem
is_lub.nonempty
{α : Type u}
[preorder α]
{s : set α}
{a : α}
[no_bot_order α]
(hs : is_lub s a) :
s.nonempty
theorem
is_glb.nonempty
{α : Type u}
[preorder α]
{s : set α}
{a : α}
[no_top_order α]
(hs : is_glb s a) :
s.nonempty
insert #
@[simp]
Adding a point to a set preserves its boundedness above.
@[simp]
Adding a point to a set preserves its boundedness below.
theorem
is_lub.insert
{γ : Type w}
[semilattice_sup γ]
(a : γ)
{b : γ}
{s : set γ}
(hs : is_lub s b) :
theorem
is_glb.insert
{γ : Type w}
[semilattice_inf γ]
(a : γ)
{b : γ}
{s : set γ}
(hs : is_glb s b) :
theorem
is_greatest.insert
{γ : Type w}
[linear_order γ]
(a : γ)
{b : γ}
{s : set γ}
(hs : is_greatest s b) :
is_greatest (insert a s) (max a b)
theorem
is_least.insert
{γ : Type w}
[linear_order γ]
(a : γ)
{b : γ}
{s : set γ}
(hs : is_least s b) :
@[simp]
theorem
upper_bounds_insert
{α : Type u}
[preorder α]
(a : α)
(s : set α) :
upper_bounds (insert a s) = set.Ici a ∩ upper_bounds s
@[simp]
theorem
lower_bounds_insert
{α : Type u}
[preorder α]
(a : α)
(s : set α) :
lower_bounds (insert a s) = set.Iic a ∩ lower_bounds s
Pair #
Lower/upper bounds #
@[simp]
theorem
is_lub_lower_bounds
{α : Type u}
[preorder α]
{s : set α}
{a : α} :
is_lub (lower_bounds s) a ↔ is_glb s a
@[simp]
theorem
is_glb_upper_bounds
{α : Type u}
[preorder α]
{s : set α}
{a : α} :
is_glb (upper_bounds s) a ↔ is_lub s a
(In)equalities with the least upper bound and the greatest lower bound #
theorem
lower_bounds_le_upper_bounds
{α : Type u}
[preorder α]
{s : set α}
{a b : α}
(ha : a ∈ lower_bounds s)
(hb : b ∈ upper_bounds s) :
theorem
is_lub_lt_iff
{α : Type u}
[preorder α]
{s : set α}
{a b : α}
(ha : is_lub s a) :
a < b ↔ ∃ (c : α) (H : c ∈ upper_bounds s), c < b
theorem
lt_is_glb_iff
{α : Type u}
[preorder α]
{s : set α}
{a b : α}
(ha : is_glb s a) :
b < a ↔ ∃ (c : α) (H : c ∈ lower_bounds s), b < c
theorem
is_least.unique
{α : Type u}
[partial_order α]
{s : set α}
{a b : α}
(Ha : is_least s a)
(Hb : is_least s b) :
a = b
theorem
is_least.is_least_iff_eq
{α : Type u}
[partial_order α]
{s : set α}
{a b : α}
(Ha : is_least s a) :
theorem
is_greatest.unique
{α : Type u}
[partial_order α]
{s : set α}
{a b : α}
(Ha : is_greatest s a)
(Hb : is_greatest s b) :
a = b
theorem
is_greatest.is_greatest_iff_eq
{α : Type u}
[partial_order α]
{s : set α}
{a b : α}
(Ha : is_greatest s a) :
is_greatest s b ↔ a = b
theorem
is_lub.unique
{α : Type u}
[partial_order α]
{s : set α}
{a b : α}
(Ha : is_lub s a)
(Hb : is_lub s b) :
a = b
theorem
is_glb.unique
{α : Type u}
[partial_order α]
{s : set α}
{a b : α}
(Ha : is_glb s a)
(Hb : is_glb s b) :
a = b
theorem
set.subsingleton_of_is_lub_le_is_glb
{α : Type u}
[partial_order α]
{s : set α}
{a b : α}
(Ha : is_glb s a)
(Hb : is_lub s b)
(hab : b ≤ a) :
theorem
is_glb_lt_is_lub_of_ne
{α : Type u}
[partial_order α]
{s : set α}
{a b : α}
(Ha : is_glb s a)
(Hb : is_lub s b)
{x y : α}
(Hx : x ∈ s)
(Hy : y ∈ s)
(Hxy : x ≠ y) :
a < b
theorem
is_lub.exists_between
{α : Type u}
[linear_order α]
{s : set α}
{a b : α}
(h : is_lub s a)
(hb : b < a) :
theorem
is_glb.exists_between
{α : Type u}
[linear_order α]
{s : set α}
{a b : α}
(h : is_glb s a)
(hb : a < b) :
Least upper bound and the greatest lower bound in linear ordered additive commutative groups #
Images of upper/lower bounds under monotone functions #
theorem
monotone.mem_upper_bounds_image
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(Hf : monotone f)
{a : α}
{s : set α}
(Ha : a ∈ upper_bounds s) :
f a ∈ upper_bounds (f '' s)
theorem
monotone.mem_lower_bounds_image
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(Hf : monotone f)
{a : α}
{s : set α}
(Ha : a ∈ lower_bounds s) :
f a ∈ lower_bounds (f '' s)
theorem
monotone.image_upper_bounds_subset_upper_bounds_image
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : monotone f) :
f '' upper_bounds s ⊆ upper_bounds (f '' s)
theorem
monotone.image_lower_bounds_subset_lower_bounds_image
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : monotone f) :
f '' lower_bounds s ⊆ lower_bounds (f '' s)
theorem
monotone.map_is_greatest
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(Hf : monotone f)
{a : α}
{s : set α}
(Ha : is_greatest s a) :
is_greatest (f '' s) (f a)
A monotone map sends a greatest element of a set to a greatest element of its image.
theorem
antitone.mem_upper_bounds_image
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(hf : antitone f)
{a : α}
{s : set α}
(ha : a ∈ lower_bounds s) :
f a ∈ upper_bounds (f '' s)
theorem
antitone.mem_lower_bounds_image
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(hf : antitone f)
{a : α}
{s : set α}
(ha : a ∈ upper_bounds s) :
f a ∈ lower_bounds (f '' s)
theorem
antitone.image_lower_bounds_subset_upper_bounds_image
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : antitone f) :
f '' lower_bounds s ⊆ upper_bounds (f '' s)
theorem
antitone.image_upper_bounds_subset_lower_bounds_image
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : antitone f) :
f '' upper_bounds s ⊆ lower_bounds (f '' s)
theorem
antitone.map_is_greatest
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(hf : antitone f)
{a : α}
{s : set α}
(ha : is_greatest s a) :
An antitone map sends a greatest element of a set to a least element of its image.
theorem
antitone.map_is_least
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(hf : antitone f)
{a : α}
{s : set α}
(ha : is_least s a) :
is_greatest (f '' s) (f a)
An antitone map sends a least element of a set to a greatest element of its image.
theorem
order_iso.upper_bounds_image
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(f : α ≃o β)
{s : set α} :
upper_bounds (⇑f '' s) = ⇑f '' upper_bounds s
theorem
order_iso.lower_bounds_image
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(f : α ≃o β)
{s : set α} :
lower_bounds (⇑f '' s) = ⇑f '' lower_bounds s