Definition 3.1 (Topological space)🔗

Let X be a set and \mathcal{T} a collection of subsets of X such that

1. The sets \emptyset and X belong to \mathcal{T}.

2. Any finite intersection of elements of \mathcal{T} belongs to \mathcal{T}.

3. Any arbitrary union of elements of \mathcal{T} belongs to \mathcal{T}.

Then we will say that \mathcal{T} is a topology on X, that (X, \mathcal{T}) is a topological space and that the elements of \mathcal{T} are open in this space.

In Lean, this definition is written as a structure consisting of four elements:

The first element, IsOpen, is a function taking each set of X to a proposition, that is, it is a description of the elements of \mathcal{T} as the set {U ∈ Set (X) | IsOpen U}. The other three elements are proofs of the properties in the definition.

Let us look at some examples and their proofs in Lean.

Example 3.1🔗

Let X be any set. Consider the collection of all subsets of X, \mathcal{T} = \mathcal{P}(X). Then \mathcal{T} is a topology on X, which we call the discrete topology.

Proof. We can describe \mathcal T as {U ∈ Set (X) | true}, because IsOpen is true for any U.

Now, proving the remaining properties is easy:

Applying the function fun x ↦ true to any set always returns true, so it suffices to use trivial.

∎

Example 3.2🔗

Let X be any set. Consider the collection \mathcal{T}=\{\emptyset, X\}. Then \mathcal{T} is a topology on X, which we call the trivial topology.

Proof. We can describe \mathcal{T} as {U ∈ Set (X) | U = X ∨ U = ∅}.

The first condition holds trivially: we want to see X = X \lor X = \emptyset.

Let us now consider two open sets (intro). We distinguish cases:

If both are X, the intersection will be X and therefore open. If one of the two is empty, then the intersection is empty, also open.

Finally, consider an arbitrary collection S of open sets. To see whether the union is open, we consider two different cases: either X is in S, in which case the union is X, or it is not, in which case all the sets in S are the empty set and so is the union.

∎

Example 3.3🔗

Consider the real line and the usual definition of an open set in \mathbb{R}, that is, A \subseteq \mathbb{R} is open if and only if for each point x \in A there exists an open ball centred at x entirely contained in A. Let \mathcal{T} be the collection of these open sets. Then \mathcal{T} is a topology on \mathbb{R}, which we call the usual topology.

Proof. In Lean, we can describe this topological space by giving its elements in the following way, where each object is defined beforehand.

The definition of an open set can be written like this:

We give the proof for the finite intersection. The others use similar mechanisms.

Let, therefore, s and t be two subsets of \mathcal{T}. Let x \in t \cap s; we want to see that there exists an open ball centred at x and contained in t \cap s.

Since x \in s, there exists a \delta_1>0 (hδ1) such that B_{\delta_1}(x) \subseteq s (hs). Analogously, there exists a \delta_2>0 (hδ2) such that B_{\delta_2}(x) \subseteq t (ht). It suffices to take \delta = \min \{\delta_1, \delta_2\}.

Trivially \delta > 0.

To see that B_\delta (x) \subseteq s \cap t, we consider y \in B_\delta(x) and want to see that y \in s and that y \in t. To see y \in s, since B_{\delta_1}(x) \subseteq s (hs), it suffices to see y \in B_{\delta_1}(x).