mathlib docs: order.bounds

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.

source

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.

source

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

source

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

source

theorem upper_bounds_mono_set {α : Type u} [preorder α] ⦃s t : set α⦄ (hst : s ⊆ t) :

upper_bounds t ⊆ upper_bounds s

source

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

lower_bounds t ⊆ lower_bounds s

source

theorem upper_bounds_mono_mem {α : Type u} [preorder α] {s : set α} ⦃a b : α⦄ (hab : a ≤ b) (a_1 : a ∈ upper_bounds s) :

b ∈ upper_bounds s

source

theorem lower_bounds_mono_mem {α : Type u} [preorder α] {s : set α} ⦃a b : α⦄ (hab : a ≤ b) (a_1 : b ∈ lower_bounds s) :

a ∈ lower_bounds s

source

theorem upper_bounds_mono {α : Type u} [preorder α] ⦃s t : set α⦄ (hst : s ⊆ t) ⦃a b : α⦄ (hab : a ≤ b) (a_1 : a ∈ upper_bounds t) :

b ∈ upper_bounds s

source

theorem lower_bounds_mono {α : Type u} [preorder α] ⦃s t : set α⦄ (hst : s ⊆ t) ⦃a b : α⦄ (hab : a ≤ b) (a_1 : b ∈ lower_bounds t) :

a ∈ lower_bounds s

source

theorem bdd_above.mono {α : Type u} [preorder α] ⦃s t : set α⦄ (h : s ⊆ t) (a : bdd_above t) :

bdd_above s

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

source

theorem bdd_below.mono {α : Type u} [preorder α] ⦃s t : set α⦄ (h : s ⊆ t) (a : bdd_below t) :

bdd_below s

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

source

theorem is_lub.of_subset_of_superset {α : Type u} [preorder α] {a : α} {s t p : set α} (hs : is_lub s a) (hp : is_lub p a) (hst : s ⊆ t) (htp : t ⊆ p) :

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

source

theorem is_glb.of_subset_of_superset {α : Type u} [preorder α] {a : α} {s t p : set α} (hs : is_glb s a) (hp : is_glb p a) (hst : s ⊆ t) (htp : t ⊆ p) :

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

source

theorem is_least.mono {α : Type u} [preorder α] {s t : set α} {a b : α} (ha : is_least s a) (hb : is_least t b) (hst : s ⊆ t) :

b ≤ a

source

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

source

theorem is_lub.mono {α : Type u} [preorder α] {s t : set α} {a b : α} (ha : is_lub s a) (hb : is_lub t b) (hst : s ⊆ t) :

a ≤ b

source

theorem is_glb.mono {α : Type u} [preorder α] {s t : set α} {a b : α} (ha : is_glb s a) (hb : is_glb t b) (hst : s ⊆ t) :

b ≤ a

source

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

is_glb s a

source

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

is_lub s a

source

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

upper_bounds s = set.Ici a

source

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

lower_bounds s = set.Iic a

source

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

lower_bounds s = set.Iic a

source

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

upper_bounds s = set.Ici a

source

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

a ≤ b ↔ b ∈ upper_bounds s

source

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

b ≤ a ↔ b ∈ lower_bounds s

source

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

bdd_above s

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

source

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

bdd_below s

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

source

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

bdd_above s

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

source

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

bdd_below s

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

source

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

s.nonempty

source

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

s.nonempty

source

@[simp]

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

upper_bounds (s ∪ t) = upper_bounds s ∩ upper_bounds t

source

@[simp]

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

lower_bounds (s ∪ t) = lower_bounds s ∩ lower_bounds t

source

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

upper_bounds s ∪ upper_bounds t ⊆ upper_bounds (s ∩ t)

source

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

lower_bounds s ∪ lower_bounds t ⊆ lower_bounds (s ∩ t)

source

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

is_least (s ∪ t) a ↔ is_least s a ∧ a ∈ lower_bounds t ∨ a ∈ lower_bounds s ∧ is_least t a

source

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

source

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

bdd_above (s ∩ t)

If s is bounded, then so is s ∩ t

source

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

bdd_above (s ∩ t)

If t is bounded, then so is s ∩ t

source

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

bdd_below (s ∩ t)

If s is bounded, then so is s ∩ t

source

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

bdd_below (s ∩ t)

If t is bounded, then so is s ∩ t

source

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

bdd_above (s ∪ t)

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

source

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

bdd_above (s ∪ t) ↔ bdd_above s ∧ bdd_above t

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

source

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

bdd_below (s ∪ t)

source

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

bdd_below (s ∪ t) ↔ bdd_below s ∧ bdd_below t

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

source

theorem is_lub.union {γ : Type w} [semilattice_sup γ] {a b : γ} {s t : set γ} (hs : is_lub s a) (ht : is_lub t b) :

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

source

