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 #

theorem Set.Bounded.mono {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} (hst : s t) (hs : ) :
theorem Set.Unbounded.mono {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} (hst : s t) (hs : ) :

Alternate characterizations of unboundedness on orders #

theorem Set.unbounded_le_of_forall_exists_lt {α : Type u_1} {s : Set α} [inst : ] (h : ∀ (a : α), b, b s a < b) :
Set.Unbounded (fun x x_1 => x x_1) s
theorem Set.unbounded_le_iff {α : Type u_1} {s : Set α} [inst : ] :
Set.Unbounded (fun x x_1 => x x_1) s ∀ (a : α), b, b s a < b
theorem Set.unbounded_lt_of_forall_exists_le {α : Type u_1} {s : Set α} [inst : ] (h : ∀ (a : α), b, b s a b) :
Set.Unbounded (fun x x_1 => x < x_1) s
theorem Set.unbounded_lt_iff {α : Type u_1} {s : Set α} [inst : ] :
Set.Unbounded (fun x x_1 => x < x_1) s ∀ (a : α), b, b s a b
theorem Set.unbounded_ge_of_forall_exists_gt {α : Type u_1} {s : Set α} [inst : ] (h : ∀ (a : α), b, b s b < a) :
Set.Unbounded (fun x x_1 => x x_1) s
theorem Set.unbounded_ge_iff {α : Type u_1} {s : Set α} [inst : ] :
Set.Unbounded (fun x x_1 => x x_1) s ∀ (a : α), b, b s b < a
theorem Set.unbounded_gt_of_forall_exists_ge {α : Type u_1} {s : Set α} [inst : ] (h : ∀ (a : α), b, b s b a) :
Set.Unbounded (fun x x_1 => x > x_1) s
theorem Set.unbounded_gt_iff {α : Type u_1} {s : Set α} [inst : ] :
Set.Unbounded (fun x x_1 => x > x_1) s ∀ (a : α), b, 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 : ) (hrr' : r r') :
theorem Set.bounded_le_of_bounded_lt {α : Type u_1} {s : Set α} [inst : ] (h : Set.Bounded (fun x x_1 => x < x_1) s) :
Set.Bounded (fun x x_1 => x x_1) s
theorem Set.Unbounded.rel_mono {α : Type u_1} {r : ααProp} {s : Set α} {r' : ααProp} (hr : r' r) (h : ) :
theorem Set.unbounded_lt_of_unbounded_le {α : Type u_1} {s : Set α} [inst : ] (h : Set.Unbounded (fun x x_1 => x x_1) s) :
Set.Unbounded (fun x x_1 => x < x_1) s
theorem Set.bounded_le_iff_bounded_lt {α : Type u_1} {s : Set α} [inst : ] [inst : ] :
Set.Bounded (fun x x_1 => x x_1) s Set.Bounded (fun x x_1 => x < x_1) s
theorem Set.unbounded_lt_iff_unbounded_le {α : Type u_1} {s : Set α} [inst : ] [inst : ] :
Set.Unbounded (fun x x_1 => x < x_1) s Set.Unbounded (fun x x_1 => x x_1) s

Greater and greater or equal #

theorem Set.bounded_ge_of_bounded_gt {α : Type u_1} {s : Set α} [inst : ] (h : Set.Bounded (fun x x_1 => x > x_1) s) :
Set.Bounded (fun x x_1 => x x_1) s
theorem Set.unbounded_gt_of_unbounded_ge {α : Type u_1} {s : Set α} [inst : ] (h : Set.Unbounded (fun x x_1 => x x_1) s) :
Set.Unbounded (fun x x_1 => x > x_1) s
theorem Set.bounded_ge_iff_bounded_gt {α : Type u_1} {s : Set α} [inst : ] [inst : ] :
Set.Bounded (fun x x_1 => x x_1) s Set.Bounded (fun x x_1 => x > x_1) s
theorem Set.unbounded_gt_iff_unbounded_ge {α : Type u_1} {s : Set α} [inst : ] [inst : ] :
Set.Unbounded (fun x x_1 => x > x_1) s Set.Unbounded (fun x x_1 => x x_1) s

