Mathlib.Order.Interval.Set.Infinite

NoMaxOrder.infinite instance

[Nonempty α] [NoMaxOrder α] : Infinite α

Full source

/-- A nonempty preorder with no maximal element is infinite. -/
instance NoMaxOrder.infinite [Nonempty α] [NoMaxOrder α] : Infinite α :=
  let ⟨f, hf⟩ := Nat.exists_strictMono α
  Infinite.of_injective f hf.injective

Nonempty Preorders without Maximal Elements are Infinite

Informal description

For any nonempty preorder $\alpha$ with no maximal element, the type $\alpha$ is infinite.

NoMinOrder.infinite instance

[Nonempty α] [NoMinOrder α] : Infinite α

Full source

/-- A nonempty preorder with no minimal element is infinite. -/
instance NoMinOrder.infinite [Nonempty α] [NoMinOrder α] : Infinite α :=
  @NoMaxOrder.infinite αᵒᵈ _ _ _

Nonempty Preorders without Minimal Elements are Infinite

Informal description

For any nonempty preorder $\alpha$ with no minimal element, the type $\alpha$ is infinite.

Set.Ioo.infinite theorem

: Infinite (Ioo a b)

Full source

theorem Ioo.infinite : Infinite (Ioo a b) :=
  @NoMaxOrder.infinite _ _ (nonempty_Ioo_subtype h) _

Infinitude of Open Intervals in Dense Orders

Informal description

For any elements $a$ and $b$ in a dense linear order, the open interval $(a, b)$ is infinite.

Set.Ioo_infinite theorem

: (Ioo a b).Infinite

Full source

theorem Ioo_infinite : (Ioo a b).Infinite :=
  infinite_coe_iff.1 <| Ioo.infinite h

Infinitude of Open Intervals in Dense Orders

Informal description

For any elements $a$ and $b$ in a dense linear order, the open interval $(a, b)$ is infinite.

Set.Ico_infinite theorem

: (Ico a b).Infinite

Full source

theorem Ico_infinite : (Ico a b).Infinite :=
  (Ioo_infinite h).mono Ioo_subset_Ico_self

Infinitude of Left-Closed Right-Open Intervals in Dense Orders

Informal description

For any elements $a$ and $b$ in a dense linear order, the left-closed right-open interval $[a, b)$ is infinite.

Set.Ico.infinite theorem

: Infinite (Ico a b)

Full source

theorem Ico.infinite : Infinite (Ico a b) :=
  infinite_coe_iff.2 <| Ico_infinite h

Infinitude of $[a, b)$ in Dense Orders

Informal description

For any elements $a$ and $b$ in a dense linear order, the left-closed right-open interval $[a, b)$ is infinite.

Set.Ioc_infinite theorem

: (Ioc a b).Infinite

Full source

theorem Ioc_infinite : (Ioc a b).Infinite :=
  (Ioo_infinite h).mono Ioo_subset_Ioc_self

Infinitude of Right-Half-Open Intervals in Dense Orders

Informal description

For any elements $a$ and $b$ in a dense linear order, the half-open interval $(a, b]$ is infinite.

Set.Ioc.infinite theorem

: Infinite (Ioc a b)

Full source

theorem Ioc.infinite : Infinite (Ioc a b) :=
  infinite_coe_iff.2 <| Ioc_infinite h

Infinitude of Right-Half-Open Intervals in Dense Orders

Informal description

For any elements $a$ and $b$ in a dense linear order, the half-open interval $(a, b]$ is infinite.

Set.Icc_infinite theorem

: (Icc a b).Infinite

Full source

theorem Icc_infinite : (Icc a b).Infinite :=
  (Ioo_infinite h).mono Ioo_subset_Icc_self

Infinitude of Closed Intervals in Dense Orders

Informal description

For any elements $a$ and $b$ in a dense linear order, the closed interval $[a, b]$ is infinite.

Set.Icc.infinite theorem

: Infinite (Icc a b)

Full source

