OK, an overview of this week: we’re doing topology. I was going to introduce filters but I decided to put them off for one more week, so this week it’s topology the way it is traditionally taught in mathematics departments. The two main goals are:

- Continuous image of a compact space is compact;
- Closed subspace of a compact space is compact.

As I say, we will be doing the traditional approach, so the thing we will use about a compact space is that every open cover has a finite subcover.

Here then are sketches of the proofs, which should be enough for a mathematician:

**Theorem. **If *S* is a compact space, if *f *is a continuous function defined on *S*, and if *T=f(S)*, then *T* is compact.

*Proof.* Say we have an open cover of *T* by sets ; we seek a finite subcover. Let denote the preimage of under *f*. Then the are open and cover . Choose a finite subcover of ‘s; then the corresponding ‘s cover *f(S)*. QED.

**Theorem. **A closed subspace of a compact space is compact.

*Proof.* Say *S* is compact and *C* is a closed subset. Then *S \ C *is open. Cover *C* by opens ; we seek a finite subcover. Now the and *S \ C* are opens which cover *S*, so we can choose a finite subcover consisting of finitely many of the and *S \ C* which cover *S* and, a forteriori, cover *C*. But *S \ C* doesn’t contribute to this cover, so we have found our finite subcover of *C*. QED.

The main goal this week is to formalise these proofs. The formalisations are mostly straightforward, given what we know, but may well take a beginner some time. I don’t know if it’s helpful or disspiriting to hear that when writing up the solutions I just sat down and worked straight through these in 5-10 minutes.

Next week, we will be doing topology again, but in a completely different way, using filters. One thing about the filter proofs is that they are shorter to formalise than the traditional proofs. But we’ll talk about filters next week, let’s stick to this week for now.

In order to formalise these traditional proofs, it will help us to know some more API (i.e. theorems in the library, for example “a set is closed if and only if its complement is open”), and a couple more tactics. We will also need to know about the ways Lean thinks about arbitrary unions (i.e., unions of possibly infinitely many things). We have (very briefly) seen unions of two things, back in week 1, but here we need to consider arbitrary covers by open sets, so the union of two things isn’t enough. So let’s talk about how Lean does unions. And before we do that, let’s remind ourselves about how sets work.

## Sets in Lean.

Lean’s concept of an abstract “collection of stuff” is a type, rather than a set. When a mathematician writes “a group is a set equipped with a binary operation…”, what they really mean is “a group is a collection of things equipped with a binary operation…”. In type theory, a collection of things is known as a type, not a set, and the things themselves are known as terms of the type, not elements of the set. This is nothing more than a change in nomenclature really. So, if Lean uses type theory and not set theory, then why are we talking about sets at all?

Well, even though Lean doesn’t have the abstract concept of a set as a random collection of stuff, it does have the concept of a *subset of a type*. This means exactly what you think it means: for example, the natural numbers are a type, and the even numbers, prime numbers, counterexamples to the Goldbach conjecture etc are all examples of subsets of this type. If we have a collection of subsets of a type then we can take unions and intersections and so on, to make more subsets of that type. We can make things like the even numbers and the prime numbers into types, and then these would be called subtypes rather than subsets, but we would then lose the ability to take unions and intersections.

In some sense, set theory is more powerful than type theory, because in set theory you can just go crazy and take unions of random things. If is a group, then you can take the union of , the real number , and the Riemann zeta function, because all of these objects are sets. This is something which you cannot do in type theory. Whether you think this makes type theory less powerful than set theory or a lot saner than set theory is a matter for your own conscience, but we will not be discussing these foundational issues here. We will be discussing topological spaces, and if `X`

is a type then a topological space structure on `X`

and the axioms which come with it fortunately only talk about unions and intersections of subsets of * X*, so we will not need to take the union of

*with other random mathematical things.*

`X`

The type of subsets of `X`

is called `set X`

. Why not `subset X`

? I guess what’s going on is that if `S : set X`

(i.e. `S`

is a term of type `set X`

, otherwise known as a subset of `X`

) then `S`

is a set of elements of `X`

. In fact here’s another reason. A topology on `X`

is a set of subsets of `X`

called the *open sets*, satisfying some axioms, and so in Lean the data of a topology is given by a term `C : set (set X)`

. Humans typically say “a set of subsets of `X`

“. If we’d called it `subset X`

then `C : subset (subset X)`

would be a subset of the type of subsets of `X`

, which is more of a mouthful. Anyway, `set X`