The universal set #

theorem Set.unbounded_le_univ {α : Type u_1} [inst : LE α] [inst : ] :
Set.Unbounded (fun x x_1 => x x_1) Set.univ
theorem Set.unbounded_lt_univ {α : Type u_1} [inst : ] [inst : ] :
Set.Unbounded (fun x x_1 => x < x_1) Set.univ
theorem Set.unbounded_ge_univ {α : Type u_1} [inst : LE α] [inst : ] :
Set.Unbounded (fun x x_1 => x x_1) Set.univ
theorem Set.unbounded_gt_univ {α : Type u_1} [inst : ] [inst : ] :
Set.Unbounded (fun x x_1 => x > x_1) Set.univ

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} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x < x_1) ()
theorem Set.bounded_le_Iio {α : Type u_1} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x x_1) ()
theorem Set.bounded_le_Iic {α : Type u_1} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x x_1) ()
theorem Set.bounded_lt_Iic {α : Type u_1} [inst : ] [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x < x_1) ()
theorem Set.bounded_gt_Ioi {α : Type u_1} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x > x_1) ()
theorem Set.bounded_ge_Ioi {α : Type u_1} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x x_1) ()
theorem Set.bounded_ge_Ici {α : Type u_1} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x x_1) ()
theorem Set.bounded_gt_Ici {α : Type u_1} [inst : ] [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x > x_1) ()

Other bounded intervals #

theorem Set.bounded_lt_Ioo {α : Type u_1} [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x < x_1) (Set.Ioo a b)
theorem Set.bounded_lt_Ico {α : Type u_1} [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x < x_1) (Set.Ico a b)
theorem Set.bounded_lt_Ioc {α : Type u_1} [inst : ] [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x < x_1) (Set.Ioc a b)
theorem Set.bounded_lt_Icc {α : Type u_1} [inst : ] [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x < x_1) (Set.Icc a b)
theorem Set.bounded_le_Ioo {α : Type u_1} [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x x_1) (Set.Ioo a b)
theorem Set.bounded_le_Ico {α : Type u_1} [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x x_1) (Set.Ico a b)
theorem Set.bounded_le_Ioc {α : Type u_1} [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x x_1) (Set.Ioc a b)
theorem Set.bounded_le_Icc {α : Type u_1} [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x x_1) (Set.Icc a b)
theorem Set.bounded_gt_Ioo {α : Type u_1} [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x > x_1) (Set.Ioo a b)
theorem Set.bounded_gt_Ioc {α : Type u_1} [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x > x_1) (Set.Ioc a b)
theorem Set.bounded_gt_Ico {α : Type u_1} [inst : ] [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x > x_1) (Set.Ico a b)
theorem Set.bounded_gt_Icc {α : Type u_1} [inst : ] [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x > x_1) (Set.Icc a b)
theorem Set.bounded_ge_Ioo {α : Type u_1} [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x x_1) (Set.Ioo a b)
theorem Set.bounded_ge_Ioc {α : Type u_1} [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x x_1) (Set.Ioc a b)
theorem Set.bounded_ge_Ico {α : Type u_1} [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x x_1) (Set.Ico a b)
theorem Set.bounded_ge_Icc {α : Type u_1} [inst : ] (a : α) (b : α) :
Set.Bounded (fun x x_1 => x x_1) (Set.Icc a b)

Unbounded intervals #

theorem Set.unbounded_le_Ioi {α : Type u_1} [inst : ] [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x x_1) ()
theorem Set.unbounded_le_Ici {α : Type u_1} [inst : ] [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x x_1) ()
theorem Set.unbounded_lt_Ioi {α : Type u_1} [inst : ] [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x < x_1) ()
theorem Set.unbounded_lt_Ici {α : Type u_1} [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x < x_1) ()

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 })
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 })

Less or equal #

