Add CCfld to iset.mm #4678
Merged
Add CCfld to iset.mm #4678
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Copied without change from set.mm
This is starvndxnbasendx , starvndxnplusgndx , and starvndxnmulrndx
Copied from set.mm. They are vscandxnbasendx , vscandxnplusgndx , vscandxnmulrndx , and vscandxnscandx
Copied from set.mm. This is ipndxnbasendx , ipndxnplusgndx , ipndxnmulrndx , and slotsdifipndx .
Copied from set.mm. These are plendxnn , basendxltplendx , plendxnbasendx , plendxnplusgndx , plendxnmulrndx , plendxnscandx , plendxnvscandx , and slotsdifplendx
Copied without change from set.mm. They are unifndx , unifid , unifndxnn , basendxltunifndx , unifndxnbasendx , unifndxntsetndx , and slotsdifunifndx Update iset-discouraged
Specifically, remove references to theorems which iset.mm does not have from various comments brought in with slot theorems.
Extending the upper range of a structure.
This is the syntax and df-icnfld . df-icnfld is based on df-cnfld from set.mm but with only the first 4 slots (at least for now), because showing existence of the sets for the other slots depends on theorems we haven't proved yet at this point in the file. Add cnfldstr to iset.mm . Stated as in set.mm. The proof is based on a portion of the set.mm proof. Update iset-discouraged file.
Stated as in set.mm. The proof needs a bit of intuitionizing but is basically the set.mm proof.
Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof.
Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof.
Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof.
This is cnfldtset , cnfldle , cnfldds , cnfldunif , and cnfldfun .
avekens
approved these changes
Feb 27, 2025
icecream17
approved these changes
Feb 28, 2025
tirix
approved these changes
Feb 28, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
After looking into what closure theorems would be needed for the whole structure as defined in set.mm, it seems like at least for now the best plan is to stick with the first four slots (base, addition, multiplication, and conjugate, that is the ones needed for up to a star ring). Because of the way extensible structures work, we can revisit this later if feasible/desirable, without affecting theorems which just use those four slots.
But as for those four slots, this stays pretty close to how set.mm handles them, with a little intuitionizing needed here and there.