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 (~df-lcm: ( > m lcm n ) ), contributed by SR. > > 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. If you look at the theorems in section *6.1.10 The > least common multiple*, then there should be no doubt that this > overloaded representation is not a problem. Only the definitions look a > little bit strange. Actually, the typesettings *are *different: lcm used > as operation has a leading and a trailing blank, lcm used as function has > not (according to our typography conventions). > "Clear by context" makes the implicit assumption that the reader has some higher-level knowledge of material involved. >From the MPE Home Page: "With no prior knowledge of advanced mathematics or even any mathematics at all, you can jump into the middle of any proof, from the most elementary to the most advanced, and understand immediately how the symbols were mechanically manipulated to go from one proof step to another, even if you don't know what the symbols themselves mean." That isn't possible if the reader has to understand context in order to interpret the displayed symbols. 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 complementary goal, which is to provide the reader with an informal higher-level understanding). I find http://us2.metamath.org/mpeuni/lcmfun.html a little jarring even though as a somewhat higher-level user I can distinguish the two lcm's. The "Syntax hints" below the proof become less useful since the two lcm symbols can't be distinguished there. Norm > > If anbody has objections against this overloading, and suggestions how the > current typesettings could be improved, I am open to change it. > > 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 turn supremum into infimum - currently we > don't have infimum defined separately. Since this is noted in set.mm on > several occations. it may be worth to think about providing a separate > definition for infimum... > -- 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/72b282c8-12a0-4b9d-a78d-ece7a817584an%40googlegroups.com.
