Deprecate `ord_aleph'_eq_enum_card`

Stream: mathlib4

[Violeta Hernández]

I'm currently trying to refactor docs#Ordinal.enumOrd, but I'm unsure about what to do with these theorems docs#Cardinal.ord_aleph'_eq_enum_card and docs#Cardinal.ord_aleph_eq_enum_card.

[Violeta Hernández]

The issue is that I feel like there's more than one change that needs to happen to these lemmas:

• They should be written in terms of the (not yet in Mathlib) ω function, rather than ord ⚬ aleph
• They should use some IsInitial predicate (also not yet in Mathlib), rather than the odd spelling o.card.ord = o

And this is adding to my planned enumOrd refactor, which would replace Unbounded (· < ·) in the auxiliary lemmas above with ¬ BddAbove

[Violeta Hernández]

Adding onto this, another one of my planned refactors is to define the ω function as the enumerator function of initial ordinals. This should lead to the much cleaner definition of aleph as card ⚬ omega (the current definition basically proves the existence of the enumerator function from scratch).

[Violeta Hernández]

So, at the end of this series of refactors, these lemmas wouldn't even be needed.

[Violeta Hernández]

And as a final point - I don't even think these lemmas are very useful to begin with? "ord ⚬ aleph' enumerates the initial ordinals" amounts to saying the function is strictly monotonic and its range is the initial ordinals. Both of these have simpler spellings.

[Violeta Hernández]

Is it ok if I simply deprecate this whole series of lemmas, even if there's no direct replacement?

[Violeta Hernández]

cc. @Nir Paz

[Nir Paz]

I think just deprecating them is alright. I guess it might not be the "safest" way to do this, but with how big and overarching the current refactors are in the set theory library, I don't think we should put a lot of extra work into this for the nonexistent chance these lemmas will be needed for something in the couple of weeks before everything they talk about changes anyways.

[Nir Paz]

Maybe people who were involved in big refactors like these ones have a more informed opinion

[Violeta Hernández]

FYI I've opened a GitHub issue keeping track of all the refactors currently underway: #17033

[Nir Paz]

Violeta Hernández said:

FYI I've opened a GitHub issue keeping track of all the refactors currently underway: #17033

Terrifying.

[Violeta Hernández]

Yeah... there's a lot of piled up technical debt.

[Violeta Hernández]

(and I'm responsible for most of it :sweat_smile:)

[Nir Paz]

Is there a notion of supremum I'm missing, or is the idea to get rid of everything except iSup (and the def same sSup)?

[Violeta Hernández]

That's basically it, yes.

[Violeta Hernández]

I still think lsub can maybe be useful if it's generalized to conditionally complete lattices with a successor. But the amount of API that would be required to have that at the same level of functionality as iSup is probably too much to be worth it when you can type the definition out explicitly.

[Nir Paz]

Violeta Hernández said:

(and I'm responsible for most of it :sweat_smile:)

Well without you we'd have a lot less set theory, so you're excused xD

[Violeta Hernández]

I've opened a PR for this deprecation #17077 by the way. Worth noting these lemmas are all unused throughout the rest of Mathlib.