mathlib documentation

order.bounds

Upper / lower bounds

In this file we define:

We also prove various lemmas about monotonicity, behaviour under , , insert, and provide formulas for , univ, and intervals.

Definitions

def upper_bounds {α : Type u} [preorder α] :
set αset α

The set of upper bounds of a set.

Equations
def lower_bounds {α : Type u} [preorder α] :
set αset α

The set of lower bounds of a set.

Equations
def bdd_above {α : Type u} [preorder α] :
set α → Prop

A set is bounded above if there exists an upper bound.

Equations
def bdd_below {α : Type u} [preorder α] :
set α → Prop

A set is bounded below if there exists a lower bound.

Equations
def is_least {α : Type u} [preorder α] :
set αα → Prop

a is a least element of a set s; for a partial order, it is unique if exists.

Equations
def is_greatest {α : Type u} [preorder α] :
set αα → Prop

a is a greatest element of a set s; for a partial order, it is unique if exists

Equations
def is_lub {α : Type u} [preorder α] :
set αα → Prop

a is a least upper bound of a set s; for a partial order, it is unique if exists.

Equations
def is_glb {α : Type u} [preorder α] :
set αα → Prop

a is a greatest lower bound of a set s; for a partial order, it is unique if exists.

Equations
theorem mem_upper_bounds {α : Type u} [preorder α] {s : set α} {a : α} :
a upper_bounds s ∀ (x : α), x sx a

theorem mem_lower_bounds {α : Type u} [preorder α] {s : set α} {a : α} :
a lower_bounds s ∀ (x : α), x sa x

theorem not_bdd_above_iff' {α : Type u} [preorder α] {s : set α} :
¬bdd_above s ∀ (x : α), ∃ (y : α) (H : y s), ¬y 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.

theorem not_bdd_below_iff' {α : Type u} [preorder α] {s : set α} :
¬bdd_below s ∀ (x : α), ∃ (y : α) (H : y s), ¬x y

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.

theorem not_bdd_above_iff {α : Type u_1} [linear_order α] {s : set α} :
¬bdd_above s ∀ (x : α), ∃ (y : α) (H : y s), x < y

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

theorem not_bdd_below_iff {α : Type u_1} [linear_order α] {s : set α} :
¬bdd_below s ∀ (x : α), ∃ (y : α) (H : y s), y < x

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_set {α : Type u} [preorder α] ⦃s t : set α⦄ :

theorem lower_bounds_mono_set {α : Type u} [preorder α] ⦃s t : set α⦄ :

theorem upper_bounds_mono_mem {α : Type u} [preorder α] {s : set α} ⦃a b : α⦄ :
a ba upper_bounds sb upper_bounds s

theorem lower_bounds_mono_mem {α : Type u} [preorder α] {s : set α} ⦃a b : α⦄ :
a bb lower_bounds sa lower_bounds s

theorem upper_bounds_mono {α : Type u} [preorder α] ⦃s t : set α⦄ (hst : s t) ⦃a b : α⦄ :
a ba upper_bounds tb upper_bounds s

theorem lower_bounds_mono {α : Type u} [preorder α] ⦃s t : set α⦄ (hst : s t) ⦃a b : α⦄ :
a bb lower_bounds ta lower_bounds s

theorem bdd_above.mono {α : Type u} [preorder α] ⦃s t : set α⦄ :
s tbdd_above tbdd_above s

If s ⊆ t and t is bounded above, then so is s.

theorem bdd_below.mono {α : Type u} [preorder α] ⦃s t : set α⦄ :
s tbdd_below tbdd_below s

If s ⊆ t and t is bounded below, then so is s.

theorem is_lub.of_subset_of_superset {α : Type u} [preorder α] {a : α} {s t p : set α} :
is_lub s ais_lub p as tt pis_lub t a

If a is a least upper bound for sets s and p, then it is a least upper bound for any set t, s ⊆ t ⊆ p.

theorem is_glb.of_subset_of_superset {α : Type u} [preorder α] {a : α} {s t p : set α} :
is_glb s ais_glb p as tt pis_glb t a

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.

theorem is_least.mono {α : Type u} [preorder α] {s t : set α} {a b : α} :
is_least s ais_least t bs tb a

theorem is_greatest.mono {α : Type u} [preorder α] {s t : set α} {a b : α} :
is_greatest s ais_greatest t bs ta b

