Zulip Chat Archive

Do we really want a specialized def 𝔠 = ℶ_ 1? It seems to me that nearly all of the theorems in the file where docs#Cardinal.continuum is defined are just theorems about infinite cardinals. If we want simp to work nicely with them, we can just instantiate them as simp lemmas about docs#Cardinal.beth.

Floris van Doorn (Dec 18 2025 at 18:08):

Maybe 𝔠 can be scoped notation for ℶ_ 1?

Floris van Doorn (Dec 18 2025 at 18:09):

If we do that, I think we can remove the definition continuum. I think that's better than the status quo.

Violeta Hernández (Dec 18 2025 at 18:36):

That makes a lot of sense. We already have ℵ₁ as notation for ℵ_ 1, so this would just be the analog for beth.

Violeta Hernández (Dec 18 2025 at 18:49):

Although, why not have the notation ℶ₁ instead? This would be consistent with both ℵ₁ and ω₁, and means that we can use the name beth1 in theorems, rather than the longer continuum.

Violeta Hernández (Dec 18 2025 at 18:52):

The docstring can say something like "beth 1 is the cardinality of the continuum"

Artie Khovanov (Dec 18 2025 at 19:22):

Discoverability, right

Violeta Hernández (Dec 18 2025 at 19:25):

I'd argue ℶ₁ is even more discoverable than 𝔠 (pop quiz! How do you write 𝔠 into Lean?)

Violeta Hernández (Dec 18 2025 at 19:27):

Perhaps this is one of those situations where you make a poll to gauge public opinion

Violeta Hernández (Dec 18 2025 at 19:28):

/poll Which is better notation for ℶ_ 1 (the cardinality of ℝ)?
ℶ₁
𝔠

Violeta Hernández (Dec 18 2025 at 22:34):

re: the last option, I also bring this up because I'm assuming that this notation would impact how we write our theorems, in the same way that we use omega1 for ω₁. Or perhaps should we be writing omega_one instead?