mathlib documentation

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 #

theorem set.bounded.mono {α : Type u_1} {r : α → α → Prop} {s t : set α} (hst : s t) (hs : set.bounded r t) :
theorem set.unbounded.mono {α : Type u_1} {r : α → α → Prop} {s t : set α} (hst : s t) (hs : set.unbounded r s) :

Alternate characterizations of unboundedness on orders #

theorem set.unbounded_le_of_forall_exists_lt {α : Type u_1} {s : set α} [preorder α] (h : ∀ (a : α), ∃ (b : α) (H : b s), a < b) :
theorem set.unbounded_le_iff {α : Type u_1} {s : set α} [linear_order α] :
set.unbounded has_le.le s ∀ (a : α), ∃ (b : α) (H : b s), a < b
theorem set.unbounded_lt_of_forall_exists_le {α : Type u_1} {s : set α} [preorder α] (h : ∀ (a : α), ∃ (b : α) (H : b s), a b) :
theorem set.unbounded_lt_iff {α : Type u_1} {s : set α} [linear_order α] :
set.unbounded has_lt.lt s ∀ (a : α), ∃ (b : α) (H : b s), a b
theorem set.unbounded_ge_of_forall_exists_gt {α : Type u_1} {s : set α} [preorder α] (h : ∀ (a : α), ∃ (b : α) (H : b s), b < a) :
theorem set.unbounded_ge_iff {α : Type u_1} {s : set α} [linear_order α] :
set.unbounded ge s ∀ (a : α), ∃ (b : α) (H : b s), b < a
theorem set.unbounded_gt_of_forall_exists_ge {α : Type u_1} {s : set α} [preorder α] (h : ∀ (a : α), ∃ (b : α) (H : b s), b a) :
theorem set.unbounded_gt_iff {α : Type u_1} {s : set α} [linear_order α] :
set.unbounded gt s ∀ (a : α), ∃ (b : α) (H : b s), b a

Relation between boundedness by strict and nonstrict orders. #

Less and less or equal #

