The proof of icombl uses icombl1. In fact icombl1 isn't really even intended for general use, since icombl is strictly more general; icombl is proven by splitting the set into a difference of left-closed right-infinite sets which are measurable by icombl1.
iocmbl isn't proven mostly because right closed intervals are not that useful. Usually left closed intervals are just as good and they have all the theorems. On Tue, Jun 11, 2019 at 5:57 AM Jon P <[email protected]> wrote: > Awesome, thanks for the help :) > > I can find icombl <http://us.metamath.org/mpegif/icombl.html> and icombl1 > <http://us.metamath.org/mpegif/icombl1.html>but can't find iocmbl and > iocmbl1, am I right in thinking they don't exist? If so I could have a go > at cooking them up. > > Also I think maybe the proof of icombl1 could be shorted by using icombl. > I haven't shortened a proof before, would this be helpful? Do I just edit > the proof and then submit it? > > -- > 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/39fc1f70-e15f-4fd6-8c86-d69f14f424c5%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/39fc1f70-e15f-4fd6-8c86-d69f14f424c5%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSsaiGfxw8eD_rjEqWzgVGc64qO9WdjpWgKohrtTB7n3mg%40mail.gmail.com.