theorem is_lub.mono {α : Type u} [preorder α] {s t : set α} {a b : α} :
is_lub s ais_lub t bs ta b

theorem is_glb.mono {α : Type u} [preorder α] {s t : set α} {a b : α} :
is_glb s ais_glb t bs tb a

Conversions

theorem is_least.is_glb {α : Type u} [preorder α] {s : set α} {a : α} :
is_least s ais_glb s a

theorem is_greatest.is_lub {α : Type u} [preorder α] {s : set α} {a : α} :
is_greatest s ais_lub s a

theorem is_lub.upper_bounds_eq {α : Type u} [preorder α] {s : set α} {a : α} :

theorem is_glb.lower_bounds_eq {α : Type u} [preorder α] {s : set α} {a : α} :

theorem is_least.lower_bounds_eq {α : Type u} [preorder α] {s : set α} {a : α} :

theorem is_greatest.upper_bounds_eq {α : Type u} [preorder α] {s : set α} {a : α} :

theorem is_lub_le_iff {α : Type u} [preorder α] {s : set α} {a b : α} :
is_lub s a(a b b upper_bounds s)

theorem le_is_glb_iff {α : Type u} [preorder α] {s : set α} {a b : α} :
is_glb s a(b a b lower_bounds s)

theorem is_lub.bdd_above {α : Type u} [preorder α] {s : set α} {a : α} :
is_lub s abdd_above s

If s has a least upper bound, then it is bounded above.

theorem is_glb.bdd_below {α : Type u} [preorder α] {s : set α} {a : α} :
is_glb s abdd_below s

If s has a greatest lower bound, then it is bounded below.

theorem is_greatest.bdd_above {α : Type u} [preorder α] {s : set α} {a : α} :

If s has a greatest element, then it is bounded above.

theorem is_least.bdd_below {α : Type u} [preorder α] {s : set α} {a : α} :

If s has a least element, then it is bounded below.

theorem is_least.nonempty {α : Type u} [preorder α] {s : set α} {a : α} :
is_least s a → s.nonempty

theorem is_greatest.nonempty {α : Type u} [preorder α] {s : set α} {a : α} :

Union and intersection

@[simp]
theorem upper_bounds_union {α : Type u} [preorder α] {s t : set α} :

@[simp]
theorem lower_bounds_union {α : Type u} [preorder α] {s t : set α} :

theorem is_least_union_iff {α : Type u} [preorder α] {a : α} {s t : set α} :

theorem is_greatest_union_iff {α : Type u} [preorder α] {s t : set α} {a : α} :

theorem bdd_above.inter_of_left {α : Type u} [preorder α] {s t : set α} :
bdd_above sbdd_above (s t)

If s is bounded, then so is s ∩ t

theorem bdd_above.inter_of_right {α : Type u} [preorder α] {s t : set α} :
bdd_above tbdd_above (s t)

If t is bounded, then so is s ∩ t

theorem bdd_below.inter_of_left {α : Type u} [preorder α] {s t : set α} :
bdd_below sbdd_below (s t)

If s is bounded, then so is s ∩ t

theorem bdd_below.inter_of_right {α : Type u} [preorder α] {s t : set α} :
bdd_below tbdd_below (s t)

If t is bounded, then so is s ∩ t

theorem bdd_above.union {γ : Type w} [semilattice_sup γ] {s t : set γ} :
bdd_above sbdd_above tbdd_above (s t)

If s and t are bounded above sets in a semilattice_sup, then so is s ∪ t.

theorem bdd_above_union {γ : Type w} [semilattice_sup γ] {s t : set γ} :

The union of two sets is bounded above if and only if each of the sets is.

theorem bdd_below.union {γ : Type w} [semilattice_inf γ] {s t : set γ} :
bdd_below sbdd_below tbdd_below (s t)

theorem bdd_below_union {γ : Type w} [semilattice_inf γ] {s t : set γ} :

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 γ} :
is_lub s ais_lub t bis_lub (s t) (a 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 γ} :
is_glb s a₁is_glb t a₂is_glb (s t) (a₁ 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} [decidable_linear_order γ] {a b : γ} {s t : set γ} :
is_least s ais_least t bis_least (s t) (min a 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} [decidable_linear_order γ] {a b : γ} {s t : set γ} :
is_greatest s ais_greatest t bis_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.

Specific sets

Unbounded intervals