it is; let’s continue.

A word of warning: in type theory, terms can have exactly one type. If `x`

is a term and `x : A`

and `x : B`

(i.e. `x`

has type `A`

and type `B`

) then necessarily `A = B`

. So this presents us with a difficulty. If `X : Type`

is a type and `S : set X`

is a subset, and if `x : X`

is a term of type `X`

which is an element of the subset `S`

, then surely we want `x : S`

(representing the fact that `x`

is an element of `S`

), and yet I’ve just explained that this is not allowed unless `S = X`

, which of course will not in general be true. But in fact even more is false — the assertion `x : S`

*does not even make sense*, because `S`

is not a type! It is a term, of type `set X`

. And `S = X`

does not make sense either! The subset of `X`

corresponding to all the terms of `X`

is called `univ : set X`

. So how the heck are we going to express the true-false statement that `x`

is an element of `S`

? Well, `S`

is a set, not a type, so we can just use set notation! `x ∈ S`

is the assertion that the term `x : X`

is an element of the subset `S : set X`

.

## Three types of union.

There are three ways to do unions in Lean! Four if you count binary unions — if `S T : set X`

then the usual `S ∪ T`

notation is the union of `S`

and `T`

. But here we are concerned with arbitrary unions — the union of a collection of subsets of `X`

.

### Union

Let’s start with `set.Union`

. This is a function: let’s take a look at its type. We can do this by typing `#check set.Union`

in Lean and then hovering over `set.Union`

. We see

```
set.Union : (ι → set X) → set X
```

Here `X`

and `ι`

are types. So we see that `set.Union`

takes in a function from `ι`

to the subsets of `X`

(let’s call this function `F`

), and it outputs a subset of `X`

; this subset is of course the union of the `F i`

as `i`

runs through the terms of `ι`

, but we can’t see that from the type alone, we would have to use `#print set.Union`

to see this, or we can just read the docstring, which is also visible when you hover over `set.Union`

. If you `#check @set.Union`

(note the `@`

, which means “display all the inputs which Lean will figure out by itself”) you’ll see something like this:

```
set.Union : Π {X : Type v} {ι : Sort x}, (ι → set X) → set X
```

telling us that the first two inputs are in squiggly brackets so Lean will not be asking the user for them, it will be figuring out them itself by looking at the type (i.e., the domain and range) of the input `F`

. Technical note: that `Sort`

means that `ι`

can, as well as a `Type`

, also be a `Prop`

. More on this later.

Now `set.Union`

is a definition, so it needs an interface, or an API. What do we need to know about this definition in order to use it? Well, in some sense, we only need to know one theorem: we need to know when is an element in the union of a bunch of sets. This is

```
set.mem_Union : x ∈ set.Union F ↔ ∃ (i : ι), x ∈ F i
```

If, like me, you are sick of typing `set`

in front of every function or theorem about sets, we can just `open set`

at the beginning of our file, and then this theorem is magically just called `mem_Union`

, and the union of the sets indexed by the function `F`

is just called `Union F`

. Actually we can do better — there is notation for `Union`

. If `F : (ι → set X)`

then `Union F`

can be written as `⋃ (i : ι), F i`

. You will find that the most common usage of `mem_Union`

is rewriting `x ∈ ⋃ (i : ι), F i`

into `∃ (i : ι), x ∈ F i`

, which you can then make progress with using `cases`

(if it’s a hypothesis) or `use`

(if it’s a goal).

### sUnion

The next kind of union I’ll talk about (although we won’t use it this week so you can skip straight to `bUnion`

if you like) is `set.sUnion`

, or just `sUnion`

if you have the `set`

namespace open. Here our arbitrary collection of subsets of `X`

is just a set of them, rather than a collection indexed by a type `ι`

. We’ve seen this before — in Lean this looks like `C : set (set X)`

— a set of sets of elements of `X`

, or a set of subsets of `X`

if you like. An example would be the open sets in a topology on `X`

, or, as we’ll see next week, the sets which comprise a filter on `X`

. We take the union of these sets using `set.sUnion`

.

```
sUnion : set (set X) → set X
```

Again this a definition (it has an input `{X}`

as well, but Lean will figure it out once it sees `C`

), again it has notation (`⋃₀ C`

is `sUnion C`

) and again a definition needs an API, the key theorem of which is

```
mem_sUnion : x ∈ ⋃₀ C ↔ ∃ (S : set X) (H : S ∈ C), x ∈ S
```

