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 : Set.Bounded r t)
:
Set.Bounded r s
theorem
Set.Unbounded.mono
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
{t : Set α}
(hst : s ⊆ t)
(hs : Set.Unbounded r s)
:
Set.Unbounded r t
Alternate characterizations of unboundedness on orders #
theorem
Set.unbounded_le_of_forall_exists_lt
{α : Type u_1}
{s : Set α}
[Preorder α]
(h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b)
:
Set.Unbounded (fun x x_1 => x ≤ x_1) s
theorem
Set.unbounded_lt_of_forall_exists_le
{α : Type u_1}
{s : Set α}
[Preorder α]
(h : ∀ (a : α), ∃ b, b ∈ s ∧ a ≤ b)
:
Set.Unbounded (fun x x_1 => x < x_1) s
theorem
Set.unbounded_ge_of_forall_exists_gt
{α : Type u_1}
{s : Set α}
[Preorder α]
(h : ∀ (a : α), ∃ b, b ∈ s ∧ b < a)
:
Set.Unbounded (fun x x_1 => x ≥ x_1) s
theorem
Set.unbounded_gt_of_forall_exists_ge
{α : Type u_1}
{s : Set α}
[Preorder α]
(h : ∀ (a : α), ∃ b, b ∈ s ∧ b ≤ a)
:
Set.Unbounded (fun x x_1 => x > x_1) s
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')
:
Set.Bounded r' s
theorem
Set.bounded_le_of_bounded_lt
{α : Type u_1}
{s : Set α}
[Preorder α]
(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 : Set.Unbounded r s)
:
Set.Unbounded r' s
theorem
Set.unbounded_lt_of_unbounded_le
{α : Type u_1}
{s : Set α}
[Preorder α]
(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 α}
[Preorder α]
[NoMaxOrder α]
:
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 α}
[Preorder α]
[NoMaxOrder α]
:
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 α}
[Preorder α]
(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 α}
[Preorder α]
(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 α}
[Preorder α]
[NoMinOrder α]
:
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 α}
[Preorder α]
[NoMinOrder α]
:
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}
[LE α]
[NoTopOrder α]
:
Set.Unbounded (fun x x_1 => x ≤ x_1) Set.univ
theorem
Set.unbounded_lt_univ
{α : Type u_1}
[Preorder α]
[NoTopOrder α]
:
Set.Unbounded (fun x x_1 => x < x_1) Set.univ
theorem
Set.unbounded_ge_univ
{α : Type u_1}
[LE α]
[NoBotOrder α]
:
Set.Unbounded (fun x x_1 => x ≥ x_1) Set.univ
theorem
Set.unbounded_gt_univ
{α : Type u_1}
[Preorder α]
[NoBotOrder α]
:
Set.Unbounded (fun x x_1 => x > x_1) Set.univ
Bounded and unbounded intervals #
Half-open bounded intervals #
theorem
Set.bounded_lt_Iio
{α : Type u_1}
[Preorder α]
(a : α)
:
Set.Bounded (fun x x_1 => x < x_1) (Set.Iio a)
theorem
Set.bounded_le_Iio
{α : Type u_1}
[Preorder α]
(a : α)
:
Set.Bounded (fun x x_1 => x ≤ x_1) (Set.Iio a)
theorem
Set.bounded_le_Iic
{α : Type u_1}
[Preorder α]
(a : α)
:
Set.Bounded (fun x x_1 => x ≤ x_1) (Set.Iic a)
theorem
Set.bounded_lt_Iic
{α : Type u_1}
[Preorder α]
[NoMaxOrder α]
(a : α)
:
Set.Bounded (fun x x_1 => x < x_1) (Set.Iic a)
theorem
Set.bounded_gt_Ioi
{α : Type u_1}
[Preorder α]
(a : α)
:
Set.Bounded (fun x x_1 => x > x_1) (Set.Ioi a)
theorem
Set.bounded_ge_Ioi
{α : Type u_1}
[Preorder α]
(a : α)
:
Set.Bounded (fun x x_1 => x ≥ x_1) (Set.Ioi a)
theorem
Set.bounded_ge_Ici
{α : Type u_1}
[Preorder α]
(a : α)
:
Set.Bounded (fun x x_1 => x ≥ x_1) (Set.Ici a)
theorem
Set.bounded_gt_Ici
{α : Type u_1}
[Preorder α]
[NoMinOrder α]
(a : α)
:
Set.Bounded (fun x x_1 => x > x_1) (Set.Ici a)
Other bounded intervals #
theorem
Set.bounded_lt_Ioo
{α : Type u_1}
[Preorder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x < x_1) (Set.Ioo a b)
theorem
Set.bounded_lt_Ico
{α : Type u_1}
[Preorder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x < x_1) (Set.Ico a b)
theorem
Set.bounded_lt_Ioc
{α : Type u_1}
[Preorder α]
[NoMaxOrder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x < x_1) (Set.Ioc a b)
theorem
Set.bounded_lt_Icc
{α : Type u_1}
[Preorder α]
[NoMaxOrder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x < x_1) (Set.Icc a b)
theorem
Set.bounded_le_Ioo
{α : Type u_1}
[Preorder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x ≤ x_1) (Set.Ioo a b)
theorem
Set.bounded_le_Ico
{α : Type u_1}
[Preorder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x ≤ x_1) (Set.Ico a b)
theorem
Set.bounded_le_Ioc
{α : Type u_1}
[Preorder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x ≤ x_1) (Set.Ioc a b)
theorem
Set.bounded_le_Icc
{α : Type u_1}
[Preorder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x ≤ x_1) (Set.Icc a b)
theorem
Set.bounded_gt_Ioo
{α : Type u_1}
[Preorder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x > x_1) (Set.Ioo a b)
theorem
Set.bounded_gt_Ioc
{α : Type u_1}
[Preorder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x > x_1) (Set.Ioc a b)
theorem
Set.bounded_gt_Ico
{α : Type u_1}
[Preorder α]
[NoMinOrder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x > x_1) (Set.Ico a b)
theorem
Set.bounded_gt_Icc
{α : Type u_1}
[Preorder α]
[NoMinOrder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x > x_1) (Set.Icc a b)
theorem
Set.bounded_ge_Ioo
{α : Type u_1}
[Preorder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x ≥ x_1) (Set.Ioo a b)
theorem
Set.bounded_ge_Ioc
{α : Type u_1}
[Preorder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x ≥ x_1) (Set.Ioc a b)
theorem
Set.bounded_ge_Ico
{α : Type u_1}
[Preorder α]
(a : α)
(b : α)
:
Set.Bounded (fun x x_1 => x ≥ x_1) (Set.Ico a b)
theorem
Set.bounded_ge_Icc
{α : Type u_1}
[Preorder α]
(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}
[SemilatticeSup α]
[NoMaxOrder α]
(a : α)
:
Set.Unbounded (fun x x_1 => x ≤ x_1) (Set.Ioi a)
theorem
Set.unbounded_le_Ici
{α : Type u_1}
[SemilatticeSup α]
[NoMaxOrder α]
(a : α)
:
Set.Unbounded (fun x x_1 => x ≤ x_1) (Set.Ici a)
theorem
Set.unbounded_lt_Ioi
{α : Type u_1}
[SemilatticeSup α]
[NoMaxOrder α]
(a : α)
:
Set.Unbounded (fun x x_1 => x < x_1) (Set.Ioi a)
theorem
Set.unbounded_lt_Ici
{α : Type u_1}
[SemilatticeSup α]
(a : α)
:
Set.Unbounded (fun x x_1 => x < x_1) (Set.Ici 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 b → r 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 b → r 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 α}
[SemilatticeSup α]
(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 α}
[SemilatticeSup α]
(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 α}
[LinearOrder α]
(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 α}
[LinearOrder α]
(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 α}
[LinearOrder α]
(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 α}
[LinearOrder α]
(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 α}
[SemilatticeSup α]
(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 α}
[SemilatticeSup α]
(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 α}
[LinearOrder α]
(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 α}
[LinearOrder α]
(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 α}
[LinearOrder α]
[NoMaxOrder α]
(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 α}
[LinearOrder α]
[NoMaxOrder α]
(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 α}
[SemilatticeInf α]
(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 α}
[SemilatticeInf α]
(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 α}
[LinearOrder α]
(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 α}
[LinearOrder α]
(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 α}
[LinearOrder α]
(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 α}
[LinearOrder α]
(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 α}
[SemilatticeInf α]
(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 α}
[SemilatticeInf α]
(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 α}
[LinearOrder α]
(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 α}
[LinearOrder α]
(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 α}
[LinearOrder α]
[NoMinOrder α]
(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 α}
[LinearOrder α]
[NoMinOrder α]
(a : α)
:
Set.Unbounded (fun x x_1 => x > x_1) (s ∩ {b | b < a}) ↔ Set.Unbounded (fun x x_1 => x > x_1) s