Given a universal set $\mathcal U$, one can go back and forth between predicates on elements of $\mathcal U$ and subsets of $\mathcal U$.

For $P(x)$, a predicate on $x \in \mathcal U$, we define the set \(X := \lbrace x \mid P(x) \rbrace\) This is the set of all $x \in \mathcal U$ satisfying $P$.

For a subset $X \subset \mathcal U$, we have \(P(x) := x \in X\) the predicate which checks membership of $x$ in $X$.

We use this idea to embed basic set theory in Lean as follows. For our universe of discourse $\mathcal U$, we use a type U:Type and then we define Set U to simply be predicates

Here we create a definition, denoted def, to indicate we are constructing some data. Theorems/examples are just special types of definitions in Lean.

Membership now becomes satisifcation of the underlying predicate.

We introduce standard mathematical notation for membership ∈ typed as \in. To check membership is then equivelent to providing a proof of the predicate.

We have containment of sets.

Then, our basic set operations mirror our logical operations.

We also have the universal set and the empty set

With this, we can define the complement of a set: all elements not in it.

Then the remainder of set-theoretic constructs

Taking both power sets and products naturally land us in sets of a different type than we start.

Notice for products we have a product type U × V. Terms of this type are pairs (u,v) where u:U and v:V. Writing z : U × V we can access the each entry using z.1 and z.2.

Before we prove anything, we need one essential fact: set extensionality. This is an axiom of set theory but is a consequence (of other extensionality axioms) in Lean.

Let’s see some proves using these notions.

We introduced some new syntax here. Note the dots. They focus your infoview on a single current goal if you have multiple. They are not necessary but might be helpful. Note that you need to indent if you use dots.