Infinitude of intervals

Bounded intervals in dense orders are infinite, as are unbounded intervals in orders that are unbounded on the appropriate side.

theorem set.Ioo.infinite {α : Type u_1} [preorder α] [densely_ordered α] {a b : α} (h : a < b) :

theorem set.Ico.infinite {α : Type u_1} [preorder α] [densely_ordered α] {a b : α} (h : a < b) :

theorem set.Ioc.infinite {α : Type u_1} [preorder α] [densely_ordered α] {a b : α} (h : a < b) :

theorem set.Icc.infinite {α : Type u_1} [preorder α] [densely_ordered α] {a b : α} (h : a < b) :

theorem set.Iio.infinite {α : Type u_1} [preorder α] [no_bot_order α] {b : α} :

theorem set.Iic.infinite {α : Type u_1} [preorder α] [no_bot_order α] {b : α} :

theorem set.Ioi.infinite {α : Type u_1} [preorder α] [no_top_order α] {a : α} :

theorem set.Ici.infinite {α : Type u_1} [preorder α] [no_top_order α] {a : α} :