In words — a term `x : X`

is in the union of all the sets of `C`

if and only there exists a subset `S`

of `X`

which is in `C`

and for which `x ∈ S`

.

### bUnion

There is a third kind of union, which is actually quite helpful in practice. This is when we have an index type `ι`

and `F : ι → set X`

, but we only want to take the union of `F i`

for all `i`

in a subset `Z`

of `ι`

. There seems to be no definition of `set.bUnion`

itself, but we have notation `⋃ i ∈ Z, F i`

and of course the key theorem:

```
theorem mem_bUnion_iff {Z : set ι} {F : ι → set X} {x : X} :
x ∈ (⋃ i ∈ Z, F i) ↔ ∃ i ∈ Z, x ∈ F i
```

Note that for some reason it’s called `mem_bUnion_iff`

rather than `mem_bUnion`

, which is odd because Lean is usually extremely anally retentive about consistency like this. It turns out that `mem_bUnion`

is just the right to left implication of this.

We finish with a technical note, which can be omitted on first reading. This `bUnion`

stuff is actually just a union over a union, once you realise that in type theory true-false statements can be thought of as types, and proofs as their terms. This is why `ι`

is allowed to be a `Prop`

as well as a `Type`

. Here are two proofs of the same result (one direction of `mem_bUnion_iff`

). The first uses `mem_bUnion_iff`

and is unsurprising. The second is a more peculiar proof (I give the full Lean code so you can try it at home):

```
import data.set.lattice
variables (X : Type) (ι : Type) {Z : set ι} {F : ι → set X} {x : X}
open set
-- proof using mem_bUnion_iff
example (h : x ∈ (⋃ i ∈ Z, F i)) : ∃ i ∈ Z, x ∈ F i :=
begin
rw mem_bUnion_iff at h,
exact h,
end
-- proof using mem_Union
example (h : x ∈ (⋃ i ∈ Z, F i)) : ∃ i ∈ Z, x ∈ F i :=
begin
-- h : x ∈ ⋃ (i : ι) (H : i ∈ Z), F i
rw mem_Union at h,
-- h : ∃ (i : ι), x ∈ ⋃ (H : i ∈ Z), F i
cases h with i hixF,
-- hixF : x ∈ ⋃ (H : i ∈ Z), F i
rw mem_Union at hixF,
-- ∃ (i_1 : i ∈ Z), x ∈ F i
cases hixF with hiZ hx,
-- hx : x ∈ F i
-- ⊢ ∃ (i : ι) (H : i ∈ Z), x ∈ F i
use [i, hiZ],
exact hx,
end
```

The first proof uses `mem_bUnion_iff`

; the second one emulates it with `mem_Union`

. You can see in the second proof that `⋃ i ∈ Z, F i`

is unfolded to `⋃ (i : ι) (H : i ∈ Z), F i`

so it is really a union over two things. First a union over all `i : ι`

, and second a union over all proofs that `i ∈ Z`

! This is a `Prop`

but we’re taking a `Union`

over it anyway. If `i ∈ Z`

then this union is a union over one element, and if `i ∉ Z`

then it’s a union over no elements, so things work out in the end.

In the “warm-up” part A for this week, we try some basic things with infinite unions.

## Theorems you will need this week

I can’t guess the exact direction you will go, but here are some of the theorems I used in my formalisation of the topology proofs:

`continuous.is_open_preimage`

says that the preimage of an open set is open.`subset_def`

says`S ⊆ T ↔ ∀ x, x ∈ S → x ∈ T`

`compact_iff_finite_subcover'`

says that a space is compact iff every open cover has a finite subcover. Note the`'`

at the end of the statement! Without the`'`

you will get a different notion of finiteness.`is_open_compl_iff`

says that a set has open complement iff it’s closed.`finite.preimage`

says that the preimage of a`finite`

set under an injective map is finite. Note that if you use the unprimed`compact_iff_finite_subcover`

then you will end up with a`finset`

instead, and that’s another story.

I often find these theorems by half-guessing the name and then pressing ctrl-space. Or I use `library_search`

.

## Some tactics

Here are some tactics I’ve not mentioned before, but which I use in the model solutions.

`change`

: If the goal is

, and**⊢**P`Q`

is a proposition which is equal by definition to`P`

, then`change Q`

will change the goal to

. This can be helpful if you want to use**⊢**Q`rw`

on a goal but it’s not quite in the form you want.`rwa h`

just means`rw h, assumption`

