Upper / lower bounds

In this file we prove various lemmas about upper/lower bounds of a set: monotonicity, behaviour under ∪, ∩, insert, and provide formulas for ∅, univ, and intervals.

theorem mem_upperBounds {α : Type u} [Preorder α] {s : Set α} {a : α} : a ∈ upperBounds s ↔ ∀ x ∈ s, x ≤ a

theorem mem_lowerBounds {α : Type u} [Preorder α] {s : Set α} {a : α} : a ∈ lowerBounds s ↔ ∀ x ∈ s, a ≤ x

theorem mem_upperBounds_iff_subset_Iic {α : Type u} [Preorder α] {s : Set α} {a : α} : a ∈ upperBounds s ↔ s ⊆ Set.Iic a

theorem mem_lowerBounds_iff_subset_Ici {α : Type u} [Preorder α] {s : Set α} {a : α} : a ∈ lowerBounds s ↔ s ⊆ Set.Ici a

theorem bddAbove_def {α : Type u} [Preorder α] {s : Set α} : BddAbove s ↔ ∃ (x : α), ∀ y ∈ s, y ≤ x

theorem bddBelow_def {α : Type u} [Preorder α] {s : Set α} : BddBelow s ↔ ∃ (x : α), ∀ y ∈ s, x ≤ y

theorem bot_mem_lowerBounds {α : Type u} [Preorder α] [OrderBot α] (s : Set α) : ⊥ ∈ lowerBounds s

theorem top_mem_upperBounds {α : Type u} [Preorder α] [OrderTop α] (s : Set α) : ⊤ ∈ upperBounds s

@[simp]

theorem isLeast_bot_iff {α : Type u} [Preorder α] {s : Set α} [OrderBot α] : IsLeast s ⊥ ↔ ⊥ ∈ s

@[simp]

theorem isGreatest_top_iff {α : Type u} [Preorder α] {s : Set α} [OrderTop α] : IsGreatest s ⊤ ↔ ⊤ ∈ s

theorem not_bddAbove_iff' {α : Type u} [Preorder α] {s : Set α} : ¬BddAbove s ↔ ∀ (x : α), ∃ 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_bddAbove_iff.

theorem not_bddBelow_iff' {α : Type u} [Preorder α] {s : Set α} : ¬BddBelow s ↔ ∀ (x : α), ∃ 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_bddBelow_iff.

theorem not_bddAbove_iff {α : Type u_1} [LinearOrder α] {s : Set α} : ¬BddAbove s ↔ ∀ (x : α), ∃ 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_bddAbove_iff'.

theorem not_bddBelow_iff {α : Type u_1} [LinearOrder α] {s : Set α} : ¬BddBelow s ↔ ∀ (x : α), ∃ 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_bddBelow_iff'.

@[simp]

