I proved iocunico <https://pastebin.com/Nf7p4ry9>today so that is a nice
step forwards :) I'm hopeful using itgsplit to prove the following is now
possible. Not sure if I should prove R u. S = { Q } seperately.
50:: |- A e. dom area
51:: |- Q e. RR
52:: |- R = ( -oo (,] Q )
53:: |- S = ( Q [,) +oo )
54:: |- B = { <. x , y >. | ( <. x , y >. e. A /\ x e. R ) }
55:: |- C = { <. x , y >. | ( <. x , y >. e. A /\ x e. S ) }
QED:: ( area ` A ) = ( area ` B ) + ( area ` C )
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/679359f1-e8d2-4f93-a6f3-169ddb59c0fb%40googlegroups.com.
