Infinitude of intervals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

theorem no_max_order.infinite {α : Type u_1} [preorder α] [nonempty α] [no_max_order α] :

infinite α

A nonempty preorder with no maximal element is infinite. This is not an instance to avoid a cycle with infinite α → nontrivial α → nonempty α.

source

theorem no_min_order.infinite {α : Type u_1} [preorder α] [nonempty α] [no_min_order α] :

infinite α

A nonempty preorder with no minimal element is infinite. This is not an instance to avoid a cycle with infinite α → nontrivial α → nonempty α.

source

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

infinite ↥(set.Ioo a b)

source

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

(set.Ioo a b).infinite

source

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

(set.Ico a b).infinite

source

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

infinite ↥(set.Ico a b)

source

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

(set.Ioc a b).infinite

source

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

infinite ↥(set.Ioc a b)

source

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

(set.Icc a b).infinite

source

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

infinite ↥(set.Icc a b)

source

@[protected, instance]

def set.Iio.infinite {α : Type u_1} [preorder α] [no_min_order α] {a : α} :

infinite ↥(set.Iio a)

source

theorem set.Iio_infinite {α : Type u_1} [preorder α] [no_min_order α] (a : α) :

(set.Iio a).infinite

source

@[protected, instance]

def set.Iic.infinite {α : Type u_1} [preorder α] [no_min_order α] {a : α} :

infinite ↥(set.Iic a)

source

theorem set.Iic_infinite {α : Type u_1} [preorder α] [no_min_order α] (a : α) :

(set.Iic a).infinite

source

@[protected, instance]

def set.Ioi.infinite {α : Type u_1} [preorder α] [no_max_order α] {a : α} :

infinite ↥(set.Ioi a)

source

theorem set.Ioi_infinite {α : Type u_1} [preorder α] [no_max_order α] (a : α) :

(set.Ioi a).infinite

source

@[protected, instance]

def set.Ici.infinite {α : Type u_1} [preorder α] [no_max_order α] {a : α} :

infinite ↥(set.Ici a)

source

theorem set.Ici_infinite {α : Type u_1} [preorder α] [no_max_order α] (a : α) :

(set.Ici a).infinite