theorem Set.bounded_le_inter_not_le {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x x_1) (s { b | ¬b a }) Set.Bounded (fun x x_1 => x x_1) s
theorem Set.unbounded_le_inter_not_le {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x x_1) (s { b | ¬b a }) Set.Unbounded (fun x x_1 => x x_1) s
theorem Set.bounded_le_inter_lt {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x x_1) (s { b | a < b }) Set.Bounded (fun x x_1 => x x_1) s
theorem Set.unbounded_le_inter_lt {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x x_1) (s { b | a < b }) Set.Unbounded (fun x x_1 => x x_1) s
theorem Set.bounded_le_inter_le {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x x_1) (s { b | a b }) Set.Bounded (fun x x_1 => x x_1) s
theorem Set.unbounded_le_inter_le {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x x_1) (s { b | a b }) Set.Unbounded (fun x x_1 => x x_1) s

Less than #

theorem Set.bounded_lt_inter_not_lt {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x < x_1) (s { b | ¬b < a }) Set.Bounded (fun x x_1 => x < x_1) s
theorem Set.unbounded_lt_inter_not_lt {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x < x_1) (s { b | ¬b < a }) Set.Unbounded (fun x x_1 => x < x_1) s
theorem Set.bounded_lt_inter_le {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x < x_1) (s { b | a b }) Set.Bounded (fun x x_1 => x < x_1) s
theorem Set.unbounded_lt_inter_le {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x < x_1) (s { b | a b }) Set.Unbounded (fun x x_1 => x < x_1) s
theorem Set.bounded_lt_inter_lt {α : Type u_1} {s : Set α} [inst : ] [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x < x_1) (s { b | a < b }) Set.Bounded (fun x x_1 => x < x_1) s
theorem Set.unbounded_lt_inter_lt {α : Type u_1} {s : Set α} [inst : ] [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x < x_1) (s { b | a < b }) Set.Unbounded (fun x x_1 => x < x_1) s

Greater or equal #

theorem Set.bounded_ge_inter_not_ge {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x x_1) (s { b | ¬a b }) Set.Bounded (fun x x_1 => x x_1) s
theorem Set.unbounded_ge_inter_not_ge {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x x_1) (s { b | ¬a b }) Set.Unbounded (fun x x_1 => x x_1) s
theorem Set.bounded_ge_inter_gt {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x x_1) (s { b | b < a }) Set.Bounded (fun x x_1 => x x_1) s
theorem Set.unbounded_ge_inter_gt {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x x_1) (s { b | b < a }) Set.Unbounded (fun x x_1 => x x_1) s
theorem Set.bounded_ge_inter_ge {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x x_1) (s { b | b a }) Set.Bounded (fun x x_1 => x x_1) s
theorem Set.unbounded_ge_iff_unbounded_inter_ge {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x x_1) (s { b | b a }) Set.Unbounded (fun x x_1 => x x_1) s

Greater than #

theorem Set.bounded_gt_inter_not_gt {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x > x_1) (s { b | ¬a < b }) Set.Bounded (fun x x_1 => x > x_1) s
theorem Set.unbounded_gt_inter_not_gt {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x > x_1) (s { b | ¬a < b }) Set.Unbounded (fun x x_1 => x > x_1) s
theorem Set.bounded_gt_inter_ge {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x > x_1) (s { b | b a }) Set.Bounded (fun x x_1 => x > x_1) s
theorem Set.unbounded_inter_ge {α : Type u_1} {s : Set α} [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x > x_1) (s { b | b a }) Set.Unbounded (fun x x_1 => x > x_1) s
theorem Set.bounded_gt_inter_gt {α : Type u_1} {s : Set α} [inst : ] [inst : ] (a : α) :
Set.Bounded (fun x x_1 => x > x_1) (s { b | b < a }) Set.Bounded (fun x x_1 => x > x_1) s
theorem Set.unbounded_gt_inter_gt {α : Type u_1} {s : Set α} [inst : ] [inst : ] (a : α) :
Set.Unbounded (fun x x_1 => x > x_1) (s { b | b < a }) Set.Unbounded (fun x x_1 => x > x_1) s