theorem bddBelow_preimage_ofDual {α : Type u} [Preorder α] {s : Set α} : BddBelow (⇑OrderDual.ofDual ⁻¹' s) ↔ BddAbove s

@[simp]

theorem bddAbove_preimage_ofDual {α : Type u} [Preorder α] {s : Set α} : BddAbove (⇑OrderDual.ofDual ⁻¹' s) ↔ BddBelow s

@[simp]

theorem bddBelow_preimage_toDual {α : Type u} [Preorder α] {s : Set αᵒᵈ} : BddBelow (⇑OrderDual.toDual ⁻¹' s) ↔ BddAbove s

@[simp]

theorem bddAbove_preimage_toDual {α : Type u} [Preorder α] {s : Set αᵒᵈ} : BddAbove (⇑OrderDual.toDual ⁻¹' s) ↔ BddBelow s

theorem BddAbove.dual {α : Type u} [Preorder α] {s : Set α} (h : BddAbove s) : BddBelow (⇑OrderDual.ofDual ⁻¹' s)

theorem BddBelow.dual {α : Type u} [Preorder α] {s : Set α} (h : BddBelow s) : BddAbove (⇑OrderDual.ofDual ⁻¹' s)

theorem IsLeast.dual {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : IsGreatest (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)

theorem IsGreatest.dual {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : IsLeast (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)

theorem IsLUB.dual {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) : IsGLB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)

theorem IsGLB.dual {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) : IsLUB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)

@[reducible, inline]

abbrev IsLeast.orderBot {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : OrderBot ↑s

If a is the least element of a set s, then subtype s is an order with bottom element.

Equations

• h.orderBot = OrderBot.mk ⋯

@[reducible, inline]

abbrev IsGreatest.orderTop {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : OrderTop ↑s

If a is the greatest element of a set s, then subtype s is an order with top element.

Equations

• h.orderTop = OrderTop.mk ⋯

Monotonicity

theorem upperBounds_mono_set {α : Type u} [Preorder α] ⦃s : Set α⦄ ⦃t : Set α⦄ (hst : s ⊆ t) : upperBounds t ⊆ upperBounds s

theorem lowerBounds_mono_set {α : Type u} [Preorder α] ⦃s : Set α⦄ ⦃t : Set α⦄ (hst : s ⊆ t) : lowerBounds t ⊆ lowerBounds s

theorem upperBounds_mono_mem {α : Type u} [Preorder α] {s : Set α} ⦃a : α⦄ ⦃b : α⦄ (hab : a ≤ b) : a ∈ upperBounds s → b ∈ upperBounds s

theorem lowerBounds_mono_mem {α : Type u} [Preorder α] {s : Set α} ⦃a : α⦄ ⦃b : α⦄ (hab : a ≤ b) : b ∈ lowerBounds s → a ∈ lowerBounds s

theorem upperBounds_mono {α : Type u} [Preorder α] ⦃s : Set α⦄ ⦃t : Set α⦄ (hst : s ⊆ t) ⦃a : α⦄ ⦃b : α⦄ (hab : a ≤ b) : a ∈ upperBounds t → b ∈ upperBounds s

theorem lowerBounds_mono {α : Type u} [Preorder α] ⦃s : Set α⦄ ⦃t : Set α⦄ (hst : s ⊆ t) ⦃a : α⦄ ⦃b : α⦄ (hab : a ≤ b) : b ∈ lowerBounds t → a ∈ lowerBounds s

theorem BddAbove.mono {α : Type u} [Preorder α] ⦃s : Set α⦄ ⦃t : Set α⦄ (h : s ⊆ t) : BddAbove t → BddAbove s

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

theorem BddBelow.mono {α : Type u} [Preorder α] ⦃s : Set α⦄ ⦃t : Set α⦄ (h : s ⊆ t) : BddBelow t → BddBelow s

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

theorem IsLUB.of_subset_of_superset {α : Type u} [Preorder α] {a : α} {s : Set α} {t : Set α} {p : Set α} (hs : IsLUB s a) (hp : IsLUB p a) (hst : s ⊆ t) (htp : t ⊆ p) : IsLUB 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 IsGLB.of_subset_of_superset {α : Type u} [Preorder α] {a : α} {s : Set α} {t : Set α} {p : Set α} (hs : IsGLB s a) (hp : IsGLB p a) (hst : s ⊆ t) (htp : t ⊆ p) : IsGLB 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 IsLeast.mono {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} {b : α} (ha : IsLeast s a) (hb : IsLeast t b) (hst : s ⊆ t) : b ≤ a

theorem IsGreatest.mono {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} {b : α} (ha : IsGreatest s a) (hb : IsGreatest t b) (hst : s ⊆ t) : a ≤ b

theorem IsLUB.mono {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} {b : α} (ha : IsLUB s a) (hb : IsLUB t b) (hst : s ⊆ t) : a ≤ b

theorem IsGLB.mono {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} {b : α} (ha : IsGLB s a) (hb : IsGLB t b) (hst : s ⊆ t) : b ≤ a

theorem subset_lowerBounds_upperBounds {α : Type u} [Preorder α] (s : Set α) : s ⊆ lowerBounds (upperBounds s)

theorem subset_upperBounds_lowerBounds {α : Type u} [Preorder α] (s : Set α) : s ⊆ upperBounds (lowerBounds s)

theorem Set.Nonempty.bddAbove_lowerBounds {α : Type u} [Preorder α] {s : Set α} (hs : s.Nonempty) : BddAbove (lowerBounds s)

theorem Set.Nonempty.bddBelow_upperBounds {α : Type u} [Preorder α] {s : Set α} (hs : s.Nonempty) : BddBelow (upperBounds s)

Conversions

theorem IsLeast.isGLB {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : IsGLB s a

theorem IsGreatest.isLUB {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : IsLUB s a

theorem IsLUB.upperBounds_eq {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) : upperBounds s = Set.Ici a

theorem IsGLB.lowerBounds_eq {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) : lowerBounds s = Set.Iic a

theorem IsLeast.lowerBounds_eq {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : lowerBounds s = Set.Iic a

theorem IsGreatest.upperBounds_eq {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : upperBounds s = Set.Ici a

theorem IsGreatest.lt_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (h : IsGreatest s a) : a < b ↔ ∀ x ∈ s, x < b

theorem IsLeast.lt_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (h : IsLeast s a) : b < a ↔ ∀ x ∈ s, b < x

theorem isLUB_le_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) : a ≤ b ↔ b ∈ upperBounds s

theorem le_isGLB_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) : b ≤ a ↔ b ∈ lowerBounds s

theorem isLUB_iff_le_iff {α : Type u} [Preorder α] {s : Set α} {a : α} : IsLUB s a ↔ ∀ (b : α), a ≤ b ↔ b ∈ upperBounds s

theorem isGLB_iff_le_iff {α : Type u} [Preorder α] {s : Set α} {a : α} : IsGLB s a ↔ ∀ (b : α), b ≤ a ↔ b ∈ lowerBounds s

theorem IsLUB.bddAbove {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) : BddAbove s

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

theorem IsGLB.bddBelow {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) : BddBelow s

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

theorem IsGreatest.bddAbove {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : BddAbove s

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

theorem IsLeast.bddBelow {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : BddBelow s

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

theorem IsLeast.nonempty {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : s.Nonempty

theorem IsGreatest.nonempty {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : s.Nonempty

Union and intersection

@[simp]

theorem upperBounds_union {α : Type u} [Preorder α] {s : Set α} {t : Set α} : upperBounds (s ∪ t) = upperBounds s ∩ upperBounds t

@[simp]

theorem lowerBounds_union {α : Type u} [Preorder α] {s : Set α} {t : Set α} : lowerBounds (s ∪ t) = lowerBounds s ∩ lowerBounds t

theorem union_upperBounds_subset_upperBounds_inter {α : Type u} [Preorder α] {s : Set α} {t : Set α} : upperBounds s ∪ upperBounds t ⊆ upperBounds (s ∩ t)

theorem union_lowerBounds_subset_lowerBounds_inter {α : Type u} [Preorder α] {s : Set α} {t : Set α} : lowerBounds s ∪ lowerBounds t ⊆ lowerBounds (s ∩ t)

theorem isLeast_union_iff {α : Type u} [Preorder α] {a : α} {s : Set α} {t : Set α} : IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a

theorem isGreatest_union_iff {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} : IsGreatest (s ∪ t) a ↔ IsGreatest s a ∧ a ∈ upperBounds t ∨ a ∈ upperBounds s ∧ IsGreatest t a

theorem BddAbove.inter_of_left {α : Type u} [Preorder α] {s : Set α} {t : Set α} (h : BddAbove s) : BddAbove (s ∩ t)

If s is bounded, then so is s ∩ t

theorem BddAbove.inter_of_right {α : Type u} [Preorder α] {s : Set α} {t : Set α} (h : BddAbove t) : BddAbove (s ∩ t)

If t is bounded, then so is s ∩ t

theorem BddBelow.inter_of_left {α : Type u} [Preorder α] {s : Set α} {t : Set α} (h : BddBelow s) : BddBelow (s ∩ t)

If s is bounded, then so is s ∩ t

theorem BddBelow.inter_of_right {α : Type u} [Preorder α] {s : Set α} {t : Set α} (h : BddBelow t) : BddBelow (s ∩ t)

If t is bounded, then so is s ∩ t

theorem BddAbove.union {α : Type u} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} {t : Set α} : BddAbove s → BddAbove t → BddAbove (s ∪ t)

In a directed order, the union of bounded above sets is bounded above.

theorem bddAbove_union {α : Type u} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} {t : Set α} : BddAbove (s ∪ t) ↔ BddAbove s ∧ BddAbove t

In a directed order, the union of two sets is bounded above if and only if both sets are.

theorem BddBelow.union {α : Type u} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {s : Set α} {t : Set α} : BddBelow s → BddBelow t → BddBelow (s ∪ t)

In a codirected order, the union of bounded below sets is bounded below.

theorem bddBelow_union {α : Type u} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {s : Set α} {t : Set α} : BddBelow (s ∪ t) ↔ BddBelow s ∧ BddBelow t

In a codirected order, the union of two sets is bounded below if and only if both sets are.

theorem IsLUB.union {γ : Type w} [SemilatticeSup γ] {a : γ} {b : γ} {s : Set γ} {t : Set γ} (hs : IsLUB s a) (ht : IsLUB t b) : IsLUB (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 IsGLB.union {γ : Type w} [SemilatticeInf γ] {a₁ : γ} {a₂ : γ} {s : Set γ} {t : Set γ} (hs : IsGLB s a₁) (ht : IsGLB t a₂) : IsGLB (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 IsLeast.union {γ : Type w} [LinearOrder γ] {a : γ} {b : γ} {s : Set γ} {t : Set γ} (ha : IsLeast s a) (hb : IsLeast t b) : IsLeast (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 IsGreatest.union {γ : Type w} [LinearOrder γ] {a : γ} {b : γ} {s : Set γ} {t : Set γ} (ha : IsGreatest s a) (hb : IsGreatest t b) : IsGreatest (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 IsLUB.inter_Ici_of_mem {γ : Type w} [LinearOrder γ] {s : Set γ} {a : γ} {b : γ} (ha : IsLUB s a) (hb : b ∈ s) : IsLUB (s ∩ Set.Ici b) a

theorem IsGLB.inter_Iic_of_mem {γ : Type w} [LinearOrder γ] {s : Set γ} {a : γ} {b : γ} (ha : IsGLB s a) (hb : b ∈ s) : IsGLB (s ∩ Set.Iic b) a

theorem bddAbove_iff_exists_ge {γ : Type w} [SemilatticeSup γ] {s : Set γ} (x₀ : γ) : BddAbove s ↔ ∃ (x : γ), x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x

theorem bddBelow_iff_exists_le {γ : Type w} [SemilatticeInf γ] {s : Set γ} (x₀ : γ) : BddBelow s ↔ ∃ x ≤ x₀, ∀ y ∈ s, x ≤ y

theorem BddAbove.exists_ge {γ : Type w} [SemilatticeSup γ] {s : Set γ} (hs : BddAbove s) (x₀ : γ) : ∃ (x : γ), x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x

theorem BddBelow.exists_le {γ : Type w} [SemilatticeInf γ] {s : Set γ} (hs : BddBelow s) (x₀ : γ) : ∃ x ≤ x₀, ∀ y ∈ s, x ≤ y

Specific sets

Unbounded intervals

theorem isLeast_Ici {α : Type u} [Preorder α] {a : α} : IsLeast (Set.Ici a) a

theorem isGreatest_Iic {α : Type u} [Preorder α] {a : α} : IsGreatest (Set.Iic a) a

theorem isLUB_Iic {α : Type u} [Preorder α] {a : α} : IsLUB (Set.Iic a) a

theorem isGLB_Ici {α : Type u} [Preorder α] {a : α} : IsGLB (Set.Ici a) a

theorem upperBounds_Iic {α : Type u} [Preorder α] {a : α} : upperBounds (Set.Iic a) = Set.Ici a

theorem lowerBounds_Ici {α : Type u} [Preorder α] {a : α} : lowerBounds (Set.Ici a) = Set.Iic a

theorem bddAbove_Iic {α : Type u} [Preorder α] {a : α} : BddAbove (Set.Iic a)

theorem bddBelow_Ici {α : Type u} [Preorder α] {a : α} : BddBelow (Set.Ici a)

theorem bddAbove_Iio {α : Type u} [Preorder α] {a : α} : BddAbove (Set.Iio a)

theorem bddBelow_Ioi {α : Type u} [Preorder α] {a : α} : BddBelow (Set.Ioi a)

theorem lub_Iio_le {α : Type u} [Preorder α] {b : α} (a : α) (hb : IsLUB (Set.Iio a) b) : b ≤ a

theorem le_glb_Ioi {α : Type u} [Preorder α] {b : α} (a : α) (hb : IsGLB (Set.Ioi a) b) : a ≤ b

theorem lub_Iio_eq_self_or_Iio_eq_Iic {γ : Type w} [PartialOrder γ] {j : γ} (i : γ) (hj : IsLUB (Set.Iio i) j) : j = i ∨ Set.Iio i = Set.Iic j

theorem glb_Ioi_eq_self_or_Ioi_eq_Ici {γ : Type w} [PartialOrder γ] {j : γ} (i : γ) (hj : IsGLB (Set.Ioi i) j) : j = i ∨ Set.Ioi i = Set.Ici j

theorem exists_lub_Iio {γ : Type w} [LinearOrder γ] (i : γ) : ∃ (j : γ), IsLUB (Set.Iio i) j

theorem exists_glb_Ioi {γ : Type w} [LinearOrder γ] (i : γ) : ∃ (j : γ), IsGLB (Set.Ioi i) j

theorem isLUB_Iio {γ : Type w} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : IsLUB (Set.Iio a) a

theorem isGLB_Ioi {γ : Type w} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : IsGLB (Set.Ioi a) a

theorem upperBounds_Iio {γ : Type w} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : upperBounds (Set.Iio a) = Set.Ici a

theorem lowerBounds_Ioi {γ : Type w} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : lowerBounds (Set.Ioi a) = Set.Iic a

Singleton

@[simp]

theorem isGreatest_singleton {α : Type u} [Preorder α] {a : α} : IsGreatest {a} a

@[simp]

theorem isLeast_singleton {α : Type u} [Preorder α] {a : α} : IsLeast {a} a

@[simp]

theorem isLUB_singleton {α : Type u} [Preorder α] {a : α} : IsLUB {a} a

@[simp]

theorem isGLB_singleton {α : Type u} [Preorder α] {a : α} : IsGLB {a} a

@[simp]

theorem bddAbove_singleton {α : Type u} [Preorder α] {a : α} : BddAbove {a}

@[simp]

theorem bddBelow_singleton {α : Type u} [Preorder α] {a : α} : BddBelow {a}

@[simp]

theorem upperBounds_singleton {α : Type u} [Preorder α] {a : α} : upperBounds {a} = Set.Ici a

@[simp]

theorem lowerBounds_singleton {α : Type u} [Preorder α] {a : α} : lowerBounds {a} = Set.Iic a

Bounded intervals

theorem bddAbove_Icc {α : Type u} [Preorder α] {a : α} {b : α} : BddAbove (Set.Icc a b)

theorem bddBelow_Icc {α : Type u} [Preorder α] {a : α} {b : α} : BddBelow (Set.Icc a b)

theorem bddAbove_Ico {α : Type u} [Preorder α] {a : α} {b : α} : BddAbove (Set.Ico a b)

theorem bddBelow_Ico {α : Type u} [Preorder α] {a : α} {b : α} : BddBelow (Set.Ico a b)

theorem bddAbove_Ioc {α : Type u} [Preorder α] {a : α} {b : α} : BddAbove (Set.Ioc a b)

theorem bddBelow_Ioc {α : Type u} [Preorder α] {a : α} {b : α} : BddBelow (Set.Ioc a b)

theorem bddAbove_Ioo {α : Type u} [Preorder α] {a : α} {b : α} : BddAbove (Set.Ioo a b)

theorem bddBelow_Ioo {α : Type u} [Preorder α] {a : α} {b : α} : BddBelow (Set.Ioo a b)

theorem isGreatest_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a ≤ b) : IsGreatest (Set.Icc a b) b

theorem isLUB_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a ≤ b) : IsLUB (Set.Icc a b) b

theorem upperBounds_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a ≤ b) : upperBounds (Set.Icc a b) = Set.Ici b

theorem isLeast_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a ≤ b) : IsLeast (Set.Icc a b) a

theorem isGLB_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a ≤ b) : IsGLB (Set.Icc a b) a

theorem lowerBounds_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a ≤ b) : lowerBounds (Set.Icc a b) = Set.Iic a

theorem isGreatest_Ioc {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : IsGreatest (Set.Ioc a b) b

theorem isLUB_Ioc {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : IsLUB (Set.Ioc a b) b

theorem upperBounds_Ioc {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : upperBounds (Set.Ioc a b) = Set.Ici b

theorem isLeast_Ico {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : IsLeast (Set.Ico a b) a

theorem isGLB_Ico {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : IsGLB (Set.Ico a b) a

theorem lowerBounds_Ico {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : lowerBounds (Set.Ico a b) = Set.Iic a

theorem isGLB_Ioo {γ : Type w} [SemilatticeSup γ] [DenselyOrdered γ] {a : γ} {b : γ} (h : a < b) : IsGLB (Set.Ioo a b) a

theorem lowerBounds_Ioo {γ : Type w} [SemilatticeSup γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) : lowerBounds (Set.Ioo a b) = Set.Iic a

theorem isGLB_Ioc {γ : Type w} [SemilatticeSup γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) : IsGLB (Set.Ioc a b) a

theorem lowerBounds_Ioc {γ : Type w} [SemilatticeSup γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) : lowerBounds (Set.Ioc a b) = Set.Iic a

theorem isLUB_Ioo {γ : Type w} [SemilatticeInf γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) : IsLUB (Set.Ioo a b) b

theorem upperBounds_Ioo {γ : Type w} [SemilatticeInf γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) : upperBounds (Set.Ioo a b) = Set.Ici b

theorem isLUB_Ico {γ : Type w} [SemilatticeInf γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) : IsLUB (Set.Ico a b) b

theorem upperBounds_Ico {γ : Type w} [SemilatticeInf γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) : upperBounds (Set.Ico a b) = Set.Ici b

theorem bddBelow_iff_subset_Ici {α : Type u} [Preorder α] {s : Set α} : BddBelow s ↔ ∃ (a : α), s ⊆ Set.Ici a

theorem bddAbove_iff_subset_Iic {α : Type u} [Preorder α] {s : Set α} : BddAbove s ↔ ∃ (a : α), s ⊆ Set.Iic a

theorem bddBelow_bddAbove_iff_subset_Icc {α : Type u} [Preorder α] {s : Set α} : BddBelow s ∧ BddAbove s ↔ ∃ (a : α) (b : α), s ⊆ Set.Icc a b

Univ

@[simp]

theorem isGreatest_univ_iff {α : Type u} [Preorder α] {a : α} : IsGreatest Set.univ a ↔ IsTop a

theorem isGreatest_univ {α : Type u} [Preorder α] [OrderTop α] : IsGreatest Set.univ ⊤

@[simp]

theorem OrderTop.upperBounds_univ {γ : Type w} [PartialOrder γ] [OrderTop γ] : upperBounds Set.univ = {⊤}

theorem isLUB_univ {α : Type u} [Preorder α] [OrderTop α] : IsLUB Set.univ ⊤

@[simp]

theorem OrderBot.lowerBounds_univ {γ : Type w} [PartialOrder γ] [OrderBot γ] : lowerBounds Set.univ = {⊥}

@[simp]

theorem isLeast_univ_iff {α : Type u} [Preorder α] {a : α} : IsLeast Set.univ a ↔ IsBot a

theorem isLeast_univ {α : Type u} [Preorder α] [OrderBot α] : IsLeast Set.univ ⊥

theorem isGLB_univ {α : Type u} [Preorder α] [OrderBot α] : IsGLB Set.univ ⊥

@[simp]

theorem NoMaxOrder.upperBounds_univ {α : Type u} [Preorder α] [NoMaxOrder α] : upperBounds Set.univ = ∅

@[simp]

theorem NoMinOrder.lowerBounds_univ {α : Type u} [Preorder α] [NoMinOrder α] : lowerBounds Set.univ = ∅

@[simp]

theorem not_bddAbove_univ {α : Type u} [Preorder α] [NoMaxOrder α] : ¬BddAbove Set.univ

@[simp]

theorem not_bddBelow_univ {α : Type u} [Preorder α] [NoMinOrder α] : ¬BddBelow Set.univ

Empty set

@[simp]

theorem upperBounds_empty {α : Type u} [Preorder α] : upperBounds ∅ = Set.univ

@[simp]

theorem lowerBounds_empty {α : Type u} [Preorder α] : lowerBounds ∅ = Set.univ

@[simp]

theorem bddAbove_empty {α : Type u} [Preorder α] [Nonempty α] : BddAbove ∅

@[simp]

theorem bddBelow_empty {α : Type u} [Preorder α] [Nonempty α] : BddBelow ∅

@[simp]

theorem isGLB_empty_iff {α : Type u} [Preorder α] {a : α} : IsGLB ∅ a ↔ IsTop a

@[simp]

theorem isLUB_empty_iff {α : Type u} [Preorder α] {a : α} : IsLUB ∅ a ↔ IsBot a

theorem isGLB_empty {α : Type u} [Preorder α] [OrderTop α] : IsGLB ∅ ⊤

theorem isLUB_empty {α : Type u} [Preorder α] [OrderBot α] : IsLUB ∅ ⊥

theorem IsLUB.nonempty {α : Type u} [Preorder α] {s : Set α} {a : α} [NoMinOrder α] (hs : IsLUB s a) : s.Nonempty

theorem IsGLB.nonempty {α : Type u} [Preorder α] {s : Set α} {a : α} [NoMaxOrder α] (hs : IsGLB s a) : s.Nonempty

theorem nonempty_of_not_bddAbove {α : Type u} [Preorder α] {s : Set α} [ha : Nonempty α] (h : ¬BddAbove s) : s.Nonempty

theorem nonempty_of_not_bddBelow {α : Type u} [Preorder α] {s : Set α} [Nonempty α] (h : ¬BddBelow s) : s.Nonempty

insert

@[simp]

theorem bddAbove_insert {α : Type u} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} {a : α} : BddAbove (insert a s) ↔ BddAbove s

Adding a point to a set preserves its boundedness above.

theorem BddAbove.insert {α : Type u} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} (a : α) : BddAbove s → BddAbove (insert a s)

@[simp]

theorem bddBelow_insert {α : Type u} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {s : Set α} {a : α} : BddBelow (insert a s) ↔ BddBelow s

Adding a point to a set preserves its boundedness below.

theorem BddBelow.insert {α : Type u} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {s : Set α} (a : α) : BddBelow s → BddBelow (insert a s)

theorem IsLUB.insert {γ : Type w} [SemilatticeSup γ] (a : γ) {b : γ} {s : Set γ} (hs : IsLUB s b) : IsLUB (insert a s) (a ⊔ b)

theorem IsGLB.insert {γ : Type w} [SemilatticeInf γ] (a : γ) {b : γ} {s : Set γ} (hs : IsGLB s b) : IsGLB (insert a s) (a ⊓ b)

theorem IsGreatest.insert {γ : Type w} [LinearOrder γ] (a : γ) {b : γ} {s : Set γ} (hs : IsGreatest s b) : IsGreatest (insert a s) (max a b)

theorem IsLeast.insert {γ : Type w} [LinearOrder γ] (a : γ) {b : γ} {s : Set γ} (hs : IsLeast s b) : IsLeast (insert a s) (min a b)

@[simp]

theorem upperBounds_insert {α : Type u} [Preorder α] (a : α) (s : Set α) : upperBounds (insert a s) = Set.Ici a ∩ upperBounds s

@[simp]

theorem lowerBounds_insert {α : Type u} [Preorder α] (a : α) (s : Set α) : lowerBounds (insert a s) = Set.Iic a ∩ lowerBounds s

@[simp]

theorem OrderTop.bddAbove {α : Type u} [Preorder α] [OrderTop α] (s : Set α) : BddAbove s

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

@[simp]

theorem OrderBot.bddBelow {α : Type u} [Preorder α] [OrderBot α] (s : Set α) : BddBelow s

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

def tacticBddDefault : Lean.ParserDescr

Sets are automatically bounded or cobounded in complete lattices. To use the same statements in complete and conditionally complete lattices but let automation fill automatically the boundedness proofs in complete lattices, we use the tactic bddDefault in the statements, in the form (hA : BddAbove A := by bddDefault).

Equations

• tacticBddDefault = Lean.ParserDescr.node `tacticBddDefault 1024 (Lean.ParserDescr.nonReservedSymbol "bddDefault" false)

Pair

theorem isLUB_pair {γ : Type w} [SemilatticeSup γ] {a : γ} {b : γ} : IsLUB {a, b} (a ⊔ b)

theorem isGLB_pair {γ : Type w} [SemilatticeInf γ] {a : γ} {b : γ} : IsGLB {a, b} (a ⊓ b)

theorem isLeast_pair {γ : Type w} [LinearOrder γ] {a : γ} {b : γ} : IsLeast {a, b} (min a b)

theorem isGreatest_pair {γ : Type w} [LinearOrder γ] {a : γ} {b : γ} : IsGreatest {a, b} (max a b)

Lower/upper bounds

@[simp]

theorem isLUB_lowerBounds {α : Type u} [Preorder α] {s : Set α} {a : α} : IsLUB (lowerBounds s) a ↔ IsGLB s a

@[simp]

theorem isGLB_upperBounds {α : Type u} [Preorder α] {s : Set α} {a : α} : IsGLB (upperBounds s) a ↔ IsLUB s a

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

theorem lowerBounds_le_upperBounds {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds s) : s.Nonempty → a ≤ b

theorem isGLB_le_isLUB {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (ha : IsGLB s a) (hb : IsLUB s b) (hs : s.Nonempty) : a ≤ b

theorem isLUB_lt_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (ha : IsLUB s a) : a < b ↔ ∃ c ∈ upperBounds s, c < b

theorem lt_isGLB_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (ha : IsGLB s a) : b < a ↔ ∃ c ∈ lowerBounds s, b < c

theorem le_of_isLUB_le_isGLB {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} {x : α} {y : α} (ha : IsGLB s a) (hb : IsLUB s b) (hab : b ≤ a) (hx : x ∈ s) (hy : y ∈ s) : x ≤ y

theorem IsLeast.unique {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsLeast s a) (Hb : IsLeast s b) : a = b

theorem IsLeast.isLeast_iff_eq {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsLeast s a) : IsLeast s b ↔ a = b

theorem IsGreatest.unique {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGreatest s a) (Hb : IsGreatest s b) : a = b

theorem IsGreatest.isGreatest_iff_eq {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGreatest s a) : IsGreatest s b ↔ a = b

theorem IsLUB.unique {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsLUB s a) (Hb : IsLUB s b) : a = b

theorem IsGLB.unique {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGLB s a) (Hb : IsGLB s b) : a = b

theorem Set.subsingleton_of_isLUB_le_isGLB {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGLB s a) (Hb : IsLUB s b) (hab : b ≤ a) : s.Subsingleton

theorem isGLB_lt_isLUB_of_ne {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGLB s a) (Hb : IsLUB s b) {x : α} {y : α} (Hx : x ∈ s) (Hy : y ∈ s) (Hxy : x ≠ y) : a < b

theorem lt_isLUB_iff {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) : b < a ↔ ∃ c ∈ s, b < c

theorem isGLB_lt_iff {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) : a < b ↔ ∃ c ∈ s, c < b

theorem IsLUB.exists_between {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) (hb : b < a) : ∃ c ∈ s, b < c ∧ c ≤ a

theorem IsLUB.exists_between' {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) (h' : a ∉ s) (hb : b < a) : ∃ c ∈ s, b < c ∧ c < a

theorem IsGLB.exists_between {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) (hb : a < b) : ∃ c ∈ s, a ≤ c ∧ c < b

theorem IsGLB.exists_between' {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) (h' : a ∉ s) (hb : a < b) : ∃ c ∈ s, a < c ∧ c < b