refactor(set_theory/cardinal/basic): constrain universes #15041
Conversation
vihdzp
added
awaiting-review
vihdzp
changed the title
github-actions
bot
removed
the
awaiting-CI
|
LGTM but let's wait for one more pair of eyes: I don't want to make decisions about universe-related questions by myself. |
|
Thanks! By the way, should I add a library note explaining the changes here? |
|
Yes. |
We introduce dot notation lemmas for proving something of the form `type r < type s` or `type r ≤ type s` by providing a principal segment, an initial segment, or a relation embedding. We rename `type_le` and `type_le'` to `type_le_iff` and `type_le_iff'` for consistency with `type_lt_iff` (which can't be renamed to `type_lt`, as this is an existing theorem about `type (<)`). We could introduce `lift` variants of these, but I'd rather wait until #15041 is merged, at which point I can do the analogous refactor on ordinals.
We introduce dot notation lemmas for proving something of the form `type r < type s` or `type r ≤ type s` by providing a principal segment, an initial segment, or a relation embedding. We rename `type_le` and `type_le'` to `type_le_iff` and `type_le_iff'` for consistency with `type_lt_iff` (which can't be renamed to `type_lt`, as this is an existing theorem about `type (<)`). We could introduce `lift` variants of these, but I'd rather wait until #15041 is merged, at which point I can do the analogous refactor on ordinals.
|
Sorry this has taken a long time. I am skeptical about the loss of generality, but if you can convince someone who know about the cardinal library I'm not going to object. In the meantime, there are now merge conflicts with master. If you'd still like to proceed with this, can you please merge master? |
semorrison
added
awaiting-author
vihdzp
added
awaiting-review
|
The recent renaming of vector space dimension theorems caused some annoying merge conflicts, but they seem to be fixed now. |
1 similar comment
|
The recent renaming of vector space dimension theorems caused some annoying merge conflicts, but they seem to be fixed now. |
|
Apologies, my ongoing dimension refactor has created a few more conflicts, hopefully minor. |
|
CI is failing |
The former changes were cribbed from leanprover-community/mathlib#15041
|
CI passes now. If we want this before the mathlib4 port of the vector space files it's probably best to merge this before any other major changes to these files. |
|
maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
|
I think per https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/New.20policy.20regarding.20mathlib3.20PRs.20that.20touch.20ported.20files this can't be merged for now, unless there is some reason this is needed for porting to proceed. |
There was a problem hiding this comment.
There's a build error in this file
semorrison
added
the
too-late
We enforce a canonical way to compare cardinals
aandbof different universesuandv, namely to comparecardinal.lift.{v} aandcardinal.lift.{u} b. By doing this, we alleviate some of the universe hell going on withcardinal.lift.We rename
basis.mk_eq_dim''tobasis.mk_eq_dim', since the latter name was used for a non-complying theorem that has been purged.