Infinitude of intervals #
Bounded intervals in dense orders are infinite, as are unbounded intervals in orders that are unbounded on the appropriate side. We also prove that an unbounded preorder is an infinite type.
A nonempty preorder with no maximal element is infinite. This is not an instance to avoid
a cycle with Infinite α → Nontrivial α → Nonempty α.
A nonempty preorder with no minimal element is infinite. This is not an instance to avoid
a cycle with Infinite α → Nontrivial α → Nonempty α.
theorem
Set.Ioo.infinite
{α : Type u_1}
[Preorder α]
[DenselyOrdered α]
{a : α}
{b : α}
(h : a < b)
:
theorem
Set.Ioo_infinite
{α : Type u_1}
[Preorder α]
[DenselyOrdered α]
{a : α}
{b : α}
(h : a < b)
:
Set.Infinite (Set.Ioo a b)
theorem
Set.Ico_infinite
{α : Type u_1}
[Preorder α]
[DenselyOrdered α]
{a : α}
{b : α}
(h : a < b)
:
Set.Infinite (Set.Ico a b)
theorem
Set.Ico.infinite
{α : Type u_1}
[Preorder α]
[DenselyOrdered α]
{a : α}
{b : α}
(h : a < b)
:
theorem
Set.Ioc_infinite
{α : Type u_1}
[Preorder α]
[DenselyOrdered α]
{a : α}
{b : α}
(h : a < b)
:
Set.Infinite (Set.Ioc a b)
theorem
Set.Ioc.infinite
{α : Type u_1}
[Preorder α]
[DenselyOrdered α]
{a : α}
{b : α}
(h : a < b)
:
theorem
Set.Icc_infinite
{α : Type u_1}
[Preorder α]
[DenselyOrdered α]
{a : α}
{b : α}
(h : a < b)
:
Set.Infinite (Set.Icc a b)
theorem
Set.Icc.infinite
{α : Type u_1}
[Preorder α]
[DenselyOrdered α]
{a : α}
{b : α}
(h : a < b)
:
Equations
- ⋯ = ⋯
theorem
Set.Iio_infinite
{α : Type u_1}
[Preorder α]
[NoMinOrder α]
(a : α)
:
Set.Infinite (Set.Iio a)
Equations
- ⋯ = ⋯
theorem
Set.Iic_infinite
{α : Type u_1}
[Preorder α]
[NoMinOrder α]
(a : α)
:
Set.Infinite (Set.Iic a)
Equations
- ⋯ = ⋯
theorem
Set.Ioi_infinite
{α : Type u_1}
[Preorder α]
[NoMaxOrder α]
(a : α)
:
Set.Infinite (Set.Ioi a)
Equations
- ⋯ = ⋯
theorem
Set.Ici_infinite
{α : Type u_1}
[Preorder α]
[NoMaxOrder α]
(a : α)
:
Set.Infinite (Set.Ici a)