omega < aleph (n+1)

Stream: Is there code for X?

[Joseph Hua]

Hi! I would like to have lemma omega_lt_aleph_one : ω < aleph 1 := sorry, or anything more general that implies it, or even any instance of a cardinal such ω is strictly less than it. Is this somewhere is mathlib?

[Eric Rodriguez]

docs#cardinal.omega_lt_continuum

[Eric Rodriguez]

also docs#cardinal.aleph_lt, as omega is aleph 0 I thnk

[Gabriel Ebner]

Indeed:

example : ω < aleph 1 := aleph_zero ▸ aleph_lt.2 ordinal.zero_lt_one

[Mario Carneiro]

I didn't know about cardinal.continuum, but I would argue that it should be defined as #real not 2^\omega

[Gabriel Ebner]

But those are the same? In set theory, the "reals" is usually $2^\omega$ or $\omega^\omega$ anyhow.

[Mario Carneiro]

yes they are the same, but that should be the theorem

[Mario Carneiro]

and yes I know that set theorists like to abuse this theorem terminologically

[Eric Rodriguez]

does Lean force an answer to it? I know we have flypitch but I thought that was metamathematical

[Mario Carneiro]

you can prove c = 2^omega in ZF

[Mario Carneiro]

it is c = aleph_1 that is independent

[Reid Barton]

I think we should probably use the set theorists's language to interpret definitions in set theory--isn't the $2^\omega$ definition the more useful one anyway?

[Reid Barton]

I mean, it doesn't matter much of course.

[Reid Barton]

(I realize "continuum" is then odd but I think that's a pre-existing oddity in math terminology)

[Mario Carneiro]

If the continuum file doesn't transitively import data.real.basic, then that is another argument for the set theorist's definition. Still, I want #real = c to at least be a theorem in the library

[Eric Rodriguez]

docs#cardinal.mk_real

[Joseph Hua]

Thanks all! omega_lt_continuum does the trick

[Sebastien Gouezel]

You also have exactly omega_lt_aleph_one in #12422 !

[Sebastien Gouezel]

Mario Carneiro said:

I didn't know about cardinal.continuum, but I would argue that it should be defined as #real not 2^\omega

When you compute with cardinals, the representation as 2^\omega is much easier to use.