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.

instance NoMaxOrder.infinite {α : Type u_1} [Preorder α] [Nonempty α] [NoMaxOrder α] : Infinite α

A nonempty preorder with no maximal element is infinite.

Equations

• ⋯ = ⋯

instance NoMinOrder.infinite {α : Type u_1} [Preorder α] [Nonempty α] [NoMinOrder α] : Infinite α

A nonempty preorder with no minimal element is infinite.

Equations

• ⋯ = ⋯

theorem Set.Ioo.infinite {α : Type u_1} [Preorder α] [DenselyOrdered α] {a b : α} (h : a < b) : Infinite ↑(Set.Ioo a b)

theorem Set.Ioo_infinite {α : Type u_1} [Preorder α] [DenselyOrdered α] {a b : α} (h : a < b) : (Set.Ioo a b).Infinite

theorem Set.Ico_infinite {α : Type u_1} [Preorder α] [DenselyOrdered α] {a b : α} (h : a < b) : (Set.Ico a b).Infinite

theorem Set.Ico.infinite {α : Type u_1} [Preorder α] [DenselyOrdered α] {a b : α} (h : a < b) : Infinite ↑(Set.Ico a b)

theorem Set.Ioc_infinite {α : Type u_1} [Preorder α] [DenselyOrdered α] {a b : α} (h : a < b) : (Set.Ioc a b).Infinite

theorem Set.Ioc.infinite {α : Type u_1} [Preorder α] [DenselyOrdered α] {a b : α} (h : a < b) : Infinite ↑(Set.Ioc a b)

theorem Set.Icc_infinite {α : Type u_1} [Preorder α] [DenselyOrdered α] {a b : α} (h : a < b) : (Set.Icc a b).Infinite

theorem Set.Icc.infinite {α : Type u_1} [Preorder α] [DenselyOrdered α] {a b : α} (h : a < b) : Infinite ↑(Set.Icc a b)

instance Set.instInfiniteElemIioOfNoMinOrder {α : Type u_1} [Preorder α] [NoMinOrder α] {a : α} : Infinite ↑(Set.Iio a)

Equations

• ⋯ = ⋯

theorem Set.Iio_infinite {α : Type u_1} [Preorder α] [NoMinOrder α] (a : α) : (Set.Iio a).Infinite

instance Set.instInfiniteElemIicOfNoMinOrder {α : Type u_1} [Preorder α] [NoMinOrder α] {a : α} : Infinite ↑(Set.Iic a)

Equations

• ⋯ = ⋯

theorem Set.Iic_infinite {α : Type u_1} [Preorder α] [NoMinOrder α] (a : α) : (Set.Iic a).Infinite

instance Set.instInfiniteElemIoiOfNoMaxOrder {α : Type u_1} [Preorder α] [NoMaxOrder α] {a : α} : Infinite ↑(Set.Ioi a)

Equations

• ⋯ = ⋯

theorem Set.Ioi_infinite {α : Type u_1} [Preorder α] [NoMaxOrder α] (a : α) : (Set.Ioi a).Infinite

instance Set.instInfiniteElemIciOfNoMaxOrder {α : Type u_1} [Preorder α] [NoMaxOrder α] {a : α} : Infinite ↑(Set.Ici a)

Equations

• ⋯ = ⋯

theorem Set.Ici_infinite {α : Type u_1} [Preorder α] [NoMaxOrder α] (a : α) : (Set.Ici a).Infinite