— it’s an abbreviation. Recall the`assumption`

tactic tries to close the goal by going through all the hypotheses`X`

in the tactic state and trying`exact X`

. That proof of one direction of`mem_bUnion_iff`

could have been done in one line with`rwa mem_bUnion_iff at h`

.`contradiction`

: if there are two hypotheses in the tactic state,`h1 : P`

and`h2 : ¬ P`

then the`contradiction`

tactic will close the goal immediately (by doing`exfalso, apply h2, exact h1`

).`rcases`

: This is`cases`

on steroids — it will take things apart into more than two pieces. It is very useful for some of this topology stuff. For example if you have a hypothesis`h : ∃ (i : ι) (H : i ∈ F), x ∈ V i`

then`rcases h with ⟨i, hiF, hxV⟩`

immediately extracts`i`

, and names the proofs of`i ∈ F`

and`x ∈ V i`

both at once. With`cases`

you would have to run the tactic twice.

## option

The last new thing I want to talk about in detail this week is the `option X`

type. The tl;dr version (all you need to know) is explained in the worksheet, but here is a more in-depth discussion. Those of you familiar with Haskell or some other functional languages will know this as the `maybe X`

type, and some languages call it `optional X`

. Despite the fancy name, this type is very easy to describe: it is `X`

and some extra element, called `none`

in Lean (and sometimes called other things in other languages). It can be used in Lean to do things like a one point compactification of a topological space.

We don’t need to know the definition, but I’ll show it anyway:

```
inductive option (X : Type)
| some (x : X) : option
| none : option
```

The `option X`

type has two constructors: if `x : X`

then there’s `some x`

, which is a term of type `option X`

corresponding to `x : X`

, and then there’s a second constructor `none`

, which returns a term of type `option X`

which has no corresponding term of type `X`

— it’s the “extra term”. Note that if `x : X`

then it is *not* true that `x : option X`

. Distinct types are disjoint in Lean’s type theory. The term of type `option X`

corresponding to `x`

is `some x`

. The function `some : X → option X`

is invisible if you think of `option X`

as “`X`

plus another element”. If you think of `some`

as a function then it is injective; you’re going to need this. Here’s a theorem which implies it:

```
option.some_inj : some a = some b ↔ a = b
```

Let me end by saying a little bit about what happens when Lean sees that definition of `option X`

above. After processing the definition, Lean puts four new constants into the system. The first is `option`

, a function which eats a type `X`

and spits out a type `option X`

. You might feel that we have just “defined” `option`

above, but that’s not actually how it works: `option`

has no definition, it is a function which cannot be evaluated in any meaningful sense. However it has an API. The second and third new constants in the system are `some`

, a function from `X`

to `option X`

with no definition, and `none`

, a term of type `option X`

with no definition.

The fourth new constant is something called a *recursor*. A recursor is a way of defining functions from an inductive type. For example let’s say we want to build a function `F`

from the naturals to, say, the reals, by induction (or more precisely, by recursion). We want as input data a “start” real number (which will be `F 0`

) and a method which given a natural `n`

and a real number `r`

(which will be `F n`

), returns another real number `r'`

(which will be `F (n + 1)`

. The recursor for the natural numbers is a function which takes these things as input, and then returns the function `F`

.

The recursor for `option`

, called `option.rec`

, takes as input a term `(y0 : Y)`

and a function `f : X → Y`

, and returns the function `F : option X → Y`

which sends `none`

to `y0`

and `some x`

to `f x`

. Again this recursor has no definition, but it does satisfy the theorems `F none = y0`

and `F (some x) = f x`

, and the proofs are both `refl`

— they are true by definition.

From these new constants and these two facts about the recursor, we have enough to be able to prove all the other theorems about `option`

, for example the fact that `some`

is injective. I was surprised about this — the recursor is a very powerful tool. I talk about it more in this blog post, but here I will just finish by explaining the proof of injectivity of `some`

using the recursor. Say `a b : X`

and we know `some a = some b`

. Let’s use the recursor for `option`

to define a function from `option X`

to `X`

. It sends `none`

to `a`

, and let’s use the identity function `f : X → X`

for our function `f`

above. The recursor then spits out a function `F : option X → X`

satisfying `F (some a) = a`

and `F (some b) = b`

. But `some a = some b`

, and hence `a = b`

.

`option`

is a very simple example of a monad. If you really want to go nuts, you can try proving this. But you might have more fun trying the topology theorems.