-
Notifications
You must be signed in to change notification settings - Fork 88
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
sn-wcdeq, 19.8aw #4251
base: develop
Are you sure you want to change the base?
sn-wcdeq, 19.8aw #4251
Conversation
3rspcedvd replaced with 3rspcedvdw
df-resub $a |- -R = ( x e. RR , y e. RR |-> | ||
( iota_ z e. RR ( y + z ) = x ) ) $. | ||
$} | ||
|
||
${ | ||
$d x y z A $. $d x y z B $. | ||
$( Value of real subtraction, which is the (unique) real ` x ` such that | ||
` B + x = A ` . (Contributed by Steven Nguyen, 7-Jan-2022.) $) | ||
` B + x = A ` . (Contributed by Steven Nguyen, 7-Jan-2023.) $) | ||
resubval $p |- ( ( A e. RR /\ B e. RR ) -> | ||
( A -R B ) = ( iota_ x e. RR ( B + x ) = A ) ) $= |
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.
The proof is still very long. Maybe some theorems/lemmas can be extracted.
@@ -646216,6 +646216,13 @@ D Fn ( I ... ( M - 1 ) ) /\ | |||
( cvv cv wnel cab wcel vex elirrv nelir 2th abbi2i eqcomi ) BACZMDZAENABMBF | |||
NAGMMAHIJKL $. | |||
|
|||
$( Alternative to ~ wcdeq and ~ df-cdeq . This flattens the syntax | |||
representation ( wi ( weq vx vy ) wph ) to ( wcdeqALT vx vy wph ), |
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.
representation ( wi ( weq vx vy ) wph ) to ( wcdeqALT vx vy wph ), | |
representation ( wi ( weq vx vy ) wph ) to ( sn-wcdeq vx vy wph ), |
?
@@ -646216,6 +646216,13 @@ D Fn ( I ... ( M - 1 ) ) /\ | |||
( cvv cv wnel cab wcel vex elirrv nelir 2th abbi2i eqcomi ) BACZMDZAENABMBF | |||
NAGMMAHIJKL $. | |||
|
|||
$( Alternative to ~ wcdeq and ~ df-cdeq . This flattens the syntax | |||
representation ( wi ( weq vx vy ) wph ) to ( wcdeqALT vx vy wph ), | |||
accomplishing the stated purpose of ~ df-cleq . (Contributed by SN, |
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.
That does not really accomplish the purpose of df-cdeq (BTW, you wrote "df-cleq"). You could say it "illustrates the comment of df-cdeq". Overall, I find this theorem of dubious interest.
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 accomplishes what df-cdeq says it accomplishes: flattening the syntax tree
Resolves #4158
The changes are rather disjoint but it's small (+146-147, +18, +2-2) and gets rid of 3 misc todos.