## Stream: lean4

### Topic: sup/Sup

#### 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 Sup and NSup, where N means n-ary?

#### Eric Wieser (Mar 25 2021 at 19:46):

Then we could even distinguish docs#sum from a generalization of docs#finset.sum by calling the latter HasNAdd. Surely no one will be confused by that /s.

#### 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):

I think supS and supR would be better for such an abbreviation, since supr and 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