> I guess this is the end. Nice challenge, I enjoyed it. Nice, glad you liked it.
I also agree with Mario that it would be nice to have this in set.mm, in a mathbox or elsewhere. Gino has been mostly using theorem formulations which I suggested (apart from some d-conditions and superfluous hypotheses), but I often like Thierry's treatment better, since he reformulates theorems in a way which make them easier to use or to prove. Maybe in the end you could combine both efforts, and push a "mixed" version into set.mm where some theorems are double-credited like "contributed by GG and TA" or "contributed by GA, revised by TA" etc, where one could select "the best" approach in each case. -- 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 visit https://groups.google.com/d/msgid/metamath/10bc7d29-1790-4740-b5c7-54abf4f6cb40n%40googlegroups.com.
