Sets in Lean

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

def Set (U : Type) := U → Prop

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.

variable (U : Type) 

def Mem (x : U) (X : Set U) : Prop := X x

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

variable (U : Type)
variable (X : Set U)

-- going from a proof of X x to x ∈ X 
example (x : U) (h : X x) : x ∈ X := h  

-- going back 
example (x : U) (h : x ∈ X) : X x := h

We have containment of sets.

variable (U : Type)

def Subset {U : Type} (X Y : Set U) : Prop := ∀ x, x ∈ X → x ∈ Y
-- given the notation ⊆, typed \sub

Then, our basic set operations mirror our logical operations.

variable (U : Type)

def Union (X Y : Set U) : Set U := fun (x:U) => x ∈ X ∨ x ∈ Y
-- given the notation X ∪ Y, typed as \cup 
def Inter (X Y : Set U) : Set U := fun (x:U) => x ∈ X ∧ x ∈ Y  
-- given the notation X ∩ Y, typed as \cap 
def Diff (X Y : Set U) : Set U := fun (x:U) => x ∈ X ∧ x ∉ Y 
-- given the notation X \ Y

We also have the universal set and the empty set

variable (U : Type)

def Univ : Set U := fun _ => True 
def Empty : Set U := fun _ => False 
--  with notation ∅, typed as \empty

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

variable (U : Type)

def Comp (X: Set U) : Set U := Univ \ X 
-- given the notation Xᶜ, typed \^c

Then the remainder of set-theoretic constructs

variable (I U V: Type) 

def PowerSet (X : Set U) : Set (Set U) := fun (Y : Set U) => Y ⊆ X
-- given notation 𝒫, typed \powerset 

def Prod (X : Set U) (Y : Set V) : Set (U × V) := fun z => z.1 ∈ X ∧ z.2 ∈ Y
-- given notation X ×ˢ Y, typed \times\^s 

def BigUnion (X : I → Set U) : Set U := fun x => ∃ i, x ∈ X i 

def BigInter (X : I → Set U) : Set U := fun x => ∀ i, x ∈ X i

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.

variable (U : Type)
variable (X Y : Type) 

theorem set_ext : X = Y ↔ (∀ (x:U), x ∈ X ↔ x ∈ Y) := sorry

Let’s see some proves using these notions.

varible (U : Type)
variable (X Y : Set U)

theorem sub_left_of_union : X ⊆ X ∪ Y := by 
  intro (x:U) (h: x ∈ X)
  -- we call the corresponding operation on propositions 
  exact Or.inl h 

theorem sub_right_of_union : Y ⊆ X ∪ Y := by 
  intro (x:U) (h: x ∈ Y)
  exact Or.inr h 

theorem comm_union : X ∪ Y = Y ∪ X := by 
  -- we use set extensionality to get equality from a proof 
  -- of (∀ (x:U), x ∈ X ↔ x ∈ Y) 
  apply set_ext.mpr
  intro (x:U) 
  apply Iff.intro
  -- this allows us to split into two proofs for each direction 
  -- of containment. 
  · intro (h: x ∈ X ∪ Y ) 
    apply Or.elim h 
    -- now we supply proofs for each branch of the or 
    · exact fun (g : x ∈ X) => sub_right_of_union x g 
    · exact fun (g : x ∈ Y) => exact sub_left_of_union x g 
  · intro (h : x ∈ Y ∪ X) 
    apply Or.elim h 
    · exact fun (g : x ∈ Y) => sub_right_of_union x g 
    · exact fun (g : x ∈ X) => exact sub_left_of_union x g

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.