## 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?

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):

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

#### 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: May 16 2021 at 05:21 UTC