## Stream: Is there code for X?

### Topic: intervals are infinite

#### Reid Barton (Aug 06 2020 at 17:43):

import data.set.finite

lemma Ioo.infinite {α : Type*} [preorder α] [densely_ordered α] (a b : α) (h : a < b) :
set.infinite (set.Ioo a b) :=
sorry


(edited for truth)

#### Reid Barton (Aug 06 2020 at 18:04):

I'm pretty sure the answer is no, and I proved it with undue difficulty:

lemma Ioo.infinite [preorder α] [densely_ordered α] {x y : α} (h : x < y) :
infinite (Ioo x y) :=
begin
obtain ⟨c, hc₁, hc₂⟩ := dense h,
intro f,
letI := f.fintype,
have := fintype.well_founded_of_trans_of_irrefl ((<) : Ioo x y → Ioo x y → Prop),
obtain ⟨m, _, hm⟩ := this.has_min univ ⟨⟨c, hc₁, hc₂⟩, trivial⟩,
obtain ⟨z, hz₁, hz₂⟩ := dense m.2.1,
refine hm ⟨z, hz₁, lt_trans hz₂ m.2.2⟩ trivial hz₂
end


#### Yury G. Kudryashov (Aug 06 2020 at 18:19):

Another similar question: in case of a conditionally compete order the cardinality is at least the cardinality of 2^nat

#### Reid Barton (Aug 06 2020 at 18:43):

A bold assumption that I can figure out what the types actually are :upside_down:

#### Reid Barton (Aug 06 2020 at 18:46):

Did you know you can put a _ where I have one on the m line?

lemma Ioo.infinite [preorder α] [densely_ordered α] {x y : α} (h : x < y) :
infinite (Ioo x y) :=
begin
obtain ⟨c, hc₁, hc₂⟩ : ∃ c : α, x < c ∧ c < y := dense h,
intro f,
letI := f.fintype,
have : well_founded ((<) : Ioo x y → Ioo x y → Prop) :=
fintype.well_founded_of_trans_of_irrefl _,
obtain ⟨m, _, hm⟩ : ∃ (m : Ioo x y) _, ∀ d ∈ univ, ¬ d < m := this.has_min univ ⟨⟨c, hc₁, hc₂⟩, trivial⟩,
obtain ⟨z, hz₁, hz₂⟩ : ∃ (z : α), x < z ∧ z < m := dense m.2.1,
refine hm ⟨z, hz₁, lt_trans hz₂ m.2.2⟩ trivial hz₂
end


#### Yury G. Kudryashov (Aug 06 2020 at 19:10):

Sorry, I mean docs#conditionally_complete_lattice

#### Floris van Doorn (Aug 06 2020 at 19:36):

There is src#cardinal.mk_Ioo_real

#### Floris van Doorn (Aug 06 2020 at 19:37):

Together with src#cardinal.infinite_iff and src#cardinal.cantor you got it.

#### Reid Barton (Aug 06 2020 at 19:38):

I actually want not just real though

#### Floris van Doorn (Aug 06 2020 at 19:38):

Oh edit, nvm: this is for arbitrary dense orders

#### Floris van Doorn (Aug 06 2020 at 19:39):

Then it doesn't exist AFAIK.

Last updated: May 17 2021 at 16:26 UTC