Zulip Chat Archive

Stream: lean4

Topic: sup/Sup


view this post on Zulip 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).

view this post on Zulip Eric Wieser (Mar 25 2021 at 19:39):

For binary/nary, perhaps Sup and NSup, where N means n-ary?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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