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 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... > Yes, perhaps the time has come to provide infimum and retrofit existing uses of `' <. Norm -- 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/812eadda-1462-46e3-ad26-414bc6949287n%40googlegroups.com.
