new Uncountable

[WenrongZou]

This planet after Iso. Introduce equivalent in this planet.

[TentativeConvert]

This level should come one or two levels earlier, so it's grouped together with the other levels that are exclusively about cardinality and not about linear algebra.

[TentativeConvert]

The biggest remaining issue regarding this planet is how to connect it to Cantor. The final level of Cantor should be rephrased as an Uncountability statement, somewhere. Options that come to mind:

• Cantor → RealUncountable: Give the final level of Cantor a name, insert a level here that deduces the uncountability of sequences ℕ → ℕ from that statement.
• Cantor → Cardinality → RealUncountable: Same as above, but make the first levels of this planet into a separate "Cardinality" planet, and keep only the linear algebra stuff in RealUncountable.
• Cardinality → Cantor, Cardinality → RealUncountable: Make the first levels of this planet into a separate "Cardinality" planet, and keep only the linear algebra stuff here. Rephrase Cantor's statement at the end of Cantor.

(I'm leaning towards the first option.)