Formalising Mathematics with Lean

3.2.Β BasesπŸ”—

Definition 3.7πŸ”—

Let \mathcal{T} be a topology. A base of the topology \mathcal{T} is a collection of open sets \mathcal{B} \subset \mathcal{T} such that every open set of \mathcal{T} is a union of open sets of \mathcal{B}There are several ways of giving this definition; this is the one I have chosen to define it in Lean, independently of Mathlib. Therefore, the results in this section are not literally found in Mathlib..

def isTopoBase {X : Type} [TopologicalSpace X] (B : Set (Set X)) : Prop := (βˆ€ U ∈ B, IsOpen U) ∧ (βˆ€ V : Set X, IsOpen V β†’ βˆƒ UB βŠ† B, V = ⋃₀ UB)

Example 3.11πŸ”—

The set of open intervals in \mathbb{R}, \mathcal{B} = \left\{ I = (a, b) ~|~ a < b\right\}, is a base of the usual topology (\mathbb{R}, \mathcal{T}_u).

Proof. We have seen that open intervals are open in the usual topology (Example 3.6). Therefore, we already have the first part of the definition of a base.

lemma BaseOfRealTopo [T : TopologicalSpace ℝ] (hT : T = UsualTopology) : isTopoBase {s | βˆƒ a b : ℝ, s = Set.Ioo a b} := T:TopologicalSpace ℝhT:T = UsualTopology⊒ isTopoBase {s | βˆƒ a b, s = Set.Ioo a b} T:TopologicalSpace ℝhT:T = UsualTopology⊒ βˆ€ U ∈ {s | βˆƒ a b, s = Set.Ioo a b}, IsOpen UT:TopologicalSpace ℝhT:T = UsualTopology⊒ βˆ€ (V : Set ℝ), IsOpen V β†’ βˆƒ UB βŠ† {s | βˆƒ a b, s = Set.Ioo a b}, V = ⋃₀ UB T:TopologicalSpace ℝhT:T = UsualTopology⊒ βˆ€ U ∈ {s | βˆƒ a b, s = Set.Ioo a b}, IsOpen U intro U T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhU:U ∈ {s | βˆƒ a b, s = Set.Ioo a b}⊒ IsOpen U T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝa:ℝb:ℝhU:U = Set.Ioo a b⊒ IsOpen U T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝa:ℝb:ℝhU:U = Set.Ioo a b⊒ IsOpen (Set.Ioo a b) All goals completed! πŸ™

Now, for the second part, we consider an arbitrary U \subseteq X. We want to see that it can be written as a union of open intervals.

T:TopologicalSpace ℝhT:T = UsualTopology⊒ βˆ€ (V : Set ℝ), IsOpen V β†’ βˆƒ UB βŠ† {s | βˆƒ a b, s = Set.Ioo a b}, V = ⋃₀ UB intro U T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen U⊒ βˆƒ UB βŠ† {s | βˆƒ a b, s = Set.Ioo a b}, U = ⋃₀ UB T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen U⊒ βˆƒ UB βŠ† {s | βˆƒ a b, s = Set.Ioo a b}, U = ⋃₀ UB

To do so, consider, for each x \in U, the \delta_u resulting from applying the definition of open set, that is, such that B_{\delta_x}(x) \subseteq U. We want to prove that U = \bigcup \{B_{\delta_x}(x) | x \in U\}, and that this is a subset of \mathcal{B}.

T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―βŠ’ βˆƒ UB βŠ† {s | βˆƒ a b, s = Set.Ioo a b}, U = ⋃₀ UB T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ U⊒ βˆƒ UB βŠ† {s | βˆƒ a b, s = Set.Ioo a b}, U = ⋃₀ UB T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ U⊒ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)} βŠ† {s | βˆƒ a b, s = Set.Ioo a b} ∧ U = ⋃₀ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)}

Obviously, it is a subset of \mathcal{B} since it is a set formed by open intervals.

