Wow Theirry that is really cool :) Yeah nice theorem to have. Should it
maybe be itgexpd for deduction? Do you think it is wise to have both
versions or just the deduction one?
Re this:
h1::subarea.1 |- A e. dom area
h2::subarea.2 |- C C_ RR
h3::subarea.3 |- B = { <. x , y >. | ( <. x , y >. e. A /\ x e. C ) }
!qed:: |- B e. dom area
what I'm trying to do is use this with iocunico
<http://us.metamath.org/mpegif/iocunico.html> to split a triangle into two
halves. So for example C might be ( -oo (,] Q ) and just be the left half
of the triangle. So yeah B is only meant to be this left side. I am not so
sure whether your version does this, I am a bit confused.
I think it will be ok if C is some crazy set because at each point x e. C
the other properties of dmarea <http://us.metamath.org/mpegif/dmarea.html>
will hold, though I am sure I may well be wrong :)
Yeah I am happy to try to do it in deduction form :)
--
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/5726447e-153c-43d8-8e7b-4c20f270b3fb%40googlegroups.com.
