Zulip Chat Archive

Stream: Is there code for X?

Topic: intervals are infinite


view this post on Zulip Reid Barton (Aug 06 2020 at 17:43):

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)

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Aug 06 2020 at 18:16):

Could you please add type annotations to have and obtain?

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 06 2020 at 18:43):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Aug 06 2020 at 19:10):

Sorry, I mean docs#conditionally_complete_lattice

view this post on Zulip Floris van Doorn (Aug 06 2020 at 19:36):

There is src#cardinal.mk_Ioo_real

view this post on Zulip Floris van Doorn (Aug 06 2020 at 19:37):

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

view this post on Zulip Reid Barton (Aug 06 2020 at 19:38):

I actually want not just real though

view this post on Zulip Floris van Doorn (Aug 06 2020 at 19:38):

Oh edit, nvm: this is for arbitrary dense orders

view this post on Zulip Floris van Doorn (Aug 06 2020 at 19:39):

Then it doesn't exist AFAIK.


Last updated: May 17 2021 at 16:26 UTC