theorem is_glb.union {γ : Type w} [semilattice_inf γ] {a₁ a₂ : γ} {s t : set γ} (hs : is_glb s a₁) (ht : 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.

source

theorem is_least.union {γ : Type w} [decidable_linear_order γ] {a b : γ} {s t : set γ} (ha : is_least s a) (hb : is_least t b) :

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

source

theorem is_greatest.union {γ : Type w} [decidable_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.

source

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

is_least (set.Ici a) a

source

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

is_greatest (set.Iic a) a

source

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

is_lub (set.Iic a) a

source

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

is_glb (set.Ici a) a

source

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

upper_bounds (set.Iic a) = set.Ici a

source

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

lower_bounds (set.Ici a) = set.Iic a

source

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

bdd_above (set.Iic a)

source

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

bdd_below (set.Ici a)

source

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

bdd_above (set.Iio a)

source

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

bdd_below (set.Ioi a)

source

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

is_lub (set.Iio a) a

source

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

is_glb (set.Ioi a) a

source

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

upper_bounds (set.Iio a) = set.Ici a

source

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

lower_bounds (set.Ioi a) = set.Iic a

source

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

is_greatest {a} a

source

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

is_least {a} a

source

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

is_lub {a} a

source

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

is_glb {a} a

source

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

bdd_above {a}

source

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

bdd_below {a}

source

@[simp]

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

upper_bounds {a} = set.Ici a

source

@[simp]

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

lower_bounds {a} = set.Iic a

source

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

bdd_above (set.Icc a b)

source

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

bdd_above (set.Ico a b)

source

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

bdd_above (set.Ioc a b)

source

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

bdd_above (set.Ioo a b)

source

theorem is_greatest_Icc {α : Type u} [preorder α] {a b : α} (h : a ≤ b) :

is_greatest (set.Icc a b) b

source

theorem is_lub_Icc {α : Type u} [preorder α] {a b : α} (h : a ≤ b) :

is_lub (set.Icc a b) b

source

theorem upper_bounds_Icc {α : Type u} [preorder α] {a b : α} (h : a ≤ b) :

upper_bounds (set.Icc a b) = set.Ici b

source

theorem is_least_Icc {α : Type u} [preorder α] {a b : α} (h : a ≤ b) :

is_least (set.Icc a b) a

source

theorem is_glb_Icc {α : Type u} [preorder α] {a b : α} (h : a ≤ b) :

is_glb (set.Icc a b) a

source

theorem lower_bounds_Icc {α : Type u} [preorder α] {a b : α} (h : a ≤ b) :

lower_bounds (set.Icc a b) = set.Iic a

source

theorem is_greatest_Ioc {α : Type u} [preorder α] {a b : α} (h : a < b) :

is_greatest (set.Ioc a b) b

source

theorem is_lub_Ioc {α : Type u} [preorder α] {a b : α} (h : a < b) :

is_lub (set.Ioc a b) b

source

theorem upper_bounds_Ioc {α : Type u} [preorder α] {a b : α} (h : a < b) :

upper_bounds (set.Ioc a b) = set.Ici b

source

theorem is_least_Ico {α : Type u} [preorder α] {a b : α} (h : a < b) :

is_least (set.Ico a b) a

source

theorem is_glb_Ico {α : Type u} [preorder α] {a b : α} (h : a < b) :

is_glb (set.Ico a b) a

source

theorem lower_bounds_Ico {α : Type u} [preorder α] {a b : α} (h : a < b) :

lower_bounds (set.Ico a b) = set.Iic a

source

theorem is_glb_Ioo {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} (hab : a < b) :

is_glb (set.Ioo a b) a

source

theorem lower_bounds_Ioo {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} (hab : a < b) :

lower_bounds (set.Ioo a b) = set.Iic a

source

theorem is_glb_Ioc {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} (hab : a < b) :

is_glb (set.Ioc a b) a

source

theorem lower_bound_Ioc {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} (hab : a < b) :

lower_bounds (set.Ioc a b) = set.Iic a

source

theorem is_lub_Ioo {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} (hab : a < b) :

is_lub (set.Ioo a b) b

source

theorem upper_bounds_Ioo {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} (hab : a < b) :

upper_bounds (set.Ioo a b) = set.Ici b

source

theorem is_lub_Ico {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} (hab : a < b) :

is_lub (set.Ico a b) b

source

theorem upper_bounds_Ico {γ : Type w} [linear_order γ] [densely_ordered γ] {a b : γ} (hab : a < b) :

upper_bounds (set.Ico a b) = set.Ici b

source

theorem bdd_below_iff_subset_Ici {α : Type u} [preorder α] {s : set α} :

bdd_below s ↔ ∃ (a : α), s ⊆ set.Ici a

source

theorem bdd_above_iff_subset_Iic {α : Type u} [preorder α] {s : set α} :

bdd_above s ↔ ∃ (a : α), s ⊆ set.Iic a

source

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

source

theorem order_top.upper_bounds_univ {γ : Type w} [order_top γ] :

upper_bounds set.univ = {⊤}

source

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

is_greatest set.univ ⊤

source

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

is_lub set.univ ⊤

source

theorem order_bot.lower_bounds_univ {γ : Type w} [order_bot γ] :

lower_bounds set.univ = {⊥}

source

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

is_least set.univ ⊥

source

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

is_glb set.univ ⊥

source

theorem no_top_order.upper_bounds_univ {α : Type u} [preorder α] [no_top_order α] :

upper_bounds set.univ = ∅

source

theorem no_bot_order.lower_bounds_univ {α : Type u} [preorder α] [no_bot_order α] :

lower_bounds set.univ = ∅

source

@[simp]

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

upper_bounds ∅ = set.univ

source

@[simp]

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

lower_bounds ∅ = set.univ

source

@[simp]

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

bdd_above ∅

source

@[simp]

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

bdd_below ∅

source

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

is_glb ∅ ⊤

source

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

is_lub ∅ ⊥

source

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

s.nonempty

source

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

s.nonempty

source

theorem nonempty_of_not_bdd_above {α : Type u} [preorder α] {s : set α} [ha : nonempty α] (h : ¬bdd_above s) :

s.nonempty

source

theorem nonempty_of_not_bdd_below {α : Type u} [preorder α] {s : set α} [ha : nonempty α] (h : ¬bdd_below s) :

s.nonempty

source

@[simp]

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

bdd_above (insert a s) ↔ bdd_above s

Adding a point to a set preserves its boundedness above.

source

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

bdd_above (insert a s)

source

@[simp]

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

bdd_below (insert a s) ↔ bdd_below s

Adding a point to a set preserves its boundedness below.

source

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

bdd_below (insert a s)

source

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

is_lub (insert a s) (a ⊔ b)

source

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

is_glb (insert a s) (a ⊓ b)

source

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

is_greatest (insert a s) (max a b)

source

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

is_least (insert a s) (min a b)

source

@[simp]

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

upper_bounds (insert a s) = set.Ici a ∩ upper_bounds s

source

@[simp]

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

lower_bounds (insert a s) = set.Iic a ∩ lower_bounds s

source

@[simp]

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

bdd_above s

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

source

@[simp]

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

bdd_below s

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

source

theorem is_lub_pair {γ : Type w} [semilattice_sup γ] {a b : γ} :

is_lub {a, b} (a ⊔ b)

source

theorem is_glb_pair {γ : Type w} [semilattice_inf γ] {a b : γ} :

is_glb {a, b} (a ⊓ b)

source

theorem is_least_pair {γ : Type w} [decidable_linear_order γ] {a b : γ} :

is_least {a, b} (min a b)

source

theorem is_greatest_pair {γ : Type w} [decidable_linear_order γ] {a b : γ} :

is_greatest {a, b} (max a b)

source

theorem lower_bounds_le_upper_bounds {α : Type u} [preorder α] {s : set α} {a b : α} (ha : a ∈ lower_bounds s) (hb : b ∈ upper_bounds s) (a_1 : s.nonempty) :

a ≤ b

source

theorem is_glb_le_is_lub {α : Type u} [preorder α] {s : set α} {a b : α} (ha : is_glb s a) (hb : is_lub s b) (hs : s.nonempty) :

a ≤ b

source

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

source

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

source

theorem is_least.unique {α : Type u} [partial_order α] {s : set α} {a b : α} (Ha : is_least s a) (Hb : is_least s b) :

a = b

source

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

is_least s b ↔ a = b

source

theorem is_greatest.unique {α : Type u} [partial_order α] {s : set α} {a b : α} (Ha : is_greatest s a) (Hb : is_greatest s b) :

a = b

source

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

source

theorem is_lub.unique {α : Type u} [partial_order α] {s : set α} {a b : α} (Ha : is_lub s a) (Hb : is_lub s b) :

a = b

source

theorem is_glb.unique {α : Type u} [partial_order α] {s : set α} {a b : α} (Ha : is_glb s a) (Hb : is_glb s b) :

a = b

source

theorem lt_is_lub_iff {α : Type u} [linear_order α] {s : set α} {a b : α} (h : is_lub s a) :

b < a ↔ ∃ (c : α) (H : c ∈ s), b < c

source

theorem is_glb_lt_iff {α : Type u} [linear_order α] {s : set α} {a b : α} (h : is_glb s a) :

a < b ↔ ∃ (c : α) (H : c ∈ s), c < b

source

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)

source

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)

source

theorem monotone.map_bdd_above {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : monotone f) (a : bdd_above s) :

bdd_above (f '' s)

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

source

theorem monotone.map_bdd_below {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (hf : monotone f) (a : bdd_below s) :

bdd_below (f '' s)

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

source

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

is_least (f '' s) (f a)

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

source

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.

source

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 : β} (Hb : is_lub (f '' s) b) :

b ≤ f a

source

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 : β} (Hb : is_glb (f '' s) b) :

f a ≤ b

source

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

is_glb s x

source

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

is_lub s x

mathlib documentation

Upper / lower bounds

Definitions

Monotonicity

Conversions

Union and intersection

Specific sets

Unbounded intervals

Singleton

Bounded intervals

Univ

Empty set

insert

Pair

(In)equalities with the least upper bound and the greatest lower bound

Images of upper/lower bounds under monotone functions