intervals are infinite

Stream: Is there code for X?

[Reid Barton]

Does this already exist?

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]

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]

Could you please add type annotations to have and obtain?

[Yury G. Kudryashov]

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

[Reid Barton]

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

[Reid Barton]

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]

Sorry, I mean docs#conditionally_complete_lattice

[Floris van Doorn]

There is src#cardinal.mk_Ioo_real

[Floris van Doorn]

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

[Reid Barton]

I actually want not just real though

[Floris van Doorn]

Oh edit, nvm: this is for arbitrary dense orders

[Floris van Doorn]

Then it doesn't exist AFAIK.