Using sets in lean

Question

I'd like to do some work in topology using lean.

As a good start, I wanted to prove a couple of simple lemmas about sets in lean.

For example

def inter_to_union (H : a ∈ set.inter A B) : a ∈ set.union A B :=
    sorry

or

def set_deMorgan : a ∈ set.inter A B → a ∈ set.compl (set.union (set.compl A) (set.compl B)) :=
sorry

or, perhaps more interestingly

def set_deMorgan2 : set.inter A B = set.compl (set.union (set.compl A) (set.compl B)) :=
sorry

But I can't find anywhere elimination rules for set.union or set.inter, so I just don't know how to work with them.

1. How do I prove the lemmas?

Also, looking at the definition of sets in lean, I can see bits of syntax, which look very much like paper maths, but I don't understand at the level of dependent type theory, for example:

protected def sep (p : α → Prop) (s : set α) : set α :=
{a | a ∈ s ∧ p a}

2. How can one break down the above example into simpler notions of dependent/inductive types?

Answer 1

That module identifies sets with predicates on some type α (α is usually called 'the universe'):

def set (α : Type u) := α → Prop

If you have a set s : set α and for some x : α you can prove s a, this is interpreted as 'x belongs to s'.

In this case, x ∈ A is a notation (let us not mind about typeclasses for now) for set.mem x A which is defined as follows:

protected def mem (a : α) (s : set α) :=
s a

The above explains why the empty set is represented as the predicate always returning false:

instance : has_emptyc (set α) :=
⟨λ a, false⟩

And also, the universe is unsurprisingly represented like so:

def univ : set α :=
λ a, true

I'll show how prove the first lemma:

def inter_to_union {α : Type} {A B : set α} {a : α} : A ∩ B ⊆ A ∪ B :=
  assume (x : α) (xinAB : x ∈ A ∩ B),        -- unfold the definition of `subset`
  have xinA : x ∈ A, from and.left xinAB,
  @or.inl _ (x ∈ B) xinA

This is all like the usual "pointful" proofs for these properties in basic set theory.

Regarding your question about sep -- you can see through notations like so:

set_option pp.notation false
#print set.sep

Here is the output:

protected def set.sep : Π {α : Type u}, (α → Prop) → set α → set α :=
λ {α : Type u} (p : α → Prop) (s : set α),
  set_of (λ (a : α), and (has_mem.mem a s) (p a))