theorem set.bounded.rel_mono {α : Type u_1} {r : α → α → Prop} {s : set α} {r' : α → α → Prop} (h : set.bounded r s) (hrr' : r r') :
theorem set.bounded_le_of_bounded_lt {α : Type u_1} {s : set α} [preorder α] (h : set.bounded has_lt.lt s) :
theorem set.unbounded.rel_mono {α : Type u_1} {r : α → α → Prop} {s : set α} {r' : α → α → Prop} (hr : r' r) (h : set.unbounded r s) :

Greater and greater or equal #

theorem set.bounded_ge_of_bounded_gt {α : Type u_1} {s : set α} [preorder α] (h : set.bounded gt s) :
theorem set.unbounded_gt_of_unbounded_ge {α : Type u_1} {s : set α} [preorder α] (h : set.unbounded ge s) :
theorem set.bounded_ge_iff_bounded_gt {α : Type u_1} {s : set α} [preorder α] [no_min_order α] :

The universal set #

Bounded and unbounded intervals #

theorem set.bounded_self {α : Type u_1} {r : α → α → Prop} (a : α) :
set.bounded r {b : α | r b a}

Half-open bounded intervals #

theorem set.bounded_lt_Iio {α : Type u_1} [preorder α] (a : α) :
theorem set.bounded_le_Iio {α : Type u_1} [preorder α] (a : α) :
theorem set.bounded_le_Iic {α : Type u_1} [preorder α] (a : α) :
theorem set.bounded_lt_Iic {α : Type u_1} [preorder α] [no_max_order α] (a : α) :
theorem set.bounded_gt_Ioi {α : Type u_1} [preorder α] (a : α) :
theorem set.bounded_ge_Ioi {α : Type u_1} [preorder α] (a : α) :
theorem set.bounded_ge_Ici {α : Type u_1} [preorder α] (a : α) :
theorem set.bounded_gt_Ici {α : Type u_1} [preorder α] [no_min_order α] (a : α) :

Other bounded intervals #

theorem set.bounded_lt_Ioo {α : Type u_1} [preorder α] (a b : α) :
theorem set.bounded_lt_Ico {α : Type u_1} [preorder α] (a b : α) :
theorem set.bounded_lt_Ioc {α : Type u_1} [preorder α] [no_max_order α] (a b : α) :
theorem set.bounded_lt_Icc {α : Type u_1} [preorder α] [no_max_order α] (a b : α) :
theorem set.bounded_le_Ioo {α : Type u_1} [preorder α] (a b : α) :
theorem set.bounded_le_Ico {α : Type u_1} [preorder α] (a b : α) :
theorem set.bounded_le_Ioc {α : Type u_1} [preorder α] (a b : α) :
theorem set.bounded_le_Icc {α : Type u_1} [preorder α] (a b : α) :
theorem set.bounded_gt_Ioo {α : Type u_1} [preorder α] (a b : α) :
theorem set.bounded_gt_Ioc {α : Type u_1} [preorder α] (a b : α) :
theorem set.bounded_gt_Ico {α : Type u_1} [preorder α] [no_min_order α] (a b : α) :
theorem set.bounded_gt_Icc {α : Type u_1} [preorder α] [no_min_order α] (a b : α) :
theorem set.bounded_ge_Ioo {α : Type u_1} [preorder α] (a b : α) :
theorem set.bounded_ge_Ioc {α : Type u_1} [preorder α] (a b : α) :
theorem set.bounded_ge_Ico {α : Type u_1} [preorder α] (a b : α) :
theorem set.bounded_ge_Icc {α : Type u_1} [preorder α] (a b : α) :

Unbounded intervals #

theorem set.unbounded_le_Ioi {α : Type u_1} [semilattice_sup α] [no_max_order α] (a : α) :
theorem set.unbounded_le_Ici {α : Type u_1} [semilattice_sup α] [no_max_order α] (a : α) :
theorem set.unbounded_lt_Ioi {α : Type u_1} [semilattice_sup α] [no_max_order α] (a : α) :
theorem set.unbounded_lt_Ici {α : Type u_1} [semilattice_sup α] (a : α) :

Bounded initial segments #

theorem set.bounded_inter_not {α : Type u_1} {r : α → α → Prop} {s : set α} (H : ∀ (a b : α), ∃ (m : α), ∀ (c : α), r c a r c br c m) (a : α) :
set.bounded r (s {b : α | ¬r b a}) set.bounded r s
theorem set.unbounded_inter_not {α : Type u_1} {r : α → α → Prop} {s : set α} (H : ∀ (a b : α), ∃ (m : α), ∀ (c : α), r c a r c br c m) (a : α) :
set.unbounded r (s {b : α | ¬r b a}) set.unbounded r s

Less or equal #

theorem set.bounded_le_inter_not_le {α : Type u_1} {s : set α} [semilattice_sup α] (a : α) :
theorem set.unbounded_le_inter_not_le {α : Type u_1} {s : set α} [semilattice_sup α] (a : α) :
theorem set.bounded_le_inter_lt {α : Type u_1} {s : set α} [linear_order α] (a : α) :
theorem set.unbounded_le_inter_lt {α : Type u_1} {s : set α} [linear_order α] (a : α) :
theorem set.bounded_le_inter_le {α : Type u_1} {s : set α} [linear_order α] (a : α) :
theorem set.unbounded_le_inter_le {α : Type u_1} {s : set α} [linear_order α] (a : α) :

Less than #

theorem set.bounded_lt_inter_not_lt {α : Type u_1} {s : set α} [semilattice_sup α] (a : α) :
theorem set.unbounded_lt_inter_not_lt {α : Type u_1} {s : set α} [semilattice_sup α] (a : α) :
theorem set.bounded_lt_inter_le {α : Type u_1} {s : set α} [linear_order α] (a : α) :
theorem set.unbounded_lt_inter_le {α : Type u_1} {s : set α} [linear_order α] (a : α) :
theorem set.bounded_lt_inter_lt {α : Type u_1} {s : set α} [linear_order α] [no_max_order α] (a : α) :
theorem set.unbounded_lt_inter_lt {α : Type u_1} {s : set α} [linear_order α] [no_max_order α] (a : α) :

Greater or equal #

theorem set.bounded_ge_inter_not_ge {α : Type u_1} {s : set α} [semilattice_inf α] (a : α) :
set.bounded ge (s {b : α | ¬a b}) set.bounded ge s
theorem set.unbounded_ge_inter_not_ge {α : Type u_1} {s : set α} [semilattice_inf α] (a : α) :
theorem set.bounded_ge_inter_gt {α : Type u_1} {s : set α} [linear_order α] (a : α) :
set.bounded ge (s {b : α | b < a}) set.bounded ge s
theorem set.unbounded_ge_inter_gt {α : Type u_1} {s : set α} [linear_order α] (a : α) :
set.unbounded ge (s {b : α | b < a}) set.unbounded ge s
theorem set.bounded_ge_inter_ge {α : Type u_1} {s : set α} [linear_order α] (a : α) :
set.bounded ge (s {b : α | b a}) set.bounded ge s
theorem set.unbounded_ge_iff_unbounded_inter_ge {α : Type u_1} {s : set α} [linear_order α] (a : α) :
set.unbounded ge (s {b : α | b a}) set.unbounded ge s

Greater than #

theorem set.bounded_gt_inter_not_gt {α : Type u_1} {s : set α} [semilattice_inf α] (a : α) :
set.bounded gt (s {b : α | ¬a < b}) set.bounded gt s
theorem set.unbounded_gt_inter_not_gt {α : Type u_1} {s : set α} [semilattice_inf α] (a : α) :
set.unbounded gt (s {b : α | ¬a < b}) set.unbounded gt s
theorem set.bounded_gt_inter_ge {α : Type u_1} {s : set α} [linear_order α] (a : α) :
set.bounded gt (s {b : α | b a}) set.bounded gt s
theorem set.unbounded_inter_ge {α : Type u_1} {s : set α} [linear_order α] (a : α) :
set.unbounded gt (s {b : α | b a}) set.unbounded gt s
theorem set.bounded_gt_inter_gt {α : Type u_1} {s : set α} [linear_order α] [no_min_order α] (a : α) :
set.bounded gt (s {b : α | b < a}) set.bounded gt s
theorem set.unbounded_gt_inter_gt {α : Type u_1} {s : set α} [linear_order α] [no_min_order α] (a : α) :
set.unbounded gt (s {b : α | b < a}) set.unbounded gt s