mathlib documentation

data.set.intervals.infinite

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 : α} :