theorem is_least_Ici {α : Type u} [preorder α] {a : α} :

theorem is_greatest_Iic {α : Type u} [preorder α] {a : α} :

theorem is_lub_Iic {α : Type u} [preorder α] {a : α} :

theorem is_glb_Ici {α : Type u} [preorder α] {a : α} :

theorem upper_bounds_Iic {α : Type u} [preorder α] {a : α} :

theorem lower_bounds_Ici {α : Type u} [preorder α] {a : α} :

theorem bdd_above_Iic {α : Type u} [preorder α] {a : α} :

theorem bdd_below_Ici {α : Type u} [preorder α] {a : α} :

theorem bdd_above_Iio {α : Type u} [preorder α] {a : α} :

theorem bdd_below_Ioi {α : Type u} [preorder α] {a : α} :

theorem is_lub_Iio {γ : Type w} [linear_order γ] [densely_ordered γ] {a : γ} :

theorem is_glb_Ioi {γ : Type w} [linear_order γ] [densely_ordered γ] {a : γ} :

theorem upper_bounds_Iio {γ : Type w} [linear_order γ] [densely_ordered γ] {a : γ} :

theorem lower_bounds_Ioi {γ : Type w} [linear_order γ] [densely_ordered γ] {a : γ} :

Singleton

theorem is_greatest_singleton {α : Type u} [preorder α] {a : α} :

theorem is_least_singleton {α : Type u} [preorder α] {a : α} :
is_least {a} a

theorem is_lub_singleton {α : Type u} [preorder α] {a : α} :
is_lub {a} a

theorem is_glb_singleton {α : Type u} [preorder α] {a : α} :
is_glb {a} a

theorem bdd_above_singleton {α : Type u} [preorder α] {a : α} :

theorem bdd_below_singleton {α : Type u} [preorder α] {a : α} :

@[simp]
theorem upper_bounds_singleton {α : Type u} [preorder α] {a : α} :

@[simp]
theorem lower_bounds_singleton {α : Type u} [preorder α] {a : α} :

Bounded intervals

theorem bdd_above_Icc {α : Type u} [preorder α] {a b : α} :

theorem bdd_above_Ico {α : Type u} [preorder α] {a b : α} :

theorem bdd_above_Ioc {α : Type u} [preorder α] {a b : α} :

theorem bdd_above_Ioo {α : Type u} [preorder α] {a b : α} :

theorem is_greatest_Icc {α : Type u} [preorder α] {a b : α} :
a bis_greatest (set.Icc a b) b

theorem is_lub_Icc {α : Type u} [preorder α] {a b : α} :
a bis_lub (set.Icc a b) b

theorem upper_bounds_Icc {α : Type u} [preorder α] {a b : α} :
a bupper_bounds (set.Icc a b) = set.Ici b

theorem is_least_Icc {α : Type u} [preorder α] {a b : α} :
a bis_least (set.Icc a b) a

theorem is_glb_Icc {α : Type u} [preorder α] {a b : α} :
a bis_glb (set.Icc a b) a

theorem lower_bounds_Icc {α : Type u} [preorder α] {a b : α} :
a blower_bounds (set.Icc a b) = set.Iic a

theorem is_greatest_Ioc {α : Type u} [preorder α] {a b : α} :
a < bis_greatest (set.Ioc a b) b

theorem is_lub_Ioc {α : Type u} [preorder α] {a b : α} :
a < bis_lub (set.Ioc a b) b

theorem upper_bounds_Ioc {α : Type u} [preorder α] {a b : α} :
a < bupper_bounds (set.Ioc a b) = set.Ici b

theorem is_least_Ico {α : Type u} [preorder α] {a b : α} :
a < bis_least (set.Ico a b) a

theorem is_glb_Ico {α : Type u} [preorder α] {a b : α} :
a < bis_glb (set.Ico a b) a

theorem lower_bounds_Ico {α : Type u} [preorder α] {a b : α} :
a < blower_bounds (set.Ico a b) = set.Iic a

theorem is_glb_Ioo {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} :
a < bis_glb (set.Ioo a b) a

theorem lower_bounds_Ioo {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} :
a < blower_bounds (set.Ioo a b) = set.Iic a

theorem is_glb_Ioc {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} :
a < bis_glb (set.Ioc a b) a

theorem lower_bound_Ioc {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} :
a < blower_bounds (set.Ioc a b) = set.Iic a

