Thanks Theirry, sounds like a good plan. I proved this today as a first step towards itgsplit, does anyone have suggestions for a better name for it than splitrr, or should it be rrsplit? Also does this result already exist and I couldn't find it?
splitrr.1 $e |- Q e. RR $. splitrr.2 $e |- R = ( -oo (,] Q ) $. splitrr.3 $e |- S = ( Q [,) +oo ) $. splitrr $p |- RR = ( R u. S ) $= Full text here <https://pastebin.com/pTbXanej> if interested. -- 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/e19fae0b-6fc3-481f-bce0-4cf22be6e4ad%40googlegroups.com.
