11. Topology

Calculus is based on the concept of a function, which is used to model quantities that depend on one another. For example, it is common to study quantities that change over time. The notion of a limit is also fundamental. We may say that the limit of a function \(f(x)\) is a value \(b\) as \(x\) approaches a value \(a\), or that \(f(x)\) converges to \(b\) as \(x\) approaches \(a\). Equivalently, we may say that \(f(x)\) approaches \(b\) as \(x\) approaches a value \(a\), or that it tends to \(b\) as \(x\) tends to \(a\). We have already begun to consider such notions in Section 3.6.

Topology is the abstract study of limits and continuity. Having covered the essentials of formalization in Chapters 2 to 7, in this chapter, we will explain how topological notions are formalized in Mathlib. Not only do topological abstractions apply in much greater generality, but they also, somewhat paradoxically, make it easier to reason about limits and continuity in concrete instances.

Topological notions build on quite a few layers of mathematical structure. The first layer is naive set theory, as described in Chapter 4. The next layer is the theory of filters, which we will describe in Section 11.1. On top of that, we layer the theories of topological spaces, metric spaces, and a slightly more exotic intermediate notion called a uniform space.

Whereas previous chapters relied on mathematical notions that were likely familiar to you, the notion of a filter is less well known, even to many working mathematicians. The notion is essential, however, for formalizing mathematics effectively. Let us explain why. Let f : ℝ → ℝ be any function. We can consider the limit of f x as x approaches some value x₀, but we can also consider the limit of f x as x approaches infinity or negative infinity. We can moreover consider the limit of f x as x approaches x₀ from the right, conventionally written x₀⁺, or from the left, written x₀⁻. There are variations where x approaches x₀ or x₀⁺ or x₀⁻ but is not allowed to take on the value x₀ itself. This results in at least eight ways that x can approach something. We can also restrict to rational values of x or place other constraints on the domain, but let’s stick to those 8 cases.

We have a similar variety of options on the codomain: we can specify that f x approaches a value from the left or right, or that it approaches positive or negative infinity, and so on. For example, we may wish to say that f x tends to +∞ when x tends to x₀ from the right without being equal to x₀. This results in 64 different kinds of limit statements, and we haven’t even begun to deal with limits of sequences, as we did in Section 3.6.

The problem is compounded even further when it comes to the supporting lemmas. For instance, limits compose: if f x tends to y₀ when x tends to x₀ and g y tends to z₀ when y tends to y₀ then g ∘ f x tends to z₀ when x tends to x₀. There are three notions of “tends to” at play here, each of which can be instantiated in any of the eight ways described in the previous paragraph. This results in 512 lemmas, a lot to have to add to a library! Informally, mathematicians generally prove two or three of these and simply note that the rest can be proved “in the same way.” Formalizing mathematics requires making the relevant notion of “sameness” fully explicit, and that is exactly what Bourbaki’s theory of filters manages to do.

11.1. Filters

A filter on a type X is a collection of sets of X that satisfies certain criterion.

Filter.atTop: a filter representing the limit → ∞ on an ordered set
- (atTop : Filter ℕ), made of sets of ℕ containing {n | n ≥ N} for some N
𝓝 x, made of neighborhoods of x in a topological space
Tendsto u atTop (𝓝 a): function u tends to a as its argument goes to + ∞
- Tendsto f l l': as inputs follow the filter l, the outputs follow the filter l'

11.2. Metric spaces

A metric space is a type X equipped with a distance function dist : X → X → ℝ.

variable {X : Type*} [MetricSpace X] (a b c : X)

#check (dist a b : ℝ)
#check (dist_nonneg : 0 ≤ dist a b)
#check (dist_eq_zero : dist a b = 0 ↔ a = b)
#check (dist_comm a b : dist a b = dist b a)
#check (dist_triangle a b c : dist a c ≤ dist a b + dist b c)

11.2.1. Convergence and continuity

example {u : ℕ → X} {a : X} :
    Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε :=
  Metric.tendsto_atTop

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} :
    Continuous f ↔
      ∀ x : X, ∀ ε > 0, ∃ δ > 0, ∀ x', dist x' x < δ → dist (f x') (f x) < ε :=
  Metric.continuous_iff

Lean knows how to treat a product of two metric spaces as a metric space, so it makes sense to consider continuous functions from X × X to ℝ.

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) := by continuity

11.2.2. Balls, open sets and closed sets

Once we have a distance function, the most important geometric definitions are (open) balls and closed balls.

variable (r : ℝ)

example : Metric.ball a r = { b | dist b a < r } :=
  rfl

example : Metric.closedBall a r = { b | dist b a ≤ r } :=
  rfl

Note that r is any real number here, there is no sign restriction. Of course some statements do require a radius condition.

example (hr : 0 < r) : a ∈ Metric.ball a r :=
  Metric.mem_ball_self hr

example (hr : 0 ≤ r) : a ∈ Metric.closedBall a r :=
  Metric.mem_closedBall_self hr

Open sets:

example (s : Set X) : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s :=
  Metric.isOpen_iff

11.2.3. Cauchy Sequence

A Cauchy sequence in a metric space is a sequence whose terms get closer and closer to each other.

example (u : ℕ → X) :
    CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε :=
  Metric.cauchySeq_iff

example (u : ℕ → X) :
    CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) (u N) < ε :=
  Metric.cauchySeq_iff'

example [CompleteSpace X] (u : ℕ → X) (hu : CauchySeq u) :
    ∃ x, Tendsto u atTop (𝓝 x) :=
  cauchySeq_tendsto_of_complete hu