theorem is_lub_Ioo {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} :
a < bis_lub (set.Ioo a b) b

theorem upper_bounds_Ioo {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} :
a < bupper_bounds (set.Ioo a b) = set.Ici b

theorem is_lub_Ico {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} :
a < bis_lub (set.Ico a b) b

theorem upper_bounds_Ico {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} :
a < bupper_bounds (set.Ico a b) = set.Ici b

theorem bdd_below_iff_subset_Ici {α : Type u} [preorder α] {s : set α} :
bdd_below s ∃ (a : α), s set.Ici a

theorem bdd_above_iff_subset_Iic {α : Type u} [preorder α] {s : set α} :
bdd_above s ∃ (a : α), s set.Iic a

theorem bdd_below_bdd_above_iff_subset_Icc {α : Type u} [preorder α] {s : set α} :
bdd_below s bdd_above s ∃ (a b : α), s set.Icc a b

Univ

theorem is_greatest_univ {γ : Type w} [order_top γ] :

theorem is_lub_univ {γ : Type w} [order_top γ] :

theorem is_least_univ {γ : Type w} [order_bot γ] :

theorem is_glb_univ {γ : Type w} [order_bot γ] :

Empty set

@[simp]
theorem upper_bounds_empty {α : Type u} [preorder α] :

@[simp]
theorem lower_bounds_empty {α : Type u} [preorder α] :

@[simp]
theorem bdd_above_empty {α : Type u} [preorder α] [nonempty α] :

@[simp]
theorem bdd_below_empty {α : Type u} [preorder α] [nonempty α] :

theorem is_glb_empty {γ : Type w} [order_top γ] :

theorem is_lub_empty {γ : Type w} [order_bot γ] :

theorem is_lub.nonempty {α : Type u} [preorder α] {s : set α} {a : α} [no_bot_order α] :
is_lub s a → s.nonempty

theorem is_glb.nonempty {α : Type u} [preorder α] {s : set α} {a : α} [no_top_order α] :
is_glb s a → s.nonempty

theorem nonempty_of_not_bdd_above {α : Type u} [preorder α] {s : set α} [ha : nonempty α] :

theorem nonempty_of_not_bdd_below {α : Type u} [preorder α] {s : set α} [ha : nonempty α] :

insert

@[simp]
theorem bdd_above_insert {γ : Type w} [semilattice_sup γ] (a : γ) {s : set γ} :

Adding a point to a set preserves its boundedness above.

theorem bdd_above.insert {γ : Type w} [semilattice_sup γ] (a : γ) {s : set γ} :

@[simp]
theorem bdd_below_insert {γ : Type w} [semilattice_inf γ] (a : γ) {s : set γ} :

Adding a point to a set preserves its boundedness below.

theorem bdd_below.insert {γ : Type w} [semilattice_inf γ] (a : γ) {s : set γ} :

theorem is_lub.insert {γ : Type w} [semilattice_sup γ] (a : γ) {b : γ} {s : set γ} :
is_lub s bis_lub (insert a s) (a b)

theorem is_glb.insert {γ : Type w} [semilattice_inf γ] (a : γ) {b : γ} {s : set γ} :
is_glb s bis_glb (insert a s) (a b)

theorem is_greatest.insert {γ : Type w} [decidable_linear_order γ] (a : γ) {b : γ} {s : set γ} :
is_greatest s bis_greatest (insert a s) (max a b)

theorem is_least.insert {γ : Type w} [decidable_linear_order γ] (a : γ) {b : γ} {s : set γ} :
is_least s bis_least (insert a s) (min a b)

@[simp]
theorem upper_bounds_insert {α : Type u} [preorder α] (a : α) (s : set α) :

@[simp]
theorem lower_bounds_insert {α : Type u} [preorder α] (a : α) (s : set α) :

@[simp]
theorem order_top.bdd_above {γ : Type w} [order_top γ] (s : set γ) :

When there is a global maximum, every set is bounded above.

@[simp]
theorem order_bot.bdd_below {γ : Type w} [order_bot γ] (s : set γ) :

When there is a global minimum, every set is bounded below.

Pair

theorem is_lub_pair {γ : Type w} [semilattice_sup γ] {a b : γ} :
is_lub {a, b} (a b)

theorem is_glb_pair {γ : Type w} [semilattice_inf γ] {a b : γ} :
is_glb {a, b} (a b)

