Intuitionize structure restriction #4591
Merged
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
This is similar to df-ress from set.mm but only includes the non-trivial case. Given reasonable conditions (for example those in strsetsid ) the two cases give the same results, and df-ress is infeasible in iset.mm because it wouldn't typically be easy to show that ( Base ` w ) C_ x is decidable. Remove df-ress from iset.mm; as described above it would be hard to work with and would not have any of the advantages it has in set.mm. - Add ressvalsets to iset.mm This is similar to ressval in set.mm but adjusted for the difference between set.mm's df-ress and iset.mm's df-iress . - Add ressex to iset.mm This replaces ovex but for |`s - Add ressval2 to iset.mm Stated as in set.mm but the proof in iset.mm is trivial from ressvalsets . (In fact, we retain ressval2 only for consistency with set.mm). - Add ressval3d to iset.mm Stated as in set.mm. The proof is pretty simple because of df-iress (and in fact does not need the Fun S and E e. dom S hypotheses, but they are kept for consistency with set.mm). - Add ressid2 to mmil.html. Remove from iset.mm. - Add strressid to iset.mm This is ressid from set.mm with additional conditions on the structure. Replaces the ressid which had been in iset.mm which relied on the previous definition of structure restriction.
ressbasd is ressbas from set.mm with a W e. X condition added and put into deduction form. ressbas2d is ressbas2 from set.mm put into deduction form in a similar way to ressbas / ressbasd .
This is ressbasss from set.mm placed into deduction form and with set existence conditions added. The proof is similar to a portion of the set.mm proof.
This is resseqnbas from set.mm with some added conditions (similar to other structure restriction theorems). The proof is based on a portion of the set.mm proof. This replaces the theorem which was called resslem until recently.
Give the reason we don't have it (in light of df-iress ).
This is ressinbasd from set.mm, placed into deduction form and with an additional W e. V condition.
This is ressress from set.mm with an additional set existence condition. The proof is similar to a portion of the set.mm proof but is also moderately different especially in details.
This is ressabs from set.mm with an additional set existence condition. The proof is similar to the set.mm proof.
sctfn
approved these changes
Jan 22, 2025
| @@ -141768,11 +141768,13 @@ class of all (base sets of) groups is proper. (Contributed by Mario | |||
| defining a function using the base set and applying that, or explicitly | |||
| truncating the slot before use. | |||
|
|
|||
| (Credit for this operator goes to Mario Carneiro.) | |||
| (Credit for this operator, as well as the 2023 modification for iset.mm, | |||
| goes to Mario Carneiro.) | |||
There was a problem hiding this comment.
Well 2023 is when he proposed the modification and when I made the branch.
When several possible dates are just a few months apart, we have a practice of not worrying about it.
When they are a year and half apart, I'm not quite as sure. I think it is probably better to keep the date when I edited the file and copied the definition from a github comment into my branch (which is the 7-Oct-2023 currently in this pull request), but perhaps there are other ideas.
In the grand scheme of things (given the longevity of the metamath project and its hoped for future longevity), 2023 vs 2025 is still a somewhat small difference, but I can see how this is a bit more date skew than we encounter most of the time.
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.
This is the definition (revised version of https://us.metamath.org/mpeuni/df-ress.html as proposed in #3022 ) and the rest of the theorems in the section Extensible structures: Basic definitions. Most theorems require some change, but I think most of the additional conditions should be readily satisfied.