Intuitionize product equality and bound variable theorems #3906
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.
Stated as in set.mm. The proof is similar to the set.mm proof with a few adjustments.
Stated as in set.mm. The proof is based on the iset.mm proof of sumeq2 .
There's no reason for it to reference sumeq2d rather than sumeq2 (I think it dates from a time when theorems were different and/or differently named).
The name sbco2v is for a (slightly) different theorem in set.mm so we'd like to free up that name for a theorem matching the set.mm one.
Stated as in set.mm but proved in terms of sbie , so it doesn't have the same axiom usage properties as in set.mm.
nfsbv is stated as in set.mm but proved in terms of nfsb (so it would not have similar axiom usage properties to set.mm). sbco2v is copied without change from set.mm except that text referring to axioms (which is unverified in iset.mm) is removed.
Copied without change from set.mm, except that comments related to axiom usage which are not true (at least not as-is) in iset.mm are removed.
Stated as in set.mm. The proof is similar to the set.mm proof but adjusted for the differences in the definition of prod_ .
Copied without change from set.mm.
Copied without change from set.mm
This is prodeq1i , prodeq2i , prodeq12i , prodeq1d , prodeq2d , prodeq2dv , prodeq2sdv , 2cprodeq2dv , prodeq12dv , and prodeq12rdv All are copied without change from set.mm.
avekens
reviewed
Apr 5, 2024
| ( vz cab wsb cv wcel sbco2v sbiev sbbii bitr3i df-clab 3bitr4i eqriv ) HA | ||
| CIZBDIZACHJZBDHJZHKZTLUDUALUBACDJZDHJUCACHDEMUEBDHABCDFGNOPAHCQBHDQRS $. | ||
| $} | ||
|
|
There was a problem hiding this comment.
Fair, following set.mm on most aspects of the comments should be fine (including contribution lines in particular - in most cases intuitionizing should receive no mention or a Revised line, rather than a brand new Contributed By).
But for iset.mm specific aspects also see #756 , #2460 and in general just giving these theorems the same attention as set.mm has gotten. As far as I know, https://us.metamath.org/ileuni/ax-bndl.html and https://us.metamath.org/ileuni/ax-i12.html play a similar role to https://us.metamath.org/mpeuni/ax-13.html and their usage could be reduced in similar ways. But no one has done that yet and so unless/until that happens, the comments do have that divergence to adjust to.
avekens
approved these changes
Apr 5, 2024
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 from
prodeq2wtoprodeq12rdv. The intuitionizing here is relatively straightforward, especially since it is much like the similar theorems for sums.Also includes updating a variety of theorems to reflect set.mm names, disjoint variable constraints, etc.