Definition 3.8 (Subspace topology)🔗

Let (X, \mathcal{T}) be a topological space and A \subseteq X a subset. Then the collection \mathcal{T}|_A = \{U \cap A | U \in \mathcal{T}\} is a topology on A, called the topology relative to X on A, or the subspace topology.

We will say that (A, \mathcal{T}|_A) is a topological subspace of (X, \mathcal{T}).

In Lean, in order to use this definition, we have to prove that this collection is, indeed, a topology.

Proof. Let (X, \mathcal{T}) be a topological space and A \subseteq X a subset, and define the collection \mathcal{T}|_A = \{U \cap A | U \in \mathcal{T}\}

(1) The universe is open. Indeed, since A = X \cap A and X is open in X.

(2) Let V_1 and V_2 be open in A. Then V_1 = U_1 \cap A and V_2 = U_2 \cap A with U_1, U_2 open in X. Hence V_1 \cap V_2 = (U_1 \cap A) \cap (U_2 \cap A) = (U_1 \cap U_2) \cap A, and U_1 \cap U_2 is open in X by the second property.

(3) Let S = \{V_i\}_i be a collection of open sets in A. Then, for each V_i there exists a U_i open in X such that V_i = U_i \cap A. Then \bigcup S = \bigcup_{i}V_i = \bigcup_{i}(U_i \cap A) = A \cap \bigcup_{i}U_i, and \bigcup_{i}U_i is open in X by the third property. The Lean proof is not included here due to its greater complexity. ∎

Example 3.12🔗

Consider \mathbb{R} with the usual topology and the interval [0, 1] \subset \mathbb{R}. In the topology of [0, 1] induced by the usual topology, the intervals of the form [0, b) are open for every 0 < b \leq 1 (even though they are not open in \mathbb{R}). The intervals of the form (a, 1] are also open for each 0 \leq a < 1.

Proof. For each b > 0, it suffices to use, for example, the open interval (-1, b). We have already seen that open intervals are open in \mathbb{R}, and we have (-1, b) \cap [0, 1] = [0, b). Hence [0, b) is open in [0, 1].

∎