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_1} [Preorder α] {s : Set α} {a : α} : a ∈ upperBounds s ↔ ∀ x ∈ s, x ≤ a

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

theorem not_bddAbove_iff' {α : Type u_1} [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_1} [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_4} [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_4} [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_1} [Preorder α] {s : Set α} : BddBelow (⇑OrderDual.ofDual ⁻¹' s) ↔ BddAbove s

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[reducible, inline]

abbrev IsLeast.orderBot {α : Type u_1} [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 = { bot := ⟨a, ⋯⟩, bot_le := ⋯ }

@[reducible, inline]

abbrev IsGreatest.orderTop {α : Type u_1} [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 = { top := ⟨a, ⋯⟩, le_top := ⋯ }

theorem isLUB_congr {α : Type u_1} [Preorder α] {s t : Set α} {a : α} (h : upperBounds s = upperBounds t) : IsLUB s a ↔ IsLUB t a

theorem isGLB_congr {α : Type u_1} [Preorder α] {s t : Set α} {a : α} (h : lowerBounds s = lowerBounds t) : IsGLB s a ↔ IsGLB t a

@[simp]

theorem IsCofinalFor.of_subset {α : Type u_1} [Preorder α] {s t : Set α} (hst : s ⊆ t) : IsCofinalFor s t

@[simp]

theorem IsCoinitialFor.of_subset {α : Type u_1} [Preorder α] {s t : Set α} (hst : s ⊆ t) : IsCoinitialFor s t

theorem HasSubset.Subset.iscofinalfor {α : Type u_1} [Preorder α] {s t : Set α} (hst : s ⊆ t) : IsCofinalFor s t

Alias of IsCofinalFor.of_subset.

theorem HasSubset.Subset.iscoinitialfor {α : Type u_1} [Preorder α] {s t : Set α} (hst : s ⊆ t) : IsCoinitialFor s t

Alias of IsCoinitialFor.of_subset.

theorem IsCofinalFor.rfl {α : Type u_1} [Preorder α] {s : Set α} : IsCofinalFor s s

theorem IsCoinitialFor.rfl {α : Type u_1} [Preorder α] {s : Set α} : IsCoinitialFor s s

theorem IsCofinalFor.trans {α : Type u_1} [Preorder α] {s t u : Set α} (hst : IsCofinalFor s t) (htu : IsCofinalFor t u) : IsCofinalFor s u

theorem IsCoinitialFor.trans {α : Type u_1} [Preorder α] {s t u : Set α} (hst : IsCoinitialFor s t) (htu : IsCoinitialFor t u) : IsCoinitialFor s u

theorem IsCofinalFor.mono_left {α : Type u_1} [Preorder α] {s t u : Set α} (hst : s ⊆ t) (htu : IsCofinalFor t u) : IsCofinalFor s u

theorem IsCoinitialFor.mono_left {α : Type u_1} [Preorder α] {s t u : Set α} (hst : s ⊆ t) (htu : IsCoinitialFor t u) : IsCoinitialFor s u

theorem IsCofinalFor.mono_right {α : Type u_1} [Preorder α] {s t u : Set α} (htu : t ⊆ u) (hst : IsCofinalFor s t) : IsCofinalFor s u

theorem IsCoinitialFor.mono_right {α : Type u_1} [Preorder α] {s t u : Set α} (htu : t ⊆ u) (hst : IsCoinitialFor s t) : IsCoinitialFor s u

theorem DirectedOn.isCofinalFor_fst_image_prod_snd_image {α : Type u_1} [Preorder α] {β : Type u_4} [Preorder β] {s : Set (α × β)} (hs : DirectedOn (fun (x1 x2 : α × β) => x1 ≤ x2) s) : IsCofinalFor ((Prod.fst '' s) ×ˢ (Prod.snd '' s)) s

Monotonicity

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

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

theorem upperBounds_mono_of_isCofinalFor {α : Type u_1} [Preorder α] {s t : Set α} (hst : IsCofinalFor s t) : upperBounds t ⊆ upperBounds s

theorem lowerBounds_mono_of_isCoinitialFor {α : Type u_1} [Preorder α] {s t : Set α} (hst : IsCoinitialFor s t) : lowerBounds t ⊆ lowerBounds s

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

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

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

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

theorem BddAbove.mono {α : Type u_1} [Preorder α] ⦃s 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_1} [Preorder α] ⦃s 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_1} [Preorder α] {a : α} {s t 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_1} [Preorder α] {a : α} {s t 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_1} [Preorder α] {s t : Set α} {a b : α} (ha : IsLeast s a) (hb : IsLeast t b) (hst : s ⊆ t) : b ≤ a

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

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

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

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

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

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

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

Conversions

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

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

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

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

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

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

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

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

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

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

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

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

theorem IsLUB.bddAbove {α : Type u_1} [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_1} [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_1} [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_1} [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_1} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : s.Nonempty

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

Union and intersection

@[simp]

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

@[simp]

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

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

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

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

theorem isGreatest_union_iff {α : Type u_1} [Preorder α] {s 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_1} [Preorder α] {s t : Set α} (h : BddAbove s) : BddAbove (s ∩ t)

