Kevin Buzzard (Mar 23 2021 at 15:56):
In Lean 3 we have things like conditionally complete lattices which have a
sup (the least upper bound of two things) and a
Sup (the least upper bound of a set of things). I've been idly making some lattice theory because I'm thinking about making Lean 4 teaching material for mathematicians. I wrote this:
class HasSup (P : Type u) where sup : P → P → P
and now I realise that the capitalisation might cause confusion. Does anyone have advice or suggestions on what I should be doing here?
Of course later on we might well have the same question for
group (the structure) and
Group (the category).
Eric Wieser (Mar 25 2021 at 19:39):
For binary/nary, perhaps
NSup, where N means n-ary?
Eric Wieser (Mar 25 2021 at 19:46):
Gabriel Ebner (Mar 25 2021 at 20:02):
n-ary can (and probably should) be defined in terms of binary. (As much as I'd like to suggest
FinSup as the type class for n-ary suprema.) Similarly, indexed suprema can be defined from the set suprema.
Productively speaking, maybe
sups (supremum of set) could be an unambigous analogy to
supr (supremum of range).
Mario Carneiro (Mar 25 2021 at 21:05):
supR would be better for such an abbreviation, since
infi seem to suggest that it's not actually "supremum of range" but rather a slightly different abbreviation of "supremum"
Last updated: May 18 2021 at 22:15 UTC