Cardinal.continuum

Stream: mathlib4

[Violeta Hernández]

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]

Maybe 𝔠 can be scoped notation for ℶ_ 1?

[Floris van Doorn]

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

[Violeta Hernández]

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]

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]

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

[Artie Khovanov]

Discoverability, right

[Violeta Hernández]

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

[Violeta Hernández]

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

[Violeta Hernández]

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

[Violeta Hernández]

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?

[Yury G. Kudryashov]

I think that continuum is a more discoverable name.

[Violeta Hernández]

Alright then. Does that apply to theorem names as well?

[Yury G. Kudryashov]

I think, yes. I'm OK with turning this into a notation with a prescribed preferred name (I don't remember the exact syntax right now).

[Violeta Hernández]

recommended_spelling?

[Yury G. Kudryashov]

Also, I think that it's OK to remove (deprecate) theorems that duplicate theorems about beth.

[Yury G. Kudryashov]

If the docstring for the notation mentions both names.

[Violeta Hernández]

On a similar vein, I'd like to ask about ℵ₁. Some theorems about it write it as aleph_one (which corresponds to the fact that ℵ₁ is just notation for ℵ_ 1), while other theorems write it as aleph1 (in analogy to docs#Cardinal.aleph0). Which one should we use?

[Violeta Hernández]

/poll How do we write ℵ₁ in theorem names?
aleph_one
aleph1

[Violeta Hernández]

Alright, noted.

[Violeta Hernández]

I'm a bit sad to lose the nice visual symmetry in names like docs#Ordinal.omega0_lt_omega1, but I suppose consistent naming convention takes priority.

[Violeta Hernández]

#33198

[Jireh Loreaux]

@Violeta Hernández please run the same poll for aleph0 vs. aleph_zero.

[Violeta Hernández]

Just replied to you in that PR, but docs#Ordinal.omega0 (with notation ω) is a separate thing from ω_ 0.

[Jireh Loreaux]

Ah nevermind then

[Violeta Hernández]

The unfortunate fact is that math uses the name "omega" for both the first infinite ordinal and for the function which enumerates all the infinite ordinals, so the 0 in omega0 is more of a compromise.

[Jireh Loreaux]

So, here's a question. Do we really need docs#omega0 ? This is an honest question, as I'm not particularly familiar with this end of the library. Why not just have a theorem that has the same content as docs#Ordinal.omega_zero, but without the intermediate def?

[Violeta Hernández]

It is quite more difficult to define the isomorphism between Ordinal and Cardinal than it is to just define ω = type ℕ (· < ·).

[Jireh Loreaux]

Okay, I've merged it. I will note though that docs#omega0 also flies in the face of our naming conventions a bit, as it would likely be omegaZero if it followed them. But I'm not going to push hard for it at this point.

[Violeta Hernández]

There's also docs#Cardinal.aleph0 if someone ever wants to fix this inconsistency (I sure don't)

[Jireh Loreaux]

You don't want to do the work (makes sense), or you think it would be a bad choice to change it?

[Violeta Hernández]

The longer name doesn't add clarity and the keystrokes add up. I'd personally prefer to keep the name as it is, but perhaps I'm in the minority, and it's not like I'm in a position of power here.