When I first discovered Lean, I was captivated by the idea of machine-verified mathematics. In my journey into Lean, I learned the basics of tactics and simple proofs. Now, I want to tackle something with real mathematical depth—a theorem from my point-set topology class that I took a year and a half ago.

We used an inquiry-based learning approach in that class, which I loved. We built mathematics together, one definition and proof at a time, eventually assembling our collective work into a short book. One theorem that’s stayed with me is this beautiful result about how continuous functions preserve compactness. Let me share it with you, and in the next post, I’ll show you how to formalize it in Lean.

Setting the Stage: What is Compactness?

Before we dive into the main theorem, we need to understand what compactness means. The definition might seem technical at first, but it captures a surprisingly intuitive geometric idea.

Cover and Subcover: An indexing set gives us a way to label collections. A collection of sets is a cover of a set if . In other words, if you throw all the sets in together, they completely contain . Any subcollection that still manages to cover is called a subcover.

Open Cover: In a topological space , an open cover of is simply a cover where every set is an open set in .

Compactness: Here’s the key definition. A subset is compact if every open cover of has a finite subcover.

Think about what this means: no matter how you try to cover with open sets—even if you use infinitely many of them—you can always find a finite subcollection that still does the job. This is a kind of “finiteness” property that generalizes our intuition about closed and bounded sets in Euclidean space.

A Warmup: Closed Subsets of Compact Sets

Before tackling our main theorem, let’s prove something useful: if is compact and is a closed subset of , then is compact too.

The Proof Idea: We start with an arbitrary open cover of . Our goal is to show it has a finite subcover. Here’s the trick: since is closed, its complement is open. Notice that contains everything in that’s not in , so we can write:

This means is an open cover of . Since is compact, this cover has a finite subcover, say . (Note: might not even be needed if the indexed sets already cover .)

Now comes the punchline: doesn’t intersect at all (since is the complement of ), so when we restrict back to , we get:

Therefore is a finite subcover of our original cover , proving is compact.

The Main Event: Continuous Functions Preserve Compactness

Now we’re ready for the theorem that motivated this post:

Theorem: Let and be topological spaces. If is continuous and is compact, then is compact.

This is remarkable! Continuity is a local property—it’s about what happens in neighborhoods around points. Compactness is a global property—it’s about covers of entire sets. Yet continuous functions bridge these worlds: they take compact sets to compact sets.

The Proof Strategy: We need to show is compact, which means starting with an arbitrary open cover of and finding a finite subcover. Let be an open cover of . By definition:

Taking preimages (and using the fact that ):

Here’s where continuity enters! Since is continuous, each is open in . This means is an open cover of .

By compactness of , there exists a finite subcover with:

Applying to both sides and using the fact that :

Therefore is a finite subcover of , proving is compact!

Why This Matters

This theorem is more than just a technical result. It tells us that compactness is a topological invariant under continuous maps. If you have a compact space and you continuously deform it, the image remains compact. This is why we can prove things like: the continuous image of is always compact, or the extreme value theorem (a continuous real-valued function on a compact set attains its maximum and minimum).

The proof itself is a beautiful dance between covers in the codomain and preimages in the domain, orchestrated by the continuity of .

Coming Up Next

In my next post, I’ll show you how to formalize this exact proof in Lean. We’ll see how the mathematical ideas we’ve explored translate into precise, machine-verified code. It’s a natural next step in my Lean journey—moving from basic proofs to formalizing real mathematics from my coursework.

This theorem appears in the topology book my class wrote together. Special thanks to my professor and classmates for that collaborative mathematical journey.

This post is part of my series on learning Lean. Previous posts: Discovering Lean | A Mathematician’s Journey into Lean