When digging through the website theorem list, there's a number of times one comes upon one or more proofs just used that are just there to be lemmas for other proofs and have cryptic names. Wouldn't it be better if those weren't listed on the main theorem list? They'd still be listed from the proof that uses them. (And if they're used from multiple proofs, that should be a sign they need a better description than just "Lemma for x".)
-- Kie ekzistas vivo, ekzistas espero. -- 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/CAMZ%3Dzj654XD4tFUQMsp2fY9jQNWGCQjiNmGpxMaO3TV2GU%2Bg3g%40mail.gmail.com.
