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]> a écrit : > > 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 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. -- 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/5A535B23-7D1B-43BF-B602-C9590D8054F9%40gmx.net.
