Added more useful theorems about UpWords

[ProgramCrafter]

Used and promoted four mathbox theorems:

1. bj-issetiv -> issetiv. An element of a class exists, inference version, by BJ.
2. leltletr. Weak transitive law for ordering on reals, by AV.
3. fzindd. Induction on the integers from M to N inclusive, a deduction version, by metakunt.
4. elfzop1le2. A member in a half-open integer interval plus 1 is less than or equal to the upper bound, by Glauco Siliprandi.

I believe I've found a suitable section for each of them so that the theorems would thematically fit with surrounding ones.

---

Also, Metamath-exe somewhy refused to rewrap theorems' hypotheses; I wrapped those manually, we shall see if I did that correctly...

[avekens]

see inline comments

[icecream17]

add

22-Nov-24 bj-issetiv issetiv    moved from BJ's mathbox to main set.mm

to changes-set.txt

example: 1843f4e

---

Note: I'm not sure on how bj-isseti should be handled, so I think the comment of bj-isseti can stand, and a future edit could be combined with a shortening of isseti. Though note bj-isseti does not use extra axioms (only + df-clab)

It might be useful in the future to prove isupword a la https://us.metamath.org/mpeuni/isgrp.html

[icecream17]

@avekens the inline comments do not seem to be published

(oops I probably duplicated the changes-set change, oh well)

[avekens]

@avekens the inline comments do not seem to be published

Sorry, I think I forgot to push the "Add comment" button. My inline comment is available now.

[avekens]

My request to push back ~issetiv (as ~bj-issetiv) into the BJ's mathbox, and to use ~isseti in the proof of ~tworepnotupword instead is not taken into account yet.

[ProgramCrafter]

I've read that there is no theorem |- -. A < A (ltneverrefl) for a reason that subsequent theorems should specify their domain. Is naming it to "et-ltneverrefl" and adding a "(New usage is discouraged.)" tag a workable course of action?

[icecream17]

yes (rename is optional) (If renaming, note that ltneverrefl is inconsistent with ~ ltnri. Admittedly, ltnri is a relatively incomprehensible label, so this is also optional)

[ProgramCrafter]

More and more to know... that's interesting, actually)
While we are at it: how to define TeX rendering for my UpWord class? Right now, metamath.tirix.org only shows "Could not format assertion : No typesetting found for |- (/) e. UpWord S with typecode |-".

[avekens]

Fine for me now.

[avekens]

More and more to know... that's interesting, actually) While we are at it: how to define TeX rendering for my UpWord class? Right now, metamath.tirix.org only shows "Could not format assertion : No typesetting found for |- (/) e. UpWord S with typecode |-".

The typesetting definitions for UpWord seem to be OK:

htmldef "UpWord" as "UpWord";
  althtmldef "UpWord" as "UpWord";
  latexdef "UpWord" as "\mathrm{UpWord}";

The message complains about "|-", doesn't it? That's strange. @tirix do yo have any idea?

By the way, a space character at the end would result in a nicer HTML represenation (currently "⊢ ∅ ∈ UpWord𝑆"):

htmldef "UpWord" as "UpWord ";
  althtmldef "UpWord" as "UpWord ";
  latexdef "UpWord" as "\mathrm{UpWord}";

would result in "⊢ ∅ ∈ UpWord 𝑆"

Compare with the typesetting for Slot ("class Slot 𝐴"):

htmldef "Slot" as "Slot ";
  althtmldef "Slot" as "Slot ";
  latexdef "Slot" as "\mathrm{Slot}";

[tirix]

More and more to know... that's interesting, actually) While we are at it: how to define TeX rendering for my UpWord class? Right now, metamath.tirix.org only shows "Could not format assertion : No typesetting found for |- (/) e. UpWord S with typecode |-".

The message complains about "|-", doesn't it? That's strange. @tirix do yo have any idea?

The formatting information for metamath.tirix.org is not provided in the main set.mm file, but in set-mathml.mmts. The error warns that typesetting information is missing for the whole expression, actually. Maybe it could be phrased a bit better. It should be easy to add a new symbol by mimicking other entries there.

That file does not provide translations math token by math token (i.e. for just UpWord), but for syntactic expressions instead (i.e. for class UpWord).

I'm not keeping up regularly with new math syntax, but instead updating the file in batch from time to time. One way to ensure that it's up to date would be to add a check to the CI. Our CI is already quite strict, but on the other hand it includes some TeX checks which might be less used than metamath.tirix.org?

(BTW I see the site SSL certificate has expired, I'll see to renew it!)

[GinoGiotto]

One way to ensure that it's up to date would be to add a check to the CI. Our CI is already quite strict, but on the other hand it includes some TeX checks which might be less used than metamath.tirix.org?

Adding CI might be worth it. I visit metamath.tirix.org regularly and I would like to see the website become more relevant in the future. I believe the modern design and TeX rendering have the potential to attract more people that are curious about metamath.

[digama0]

I do think that the no-js restriction is too limiting for metamath.org. I've been trying to move the website to something more modern for ages but it's difficult to get people to thumbs up a plan; or at least that was my impression last time we discussed it on the mailing list.

[tirix]

Adding CI might be worth it. I visit metamath.tirix.org regularly and I would like to see the website become more relevant in the future. I believe the modern design and TeX rendering have the potential to attract more people that are curious about metamath.

OK, I should be able to propose a CI change for that.

[david-a-wheeler]

Just to be clear, I never said "no-JS" in 2023. What I said was:

What I want is for a way for people to access the basic information without requiring client-side JavaScript. I see no reason that it be the only way we provide the information, we already provide it in multiple forms. I just want to retain that capability. So you don't need to feel held back :-).
...
As far as speed goes, JavaScript is often slower than HTML where both can be used. In practice JavaScript files are often quite large, and JavaScript has to be parsed, examined, executed, and then its execution must cause document tree changes which finally get rendered. Web browsers are really good at rapidly & progressively rendering HTML. On systems I've worked with, HTML (even with server roundtrips) is often MUCH faster when measuring paint-to-screen times. JavaScript has gotten faster over the years, thankfully, but the gap is still large. Of course, when you need functionalities only provided by JavaScript then you need it. Like all technologies there are tradeoffs.

However, as this isn't really about UpWords, this topic should be discussed in its own issue or the mailing list.

[ProgramCrafter]

Hello! Just a reminder: I think this PR is ready for merging; style changes for "UpWord " and etc would certainly belong to next ones.

[avekens]

@ProgramCrafter please move you mathbox between "Mathbox for Saveliy Skresanov" and "Mathbox for Jarvin Udandy" with your next PR, bacause we order the mathbox alphabetically (by surname). So the contents should look like the following:

  20.38  Mathbox for Saveliy Skresanov
  20.39  Mathbox for Ender Ting
  20.40  Mathbox for Jarvin Udandy
  20.41  Mathbox for Adhemar (???)
  20.42  Mathbox for Alexander van der Vekens
  20.43  Mathbox for Zhi Wang
  20.44  Mathbox for Emmett Weisz
  20.45  Mathbox for David A. Wheeler
  20.46  Mathbox for Kunhao Zheng