T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ U⊒ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)} βŠ† {s | βˆƒ a b, s = Set.Ioo a b}T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ U⊒ U = ⋃₀ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)} T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ U⊒ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)} βŠ† {s | βˆƒ a b, s = Set.Ioo a b} intro V T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ UV:Set ℝhV:V ∈ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)}⊒ V ∈ {s | βˆƒ a b, s = Set.Ioo a b} T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ UV:Set ℝx:↑UhV:V = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)⊒ V ∈ {s | βˆƒ a b, s = Set.Ioo a b} All goals completed! πŸ™

Now, to see that U = \bigcup \{B_{\delta_x}(x) | x \in U\}, we prove the two inclusions separately.

T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ U⊒ U = ⋃₀ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)} T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:β„βŠ’ u ∈ U ↔ u ∈ ⋃₀ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)}; T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:β„βŠ’ u ∈ U β†’ u ∈ ⋃₀ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)}T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:β„βŠ’ u ∈ ⋃₀ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)} β†’ u ∈ U; all_goals T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:ℝhu:u ∈ ⋃₀ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)}⊒ u ∈ U

(\subseteq) Let u \in U. Then u \in B_{\delta_u} trivially. Hence it is in the union.

T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:ℝhu:u ∈ U⊒ u ∈ ⋃₀ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)} T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:ℝhu:u ∈ U⊒ Set.Ioo (u - Ξ΄ ⟨u, hu⟩) (u + Ξ΄ ⟨u, hu⟩) ∈ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)} ∧ u ∈ Set.Ioo (u - Ξ΄ ⟨u, hu⟩) (u + Ξ΄ ⟨u, hu⟩) T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:ℝhu:u ∈ U⊒ Set.Ioo (u - Ξ΄ ⟨u, hu⟩) (u + Ξ΄ ⟨u, hu⟩) ∈ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)}T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:ℝhu:u ∈ U⊒ u ∈ Set.Ioo (u - Ξ΄ ⟨u, hu⟩) (u + Ξ΄ ⟨u, hu⟩) T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:ℝhu:u ∈ U⊒ Set.Ioo (u - Ξ΄ ⟨u, hu⟩) (u + Ξ΄ ⟨u, hu⟩) ∈ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)} T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:ℝhu:u ∈ U⊒ βˆƒ a, βˆƒ (h : a ∈ U), Set.Ioo (u - Ξ΄ ⟨u, hu⟩) (u + Ξ΄ ⟨u, hu⟩) = Set.Ioo (a - Ξ΄ ⟨a, β‹―βŸ©) (a + Ξ΄ ⟨a, β‹―βŸ©) All goals completed! πŸ™ T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:ℝhu:u ∈ U⊒ u ∈ Set.Ioo (u - Ξ΄ ⟨u, hu⟩) (u + Ξ΄ ⟨u, hu⟩) T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:ℝhu:u ∈ U⊒ 0 < Ξ΄ ⟨u, hu⟩ All goals completed! πŸ™

(\supseteq) Let u \in \bigcup \{B_{\delta_x}(x) | x \in U\}. Then there exists a v \in U such that u \in B_{\delta_v}(v) \subseteq U. Hence u \in U.

T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:ℝhu:u ∈ ⋃₀ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)}⊒ u ∈ U T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:ℝI:Set ℝhI:I ∈ {s | βˆƒ x, s = Set.Ioo (↑x - Ξ΄ x) (↑x + Ξ΄ x)}hu:u ∈ I⊒ u ∈ U T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:ℝI:Set ℝhu:u ∈ Iv:↑UhI:I = Set.Ioo (↑v - Ξ΄ v) (↑v + Ξ΄ v)⊒ u ∈ U T:TopologicalSpace ℝhT:T = UsualTopologyU:Set ℝhUopen:IsOpen UΞ΄:↑U β†’ ℝ := fun x => Classical.choose β‹―Ξ΄spec:βˆ€ (x : ↑U), 0 < Ξ΄ x ∧ βˆ€ (y : ℝ), ↑x - Ξ΄ x < y ∧ y < ↑x + Ξ΄ x β†’ y ∈ Uu:ℝI:Set ℝv:↑Uhu:u ∈ Set.Ioo (↑v - Ξ΄ v) (↑v + Ξ΄ v)hI:I = Set.Ioo (↑v - Ξ΄ v) (↑v + Ξ΄ v)⊒ u ∈ U All goals completed! πŸ™

∎