On Sun, 30 Aug 2020 08:06:35 -0700 (PDT), "'Alexander van der Vekens' via
Metamath" wrote:
> Since most of the people have objections against using the same (looking)
> HTML-representation of two different symbols, I will change it. I think
> Mario's proposal using underlining is a good
Since most of the people have objections against using the same (looking)
HTML-representation of two different symbols, I will change it. I think
Mario's proposal using underlining is a good solution. This will result in
the following typesetting definition for the symbol ` _lcm `.
htmldef
Well, those are counterexamples to the claim that every syntax constructor
uses a unique symbol, but they are not counterexamples to the claim that
the mapping from ascii token to HTML display is injective, and until now
this property has been maintained, in some cases even when this goes
against
On Sunday, August 30, 2020 at 9:38:20 AM UTC-4 Norman Megill wrote:
...
> Up to now we have been careful not to overload the displayed symbols (to
> my knowledge). For example, we distinguish various kinds of "+" with
> subscripts, unlike most of the literature (which has a different and
>
On Sunday, August 30, 2020 at 4:53:58 AM UTC-4 Alexander van der Vekens
wrote:
>
> By the way, it seems a little confusing at the first glance that the least
> common multiple
> is defined by a supremum. Actually, it is an infimum, because the inverse
> of
> "less than" ` ``' < ` is used to
On Sunday, August 30, 2020 at 4:53:58 AM UTC-4 Alexander van der Vekens
wrote:
>
> In my latest PR, I provided a function mapping a set of integers to their
> least common multiple (~df-lcmf: ( _lcm `` s ) ) in addition to the
> operation calculating the least common multiple of two integers
>For the typesetting, however, I used the same representation "lcm" for
>both
>symbols ` lcm ` and ` _lcm ` - because it is clear by the context which
>definition is used.
I would prefer that there be a typographic way to distinguish them, though it's
fine if the distinguishing mark is
I see no ambiguity there; it's actually clear to me which gets used where.
The use of infimum made perfect sense given that the supremum is what puts
the 'g' in gcd; it's probably best that it be kept in that
unseparately-defined limbo state lest needed support theorems blow up
set.mm's
In my latest PR, I provided a function mapping a set of integers to their
least common multiple (~df-lcmf: ( _lcm `` s ) ) in addition to the
operation calculating the least common multiple of two integers (~df-lcm: (
m lcm n ) ), contributed by SR.
For the typesetting, however, I used the
