SetNotation naming conventions

Stream: std4

[Michael George]

In Classes.SetNotation, there are classes named HasSubset and HasSSubset, and there are also classes named Union and Inter (and others). Is there a reason for the different naming convention (i.e. why not HasUnion or HasInter, or why not Subset and SSubset)?

[François G. Dorais]

It's to avoid name conflicts. For example:

def DecidableSet (α) := α → Bool

namespace DecidableSet

-- This is `Prop` valued so it starts with an upper case letter
def Subset (a b : DecidableSet α) : Prop := ∀ x, a x → b x
instance : HasSubset (DecidableSet α) where
  Subset := Subset

-- This takes values in a type so it starts with a lower case letter
def inter (a b : DecidableSet α) :  DecidableSet α := fun x => a x && b x
instance : Inter (DecidableSet α) where
  inter := inter