If s is bounded, then so is s ∩ t

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

If t is bounded, then so is s ∩ t

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

If s is bounded, then so is s ∩ t

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

If t is bounded, then so is s ∩ t

theorem BddAbove.union {α : Type u_1} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {s 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_1} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {s 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_1} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {s 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_1} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {s 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 u_3} [SemilatticeSup γ] {a b : γ} {s 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 u_3} [SemilatticeInf γ] {a₁ a₂ : γ} {s 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 u_3} [LinearOrder γ] {a b : γ} {s 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 u_3} [LinearOrder γ] {a b : γ} {s 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 u_3} [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 u_3} [LinearOrder γ] {s : Set γ} {a b : γ} (ha : IsGLB s a) (hb : b ∈ s) : IsGLB (s ∩ Set.Iic b) a

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

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

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

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

Specific sets

Unbounded intervals

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

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

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

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

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

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

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

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

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

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

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

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

theorem lub_Iio_eq_self_or_Iio_eq_Iic {γ : Type u_3} [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 u_3} [PartialOrder γ] {j : γ} (i : γ) (hj : IsGLB (Set.Ioi i) j) : j = i ∨ Set.Ioi i = Set.Ici j

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

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

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

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

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

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

Singleton

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Bounded intervals

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Univ

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[deprecated NoTopOrder.upperBounds_univ (since := "2025-04-18")]

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

Alias of NoTopOrder.upperBounds_univ.

@[simp]

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

@[deprecated NoBotOrder.lowerBounds_univ (since := "2025-04-18")]

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

Alias of NoBotOrder.lowerBounds_univ.

@[simp]

theorem not_bddAbove_univ {α : Type u_1} [Preorder α] [NoTopOrder α] : ¬BddAbove Set.univ

@[simp]

theorem not_bddBelow_univ {α : Type u_1} [Preorder α] [NoBotOrder α] : ¬BddBelow Set.univ

Empty set

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

insert

@[simp]

theorem bddAbove_insert {α : Type u_1} [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_1} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} (a : α) : BddAbove s → BddAbove (insert a s)

@[simp]

theorem bddBelow_insert {α : Type u_1} [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_1} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {s : Set α} (a : α) : BddBelow s → BddBelow (insert a s)

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem OrderBot.bddBelow {α : Type u_1} [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 u_3} [SemilatticeSup γ] {a b : γ} : IsLUB {a, b} (a ⊔ b)

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

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

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

Lower/upper bounds

@[simp]

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

@[simp]

theorem isGLB_upperBounds {α : Type u_1} [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_1} [Preorder α] {s : Set α} {a b : α} (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds s) : s.Nonempty → a ≤ b

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

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

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

theorem le_of_isLUB_le_isGLB {α : Type u_1} [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

@[simp]

theorem upperBounds_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) : upperBounds (s ×ˢ t) = upperBounds s ×ˢ upperBounds t

@[simp]

theorem lowerBounds_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) : lowerBounds (s ×ˢ t) = lowerBounds s ×ˢ lowerBounds t

theorem IsLUB.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} {a : α} {b : β} (hs : s.Nonempty) (ht : t.Nonempty) (ha : IsLUB s a) (hb : IsLUB t b) : IsLUB (s ×ˢ t) (a, b)

theorem IsGLB.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} {a : α} {b : β} (hs : s.Nonempty) (ht : t.Nonempty) (ha : IsGLB s a) (hb : IsGLB t b) : IsGLB (s ×ˢ t) (a, b)

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

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

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

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

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

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

theorem Set.subsingleton_of_isLUB_le_isGLB {α : Type u_1} [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_1} [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_1} [LinearOrder α] {s : Set α} {a b : α} (h : IsLUB s a) : b < a ↔ ∃ c ∈ s, b < c

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

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

theorem IsLUB.exists_between' {α : Type u_1} [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_1} [LinearOrder α] {s : Set α} {a b : α} (h : IsGLB s a) (hb : a < b) : ∃ c ∈ s, a ≤ c ∧ c < b

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

theorem isGreatest_himp {α : Type u_1} [GeneralizedHeytingAlgebra α] (a b : α) : IsGreatest {w : α | w ⊓ a ≤ b} (a ⇨ b)

theorem isLeast_sdiff {α : Type u_1} [GeneralizedCoheytingAlgebra α] (a b : α) : IsLeast {w : α | a ≤ b ⊔ w} (a \ b)

theorem isGreatest_compl {α : Type u_1} [HeytingAlgebra α] (a : α) : IsGreatest {w : α | Disjoint w a} aᶜ

theorem isLeast_hnot {α : Type u_1} [CoheytingAlgebra α] (a : α) : IsLeast {w : α | Codisjoint a w} (￢a)

instance Nat.instDecidableIsLeast (p : ℕ → Prop) (n : ℕ) [DecidablePred p] : Decidable (IsLeast {n : ℕ | p n} n)

Equations

• Nat.instDecidableIsLeast p n = decidable_of_iff (p n ∧ ∀ k < n, ¬p k) ⋯