-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(set_theory/ordinal_arithmetic): Coefficients of Cantor Normal Form #12681
Conversation
This PR/issue depends on: |
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@@ -2019,7 +2019,7 @@ by rw [CNF_rec, dif_neg o0] | |||
base-`b` expansion of `o`. | |||
|
|||
`CNF b (b ^ u₁ * v₁ + b ^ u₂ * v₂) = [(u₁, v₁), (u₂, v₂)]` -/ | |||
def CNF (b := omega) (o : ordinal) : list (ordinal × ordinal) := | |||
def CNF (b o : ordinal) : list (ordinal × ordinal) := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If you require that b
and o
have the same universe level in almost every property about CNF
, shouldn't you just require it in the definition of CNF
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It is required in the definition. But writing p ∈ ordinal × ordinal
seems to confuse the kernel, and it ends with all of my lemmas having everything in universe max ?1 ?2
instead of using a single universe. This is why I need the universe annotations.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh I see. Yeah, that sometimes happens. Thanks for the clarification!
Other than that point, this LGTM. bors d+ |
✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…rm (#12681) We prove all coefficients of the base-b expansion of an ordinal are less than `b`. We also tweak the parameters of various other theorems.
Pull request successfully merged into master. Build succeeded: |
…rm (#12681) We prove all coefficients of the base-b expansion of an ordinal are less than `b`. We also tweak the parameters of various other theorems.
…rm (#12681) We prove all coefficients of the base-b expansion of an ordinal are less than `b`. We also tweak the parameters of various other theorems.
…rm (#12681) We prove all coefficients of the base-b expansion of an ordinal are less than `b`. We also tweak the parameters of various other theorems.
We prove all coefficients of the base-b expansion of an ordinal are less than
b
. We also tweak the parameters of various other theorems.CNF_rec
#12680