theorem is_least_pair {γ : Type w} [decidable_linear_order γ] {a b : γ} :
is_least {a, b} (min a b)

theorem is_greatest_pair {γ : Type w} [decidable_linear_order γ] {a b : γ} :
is_greatest {a, b} (max a b)

(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 : α} :
a lower_bounds sb upper_bounds ss.nonemptya b

theorem is_glb_le_is_lub {α : Type u} [preorder α] {s : set α} {a b : α} :
is_glb s ais_lub s bs.nonemptya b

theorem is_lub_lt_iff {α : Type u} [preorder α] {s : set α} {a b : α} :
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 : α} :
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 : α} :
is_least s ais_least s ba = b

theorem is_least.is_least_iff_eq {α : Type u} [partial_order α] {s : set α} {a b : α} :
is_least s a(is_least s b a = b)

theorem is_greatest.unique {α : Type u} [partial_order α] {s : set α} {a b : α} :
is_greatest s ais_greatest s ba = b

theorem is_greatest.is_greatest_iff_eq {α : Type u} [partial_order α] {s : set α} {a b : α} :
is_greatest s a(is_greatest s b a = b)

theorem is_lub.unique {α : Type u} [partial_order α] {s : set α} {a b : α} :
is_lub s ais_lub s ba = b

theorem is_glb.unique {α : Type u} [partial_order α] {s : set α} {a b : α} :
is_glb s ais_glb s ba = b

theorem lt_is_lub_iff {α : Type u} [linear_order α] {s : set α} {a b : α} :
is_lub s a(b < a ∃ (c : α) (H : c s), b < c)

theorem is_glb_lt_iff {α : Type u} [linear_order α] {s : set α} {a b : α} :
is_glb s a(a < b ∃ (c : α) (H : c s), c < b)

Least upper bound and the greatest lower bound in linear ordered additive commutative groups

theorem is_glb.exists_between_self_add {α : Type u} [decidable_linear_ordered_add_comm_group α] {s : set α} {a ε : α} :
0 < εis_glb s a(∃ (b : α), b s a b b < a + ε)

theorem is_glb.exists_between_self_add' {α : Type u} [decidable_linear_ordered_add_comm_group α] {s : set α} {a ε : α} :
0 < εis_glb s aa s(∃ (b : α), b s a < b b < a + ε)

theorem is_lub.exists_between_sub_self {α : Type u} [decidable_linear_ordered_add_comm_group α] {s : set α} {a ε : α} :
0 < εis_lub s a(∃ (b : α), b s a - ε < b b a)

theorem is_lub.exists_between_sub_self' {α : Type u} [decidable_linear_ordered_add_comm_group α] {s : set α} {a ε : α} :
0 < εis_lub s aa s(∃ (b : α), b s a - ε < b b < a)

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 α} :
a upper_bounds sf a upper_bounds (f '' s)

theorem monotone.mem_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {a : α} {s : set α} :
a lower_bounds sf a lower_bounds (f '' s)

theorem monotone.map_bdd_above {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} :
monotone fbdd_above sbdd_above (f '' s)

The image under a monotone function of a set which is bounded above is bounded above.

theorem monotone.map_bdd_below {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} :
monotone fbdd_below sbdd_below (f '' s)

The image under a monotone function of a set which is bounded below is bounded below.

theorem monotone.map_is_least {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {a : α} {s : set α} :
is_least s ais_least (f '' s) (f a)

A monotone map sends a least element of a set to a least element of its image.

theorem monotone.map_is_greatest {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {a : α} {s : set α} :
is_greatest s ais_greatest (f '' s) (f a)

A monotone map sends a greatest element of a set to a greatest element of its image.

theorem monotone.is_lub_image_le {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {a : α} {s : set α} (Ha : is_lub s a) {b : β} :
is_lub (f '' s) bb f a

theorem monotone.le_is_glb_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {a : α} {s : set α} (Ha : is_glb s a) {b : β} :
is_glb (f '' s) bf a b

theorem is_glb.of_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : ∀ {x y : α}, f x f y x y) {s : set α} {x : α} :
is_glb (f '' s) (f x)is_glb s x

theorem is_lub.of_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : ∀ {x y : α}, f x f y x y) {s : set α} {x : α} :
is_lub (f '' s) (f x)is_lub s x