Hiding lemmas on the website

[David Starner]

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.

[Norman Megill]

On Friday, January 24, 2020 at 11:50:54 AM UTC-5, David Starner wrote:

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?

The theorem list is created by 'write theorem_list', and by default that command does hide lemmas i.e. statements whose comment begins "Lemma for...".  I did it that way for reasons you mention, feeling that they cluttered up the theorem list which was supposed to be a summary.  (Another reason was that some lemmas are huge and caused the mpegif version to load painfully slowly in older browsers and computers.)  A link to the lemma along with its description is still provided, but it takes up much less space on the web page.

However, there were complaints about this because people wanted to see the math content of lemmas on the theorem list page.  So I added the qualifier '/show_lemmas' which is now used for the web site generation.

What I would suggest is that you download set.mm and metamath.exe (and optionally save the mmset.html web page into the directory to avoid bibliography warnings), then in metamath.exe type 'read set.mm' followed by 'write theorem_list /alt_html' to generate the theorem list locally with the math content of lemmas suppressed.

 

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".)

If a lemma is used for multiple proofs, it could be described as "Lemma for abc and xyz...", or perhaps it should just be a regular theorem.  Ultimately it is up to the original contributor to put meaningful commentary in the description.  But we do try to make incremental improvements over time and welcome suggestions for specific cases.

Norm