theorem Icc.infinite : Infinite (Icc a b) :=
  infinite_coe_iff.2 <| Icc_infinite h

Infinitude of Closed Intervals in Dense Orders

Informal description

For any elements $a$ and $b$ in a dense linear order, the closed interval $[a, b]$ is infinite.

Set.instInfiniteElemIioOfNoMinOrder instance

[NoMinOrder α] {a : α} : Infinite (Iio a)

Full source

instance [NoMinOrder α] {a : α} : Infinite (Iio a) :=
  NoMinOrder.infinite

Open Intervals Below are Infinite in Orders Without Minimal Elements

Informal description

For any preorder $\alpha$ with no minimal element and any element $a \in \alpha$, the open interval $(-\infty, a)$ is infinite.

Set.Iio_infinite theorem

[NoMinOrder α] (a : α) : (Iio a).Infinite

Full source

theorem Iio_infinite [NoMinOrder α] (a : α) : (Iio a).Infinite :=
  infinite_coe_iff.1 inferInstance

Infinite Open Left Interval in No-Min-Order Preorders

Informal description

For any preorder $\alpha$ with no minimal element and any element $a \in \alpha$, the open interval $(-\infty, a)$ is infinite.

Set.instInfiniteElemIicOfNoMinOrder instance

[NoMinOrder α] {a : α} : Infinite (Iic a)

Full source

instance [NoMinOrder α] {a : α} : Infinite (Iic a) :=
  NoMinOrder.infinite

Closed Intervals Below are Infinite in NoMinOrder

Informal description

For any preorder $\alpha$ with no minimal element and any element $a \in \alpha$, the closed interval $(-\infty, a]$ is infinite.

Set.Iic_infinite theorem

[NoMinOrder α] (a : α) : (Iic a).Infinite

Full source

theorem Iic_infinite [NoMinOrder α] (a : α) : (Iic a).Infinite :=
  infinite_coe_iff.1 inferInstance

Infinite Closed Left Interval in No-Min-Order Preorders

Informal description

For any preorder $\alpha$ with no minimal element and any element $a \in \alpha$, the closed interval $(-\infty, a]$ is infinite.

Set.instInfiniteElemIoiOfNoMaxOrder instance

[NoMaxOrder α] {a : α} : Infinite (Ioi a)

Full source

instance [NoMaxOrder α] {a : α} : Infinite (Ioi a) :=
  NoMaxOrder.infinite

Open Intervals Above are Infinite in NoMaxOrder

Informal description

For any preorder $\alpha$ with no maximal element and any element $a \in \alpha$, the open interval $(a, \infty)$ is infinite.

Set.Ioi_infinite theorem

[NoMaxOrder α] (a : α) : (Ioi a).Infinite

Full source

theorem Ioi_infinite [NoMaxOrder α] (a : α) : (Ioi a).Infinite :=
  infinite_coe_iff.1 inferInstance

Open Intervals Above are Infinite in NoMaxOrder Preorders

Informal description

For any preorder $\alpha$ with no maximal element and any element $a \in \alpha$, the open interval $(a, \infty)$ is infinite.

Set.instInfiniteElemIciOfNoMaxOrder instance

[NoMaxOrder α] {a : α} : Infinite (Ici a)

Full source

instance [NoMaxOrder α] {a : α} : Infinite (Ici a) :=
  NoMaxOrder.infinite

Closed Intervals are Infinite in NoMaxOrder Preorders

Informal description

For any preorder $\alpha$ with no maximal element and any element $a \in \alpha$, the closed interval $[a, \infty)$ is infinite.

Set.Ici_infinite theorem

[NoMaxOrder α] (a : α) : (Ici a).Infinite

Full source

theorem Ici_infinite [NoMaxOrder α] (a : α) : (Ici a).Infinite :=
  infinite_coe_iff.1 inferInstance

Infinite Closed Interval in NoMaxOrder Preorder

Informal description

For any preorder $\alpha$ with no maximal element and any element $a \in \alpha$, the closed interval $[a, \infty)$ is infinite.