Bounded and unbounded sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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) :
set.bounded r s
theorem
set.unbounded.mono
{α : Type u_1}
{r : α → α → Prop}
{s t : set α}
(hst : s ⊆ t)
(hs : set.unbounded r s) :
set.unbounded r t
Alternate characterizations of unboundedness on orders #
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 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) :
set.unbounded r' s
theorem
set.unbounded_lt_of_unbounded_le
{α : Type u_1}
{s : set α}
[preorder α]
(h : set.unbounded has_le.le s) :
theorem
set.unbounded_lt_iff_unbounded_le
{α : Type u_1}
{s : set α}
[preorder α]
[no_max_order α] :
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 α] :
set.bounded ge s ↔ set.bounded gt s
theorem
set.unbounded_gt_iff_unbounded_ge
{α : Type u_1}
{s : set α}
[preorder α]
[no_min_order α] :
set.unbounded gt s ↔ set.unbounded ge s
The universal set #
Bounded and unbounded intervals #
Half-open bounded intervals #
theorem
set.bounded_gt_Ici
{α : Type u_1}
[preorder α]
[no_min_order α]
(a : α) :
set.bounded gt (set.Ici a)
Other bounded intervals #
theorem
set.bounded_lt_Ioo
{α : Type u_1}
[preorder α]
(a b : α) :
set.bounded has_lt.lt (set.Ioo a b)
theorem
set.bounded_lt_Ico
{α : Type u_1}
[preorder α]
(a b : α) :
set.bounded has_lt.lt (set.Ico a b)
theorem
set.bounded_lt_Ioc
{α : Type u_1}
[preorder α]
[no_max_order α]
(a b : α) :
set.bounded has_lt.lt (set.Ioc a b)
theorem
set.bounded_lt_Icc
{α : Type u_1}
[preorder α]
[no_max_order α]
(a b : α) :
set.bounded has_lt.lt (set.Icc a b)
theorem
set.bounded_le_Ioo
{α : Type u_1}
[preorder α]
(a b : α) :
set.bounded has_le.le (set.Ioo a b)
theorem
set.bounded_le_Ico
{α : Type u_1}
[preorder α]
(a b : α) :
set.bounded has_le.le (set.Ico a b)
theorem
set.bounded_le_Ioc
{α : Type u_1}
[preorder α]
(a b : α) :
set.bounded has_le.le (set.Ioc a b)
theorem
set.bounded_le_Icc
{α : Type u_1}
[preorder α]
(a b : α) :
set.bounded has_le.le (set.Icc a b)
theorem
set.bounded_gt_Ico
{α : Type u_1}
[preorder α]
[no_min_order α]
(a b : α) :
set.bounded gt (set.Ico a b)
theorem
set.bounded_gt_Icc
{α : Type u_1}
[preorder α]
[no_min_order α]
(a b : α) :
set.bounded gt (set.Icc a b)
Unbounded intervals #
Bounded initial segments #
Less or equal #
theorem
set.bounded_le_inter_not_le
{α : Type u_1}
{s : set α}
[semilattice_sup α]
(a : α) :
set.bounded has_le.le (s ∩ {b : α | ¬b ≤ a}) ↔ set.bounded has_le.le s
theorem
set.unbounded_le_inter_not_le
{α : Type u_1}
{s : set α}
[semilattice_sup α]
(a : α) :
set.unbounded has_le.le (s ∩ {b : α | ¬b ≤ a}) ↔ set.unbounded has_le.le s
theorem
set.bounded_le_inter_lt
{α : Type u_1}
{s : set α}
[linear_order α]
(a : α) :
set.bounded has_le.le (s ∩ {b : α | a < b}) ↔ set.bounded has_le.le s
theorem
set.unbounded_le_inter_lt
{α : Type u_1}
{s : set α}
[linear_order α]
(a : α) :
set.unbounded has_le.le (s ∩ {b : α | a < b}) ↔ set.unbounded has_le.le s
theorem
set.bounded_le_inter_le
{α : Type u_1}
{s : set α}
[linear_order α]
(a : α) :
set.bounded has_le.le (s ∩ {b : α | a ≤ b}) ↔ set.bounded has_le.le s
theorem
set.unbounded_le_inter_le
{α : Type u_1}
{s : set α}
[linear_order α]
(a : α) :
set.unbounded has_le.le (s ∩ {b : α | a ≤ b}) ↔ set.unbounded has_le.le s
Less than #
theorem
set.bounded_lt_inter_not_lt
{α : Type u_1}
{s : set α}
[semilattice_sup α]
(a : α) :
set.bounded has_lt.lt (s ∩ {b : α | ¬b < a}) ↔ set.bounded has_lt.lt s
theorem
set.unbounded_lt_inter_not_lt
{α : Type u_1}
{s : set α}
[semilattice_sup α]
(a : α) :
set.unbounded has_lt.lt (s ∩ {b : α | ¬b < a}) ↔ set.unbounded has_lt.lt s
theorem
set.bounded_lt_inter_le
{α : Type u_1}
{s : set α}
[linear_order α]
(a : α) :
set.bounded has_lt.lt (s ∩ {b : α | a ≤ b}) ↔ set.bounded has_lt.lt s
theorem
set.unbounded_lt_inter_le
{α : Type u_1}
{s : set α}
[linear_order α]
(a : α) :
set.unbounded has_lt.lt (s ∩ {b : α | a ≤ b}) ↔ set.unbounded has_lt.lt s
theorem
set.bounded_lt_inter_lt
{α : Type u_1}
{s : set α}
[linear_order α]
[no_max_order α]
(a : α) :
set.bounded has_lt.lt (s ∩ {b : α | a < b}) ↔ set.bounded has_lt.lt s
theorem
set.unbounded_lt_inter_lt
{α : Type u_1}
{s : set α}
[linear_order α]
[no_max_order α]
(a : α) :
set.unbounded has_lt.lt (s ∩ {b : α | a < b}) ↔ set.unbounded has_lt.lt s
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 : α) :
set.unbounded ge (s ∩ {b : α | ¬a ≤ b}) ↔ set.unbounded ge s
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