Zulip Chat Archive

Stream: general

Topic: Type is uncountable


view this post on Zulip Kenny Lau (Apr 08 2020 at 13:28):

@Mario Carneiro did you prove that Type is uncountable?

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:29):

I proved it's inaccessible, so it is greater than omega and hence uncountable

view this post on Zulip Kenny Lau (Apr 08 2020 at 13:29):

is it in mathlib?

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:29):

yes

view this post on Zulip Kenny Lau (Apr 08 2020 at 13:30):

where can I find it?

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:31):

somewhere in set_theory.cofinality

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:32):

It is one of the conjuncts of univ_inaccessible

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:33):

the proof is apparently by simpa using lift_lt_univ' omega

view this post on Zulip Kenny Lau (Apr 08 2020 at 13:35):

https://leanprover-community.github.io/mathlib_docs/set_theory/cofinality.html#cardinal.univ_inaccessible

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:36):

Oh, actually univ is defined to be the cardinal of ordinal, not the cardinal of Type, so maybe there is a bit more to prove

view this post on Zulip Chris Hughes (Apr 08 2020 at 15:45):

There's a proof in ordinal that every type embeds into Type, or maybe cardinal. It's part of the proof of the well ordering theorem.


Last updated: May 16 2021 at 05:21 UTC