Documentation

Mathlib.Order.Bounded

Bounded and unbounded sets #

We prove miscellaneous lemmas about bounded and unbounded sets. Many of these are just variations on the same ideas, or similar results with a few minor differences. The file is divided into these different general ideas.

Subsets of bounded and unbounded sets #

source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.Bounded.mono {α : Type u_1} {r : α → α → Prop} {s t : Set α} (hst : s ⊆ t) (hs : Bounded r t) :
Bounded r s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.Unbounded.mono {α : Type u_1} {r : α → α → Prop} {s t : Set α} (hst : s ⊆ t) (hs : Unbounded r s) :
Unbounded r t

Alternate characterizations of unboundedness on orders #

source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_le_of_forall_exists_lt {α : Type u_1} {s : Set α} [Preorder α] (h : ∀ (a : α), ∃ (b : α), b ∈ s ∧ a < b) :
Unbounded (fun (x1 x2 : α) => x1 ≤ x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_ge_of_forall_exists_gt {α : Type u_1} {s : Set α} [Preorder α] (h : ∀ (a : α), ∃ (b : α), b ∈ s ∧ b < a) :
Unbounded (fun (x1 x2 : α) => x2 ≤ x1) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_le_iff {α : Type u_1} {s : Set α} [LinearOrder α] :
Unbounded (fun (x1 x2 : α) => x1 ≤ x2) s ↔ ∀ (a : α), ∃ (b : α), b ∈ s ∧ a < b
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_ge_iff {α : Type u_1} {s : Set α} [LinearOrder α] :
Unbounded (fun (x1 x2 : α) => x2 ≤ x1) s ↔ ∀ (a : α), ∃ (b : α), b ∈ s ∧ b < a
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_lt_of_forall_exists_le {α : Type u_1} {s : Set α} [Preorder α] (h : ∀ (a : α), ∃ (b : α), b ∈ s ∧ a ≤ b) :
Unbounded (fun (x1 x2 : α) => x1 < x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_gt_of_forall_exists_ge {α : Type u_1} {s : Set α} [Preorder α] (h : ∀ (a : α), ∃ (b : α), b ∈ s ∧ b ≤ a) :
Unbounded (fun (x1 x2 : α) => x2 < x1) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_lt_iff {α : Type u_1} {s : Set α} [LinearOrder α] :
Unbounded (fun (x1 x2 : α) => x1 < x2) s ↔ ∀ (a : α), ∃ (b : α), b ∈ s ∧ a ≤ b
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_gt_iff {α : Type u_1} {s : Set α} [LinearOrder α] :
Unbounded (fun (x1 x2 : α) => x2 < x1) s ↔ ∀ (a : α), ∃ (b : α), b ∈ s ∧ b ≤ a

Relation between boundedness by strict and nonstrict orders. #

Less and less or equal #

source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.Bounded.rel_mono {α : Type u_1} {r : α → α → Prop} {s : Set α} {r' : α → α → Prop} (h : Bounded r s) (hrr' : r ≤ r') :
Bounded r' s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_le_of_bounded_lt {α : Type u_1} {s : Set α} [Preorder α] (h : Bounded (fun (x1 x2 : α) => x1 < x2) s) :
Bounded (fun (x1 x2 : α) => x1 ≤ x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.Unbounded.rel_mono {α : Type u_1} {r : α → α → Prop} {s : Set α} {r' : α → α → Prop} (hr : r' ≤ r) (h : Unbounded r s) :
Unbounded r' s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_lt_of_unbounded_le {α : Type u_1} {s : Set α} [Preorder α] (h : Unbounded (fun (x1 x2 : α) => x1 ≤ x2) s) :
Unbounded (fun (x1 x2 : α) => x1 < x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_le_iff_bounded_lt {α : Type u_1} {s : Set α} [Preorder α] [NoMaxOrder α] :
Bounded (fun (x1 x2 : α) => x1 ≤ x2) s ↔ Bounded (fun (x1 x2 : α) => x1 < x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_lt_iff_unbounded_le {α : Type u_1} {s : Set α} [Preorder α] [NoMaxOrder α] :
Unbounded (fun (x1 x2 : α) => x1 < x2) s ↔ Unbounded (fun (x1 x2 : α) => x1 ≤ x2) s

Greater and greater or equal #

source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_ge_of_bounded_gt {α : Type u_1} {s : Set α} [Preorder α] (h : Bounded (fun (x1 x2 : α) => x1 > x2) s) :
Bounded (fun (x1 x2 : α) => x1 ≥ x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_gt_of_unbounded_ge {α : Type u_1} {s : Set α} [Preorder α] (h : Unbounded (fun (x1 x2 : α) => x1 ≥ x2) s) :
Unbounded (fun (x1 x2 : α) => x1 > x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_ge_iff_bounded_gt {α : Type u_1} {s : Set α} [Preorder α] [NoMinOrder α] :
Bounded (fun (x1 x2 : α) => x1 ≥ x2) s ↔ Bounded (fun (x1 x2 : α) => x1 > x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_gt_iff_unbounded_ge {α : Type u_1} {s : Set α} [Preorder α] [NoMinOrder α] :
Unbounded (fun (x1 x2 : α) => x1 > x2) s ↔ Unbounded (fun (x1 x2 : α) => x1 ≥ x2) s

The universal set #

source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_le_univ {α : Type u_1} [LE α] [NoTopOrder α] :
Unbounded (fun (x1 x2 : α) => x1 ≤ x2) univ
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_lt_univ {α : Type u_1} [Preorder α] [NoTopOrder α] :
Unbounded (fun (x1 x2 : α) => x1 < x2) univ
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_ge_univ {α : Type u_1} [LE α] [NoBotOrder α] :
Unbounded (fun (x1 x2 : α) => x1 ≥ x2) univ
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_gt_univ {α : Type u_1} [Preorder α] [NoBotOrder α] :
Unbounded (fun (x1 x2 : α) => x1 > x2) univ

Bounded and unbounded intervals #

source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_self {α : Type u_1} {r : α → α → Prop} (a : α) :
Bounded r {b : α | r b a}

Half-open bounded intervals #

source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_lt_Iio {α : Type u_1} [Preorder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 < x2) (Iio a)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_le_Iio {α : Type u_1} [Preorder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 ≤ x2) (Iio a)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_le_Iic {α : Type u_1} [Preorder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 ≤ x2) (Iic a)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_lt_Iic {α : Type u_1} [Preorder α] [NoMaxOrder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 < x2) (Iic a)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_gt_Ioi {α : Type u_1} [Preorder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 > x2) (Ioi a)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_ge_Ioi {α : Type u_1} [Preorder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 ≥ x2) (Ioi a)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_ge_Ici {α : Type u_1} [Preorder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 ≥ x2) (Ici a)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_gt_Ici {α : Type u_1} [Preorder α] [NoMinOrder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 > x2) (Ici a)

Other bounded intervals #

source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_lt_Ioo {α : Type u_1} [Preorder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 < x2) (Ioo a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_lt_Ico {α : Type u_1} [Preorder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 < x2) (Ico a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_lt_Ioc {α : Type u_1} [Preorder α] [NoMaxOrder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 < x2) (Ioc a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_lt_Icc {α : Type u_1} [Preorder α] [NoMaxOrder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 < x2) (Icc a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_le_Ioo {α : Type u_1} [Preorder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 ≤ x2) (Ioo a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_le_Ico {α : Type u_1} [Preorder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 ≤ x2) (Ico a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_le_Ioc {α : Type u_1} [Preorder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 ≤ x2) (Ioc a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_le_Icc {α : Type u_1} [Preorder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 ≤ x2) (Icc a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_gt_Ioo {α : Type u_1} [Preorder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 > x2) (Ioo a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_gt_Ioc {α : Type u_1} [Preorder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 > x2) (Ioc a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_gt_Ico {α : Type u_1} [Preorder α] [NoMinOrder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 > x2) (Ico a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_gt_Icc {α : Type u_1} [Preorder α] [NoMinOrder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 > x2) (Icc a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_ge_Ioo {α : Type u_1} [Preorder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 ≥ x2) (Ioo a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_ge_Ioc {α : Type u_1} [Preorder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 ≥ x2) (Ioc a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_ge_Ico {α : Type u_1} [Preorder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 ≥ x2) (Ico a b)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_ge_Icc {α : Type u_1} [Preorder α] (a b : α) :
Bounded (fun (x1 x2 : α) => x1 ≥ x2) (Icc a b)

Unbounded intervals #

source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_le_Ioi {α : Type u_1} [SemilatticeSup α] [NoMaxOrder α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 ≤ x2) (Ioi a)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_le_Ici {α : Type u_1} [SemilatticeSup α] [NoMaxOrder α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 ≤ x2) (Ici a)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_lt_Ioi {α : Type u_1} [SemilatticeSup α] [NoMaxOrder α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 < x2) (Ioi a)
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_lt_Ici {α : Type u_1} [SemilatticeSup α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 < x2) (Ici a)

Bounded initial segments #

source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_inter_not {α : Type u_1} {r : α → α → Prop} {s : Set α} (H : ∀ (a b : α), ∃ (m : α), ∀ (c : α), r c a ∨ r c b → r c m) (a : α) :
Bounded r (s ∩ {b : α | ¬r b a}) ↔ Bounded r s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_inter_not {α : Type u_1} {r : α → α → Prop} {s : Set α} (H : ∀ (a b : α), ∃ (m : α), ∀ (c : α), r c a ∨ r c b → r c m) (a : α) :
Unbounded r (s ∩ {b : α | ¬r b a}) ↔ Unbounded r s

Less or equal #

source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_le_inter_not_le {α : Type u_1} {s : Set α} [SemilatticeSup α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 ≤ x2) (s ∩ {b : α | ¬b ≤ a}) ↔ Bounded (fun (x1 x2 : α) => x1 ≤ x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_le_inter_not_le {α : Type u_1} {s : Set α} [SemilatticeSup α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 ≤ x2) (s ∩ {b : α | ¬b ≤ a}) ↔ Unbounded (fun (x1 x2 : α) => x1 ≤ x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_le_inter_lt {α : Type u_1} {s : Set α} [LinearOrder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 ≤ x2) (s ∩ {b : α | a < b}) ↔ Bounded (fun (x1 x2 : α) => x1 ≤ x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_le_inter_lt {α : Type u_1} {s : Set α} [LinearOrder α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 ≤ x2) (s ∩ {b : α | a < b}) ↔ Unbounded (fun (x1 x2 : α) => x1 ≤ x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_le_inter_le {α : Type u_1} {s : Set α} [LinearOrder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 ≤ x2) (s ∩ {b : α | a ≤ b}) ↔ Bounded (fun (x1 x2 : α) => x1 ≤ x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_le_inter_le {α : Type u_1} {s : Set α} [LinearOrder α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 ≤ x2) (s ∩ {b : α | a ≤ b}) ↔ Unbounded (fun (x1 x2 : α) => x1 ≤ x2) s

Less than #

source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_lt_inter_not_lt {α : Type u_1} {s : Set α} [SemilatticeSup α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 < x2) (s ∩ {b : α | ¬b < a}) ↔ Bounded (fun (x1 x2 : α) => x1 < x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_lt_inter_not_lt {α : Type u_1} {s : Set α} [SemilatticeSup α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 < x2) (s ∩ {b : α | ¬b < a}) ↔ Unbounded (fun (x1 x2 : α) => x1 < x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_lt_inter_le {α : Type u_1} {s : Set α} [LinearOrder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 < x2) (s ∩ {b : α | a ≤ b}) ↔ Bounded (fun (x1 x2 : α) => x1 < x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_lt_inter_le {α : Type u_1} {s : Set α} [LinearOrder α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 < x2) (s ∩ {b : α | a ≤ b}) ↔ Unbounded (fun (x1 x2 : α) => x1 < x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_lt_inter_lt {α : Type u_1} {s : Set α} [LinearOrder α] [NoMaxOrder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 < x2) (s ∩ {b : α | a < b}) ↔ Bounded (fun (x1 x2 : α) => x1 < x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_lt_inter_lt {α : Type u_1} {s : Set α} [LinearOrder α] [NoMaxOrder α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 < x2) (s ∩ {b : α | a < b}) ↔ Unbounded (fun (x1 x2 : α) => x1 < x2) s

Greater or equal #

source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_ge_inter_not_ge {α : Type u_1} {s : Set α} [SemilatticeInf α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 ≥ x2) (s ∩ {b : α | ¬a ≤ b}) ↔ Bounded (fun (x1 x2 : α) => x1 ≥ x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_ge_inter_not_ge {α : Type u_1} {s : Set α} [SemilatticeInf α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 ≥ x2) (s ∩ {b : α | ¬a ≤ b}) ↔ Unbounded (fun (x1 x2 : α) => x1 ≥ x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_ge_inter_gt {α : Type u_1} {s : Set α} [LinearOrder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 ≥ x2) (s ∩ {b : α | b < a}) ↔ Bounded (fun (x1 x2 : α) => x1 ≥ x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_ge_inter_gt {α : Type u_1} {s : Set α} [LinearOrder α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 ≥ x2) (s ∩ {b : α | b < a}) ↔ Unbounded (fun (x1 x2 : α) => x1 ≥ x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_ge_inter_ge {α : Type u_1} {s : Set α} [LinearOrder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 ≥ x2) (s ∩ {b : α | b ≤ a}) ↔ Bounded (fun (x1 x2 : α) => x1 ≥ x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_ge_iff_unbounded_inter_ge {α : Type u_1} {s : Set α} [LinearOrder α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 ≥ x2) (s ∩ {b : α | b ≤ a}) ↔ Unbounded (fun (x1 x2 : α) => x1 ≥ x2) s

Greater than #

source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_gt_inter_not_gt {α : Type u_1} {s : Set α} [SemilatticeInf α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 > x2) (s ∩ {b : α | ¬a < b}) ↔ Bounded (fun (x1 x2 : α) => x1 > x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_gt_inter_not_gt {α : Type u_1} {s : Set α} [SemilatticeInf α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 > x2) (s ∩ {b : α | ¬a < b}) ↔ Unbounded (fun (x1 x2 : α) => x1 > x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_gt_inter_ge {α : Type u_1} {s : Set α} [LinearOrder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 > x2) (s ∩ {b : α | b ≤ a}) ↔ Bounded (fun (x1 x2 : α) => x1 > x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_inter_ge {α : Type u_1} {s : Set α} [LinearOrder α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 > x2) (s ∩ {b : α | b ≤ a}) ↔ Unbounded (fun (x1 x2 : α) => x1 > x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.bounded_gt_inter_gt {α : Type u_1} {s : Set α} [LinearOrder α] [NoMinOrder α] (a : α) :
Bounded (fun (x1 x2 : α) => x1 > x2) (s ∩ {b : α | b < a}) ↔ Bounded (fun (x1 x2 : α) => x1 > x2) s
source
@[deprecated "deprecated without replacement" (since := "2026-04-16")]
theorem Set.unbounded_gt_inter_gt {α : Type u_1} {s : Set α} [LinearOrder α] [NoMinOrder α] (a : α) :
Unbounded (fun (x1 x2 : α) => x1 > x2) (s ∩ {b : α | b < a}) ↔ Unbounded (fun (x1 x2 : α) => x1 > x2) s