Sets in Lean, example sheet 2 : the empty set and the "universal set". #

We know what the empty subset of X is, and the Lean notation for it is ∅, or, if you want to say which type we're the empty subset of, it's ∅ : set X.

At the other extreme, the subset of X containing all the terms of type X is...well...mathematicians would just call it X, but X is a type, and so if we want a set it's called set.univ : set X, or just univ : set X if we have opened the set namespace. Let's do that now.