Zulip Chat Archive
Stream: general
Topic: Type is uncountable
Kenny Lau (Apr 08 2020 at 13:28):
@Mario Carneiro did you prove that Type is uncountable?
Mario Carneiro (Apr 08 2020 at 13:29):
I proved it's inaccessible, so it is greater than omega and hence uncountable
Kenny Lau (Apr 08 2020 at 13:29):
is it in mathlib?
Mario Carneiro (Apr 08 2020 at 13:29):
yes
Kenny Lau (Apr 08 2020 at 13:30):
where can I find it?
Mario Carneiro (Apr 08 2020 at 13:31):
somewhere in set_theory.cofinality
Mario Carneiro (Apr 08 2020 at 13:32):
It is one of the conjuncts of univ_inaccessible
Mario Carneiro (Apr 08 2020 at 13:33):
the proof is apparently by simpa using lift_lt_univ' omega
Kenny Lau (Apr 08 2020 at 13:35):
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
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: Dec 20 2023 at 11:08 UTC