Misc

[GinoGiotto]

• Added $j tags to relevant recently edited theorems¹² to ensure they remain ax-13 free.

• Apply consistency in label naming: in my first PR about adding DV¹ the original theorems were renamed as *ALT, while in the second one² they were renamed as *g. In this PR, I've renamed the *ALT versions of the first PR¹ to *g for uniformity (and adapted their comments).

• Updated changes-set.txt to document the renaming of original versions of the first PR¹ to *g. Given the brief existence of the *ALT versions, I believe we can consider the original theorems directly converted to *g, without explicitly mentioning their temporary existence as *ALT.

• Added proposed label renamings in changes-set.txt that better match established conventions. While I don't plan to implement these renamings anytime soon, this inclusion ensures they won't be forgotten. As wlammen said, in the end you can have both: reduced axiom usage and a label naming that suits the current practice. I welcome anyone willing to take up the renaming task.

Footnotes

1. First PR about adding DV conditions: https://github.com/metamath/set.mm/pull/3778 ↩ ↩² ↩³ ↩⁴

2. Second PR about adding DV conditions: https://github.com/metamath/set.mm/pull/3781 ↩ ↩²

[benjub]

I second @wlammen's remark, and provided you address it, I approve.

[GinoGiotto]

Sorry for the corrections, it should be good now.