I was thinking about something like this: https://pastebin.com/SFyGskvW
But then I found that this misses the ~ ioounsn. ;-) I'd suggest to make your theorem slightly more generic, like |- ( ( ( A e. RR* /\ B e. RR /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,] B ) u. ( B [,) C ) ) = ( A (,) C ) ) Then it is in the form of the other theorems and could be named e.g. ~ iocunico. Sorry for the short post answering to my own post! On 06/06/2019 19:06, Thierry Arnoux wrote:
Hi Jon, Looks good, though it probably would have been shorter with ~ ioojoin or some similar theorem. _ Thierry Le 6 juin 2019 à 17:57, Jon P <[email protected] <mailto:[email protected]>> a écrit :
-- 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/8693d812-5755-b333-f0f9-1e89308b154b%40gmx.net.
