(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2005-2012 Slawomir Kolodynski This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) header{*\isaheader{Topology\_ZF.thy}*} theory Topology_ZF imports ZF1 Finite_ZF Fol1 begin text{* This theory file provides basic definitions and properties of topology, open and closed sets, closure and boundary.*} section{*Basic definitions and properties*} text{*A typical textbook defines a topology on a set $X$ as a collection $T$ of subsets of $X$ such that $X\in T$, $\emptyset \in T$ and $T$ is closed with respect to arbitrary unions and intersection of two sets. One can notice here that since we always have $\bigcup T = X$, the set on which the topology is defined (the "carrier" of the topology) can always be constructed from the topology itself and is superfluous in the definition. Moreover, as Marnix Klooster pointed out to me, the fact that the empty set is open can also be proven from other axioms. Hence, we define a topology as a collection of sets that is closed under arbitrary unions and intersections of two sets, without any mention of the set on which the topology is defined. Recall that @{text "Pow(T)"} is the powerset of $T$, so that if $M\in$ @{text " Pow(T)"} then $M$ is a subset of $T$. The sets that belong to a topology $T$ will be sometimes called ''open in'' $T$ or just ''open'' if the topology is clear from the context. *} text{*Topology is a collection of sets that is closed under arbitrary unions and intersections of two sets.*} definition IsATopology ("_ {is a topology}" [90] 91) where "T {is a topology} ≡ ( ∀M ∈ Pow(T). ⋃M ∈ T ) ∧ ( ∀U∈T. ∀ V∈T. U∩V ∈ T)" text{*We define interior of a set $A$ as the union of all open sets contained in $A$. We use @{text "Interior(A,T)"} to denote the interior of A.*} definition "Interior(A,T) ≡ ⋃ {U∈T. U ⊆ A}" text{*A set is closed if it is contained in the carrier of topology and its complement is open.*} definition IsClosed (infixl "{is closed in}" 90) where "D {is closed in} T ≡ (D ⊆ ⋃T ∧ ⋃T - D ∈ T)" text{*To prove various properties of closure we will often use the collection of closed sets that contain a given set $A$. Such collection does not have a separate name in informal math. We will call it @{text "ClosedCovers(A,T)"}. *} definition "ClosedCovers(A,T) ≡ {D ∈ Pow(⋃T). D {is closed in} T ∧ A⊆D}" text{*The closure of a set $A$ is defined as the intersection of the collection of closed sets that contain $A$.*} definition "Closure(A,T) ≡ ⋂ ClosedCovers(A,T)" text{*We also define boundary of a set as the intersection of its closure with the closure of the complement (with respect to the carrier).*} definition "Boundary(A,T) ≡ Closure(A,T) ∩ Closure(⋃T - A,T)" text{* A set $K$ is compact if for every collection of open sets that covers $K$ we can choose a finite one that still covers the set. Recall that @{text "FinPow(M)"} is the collection of finite subsets of $M$ (finite powerset of $M$), defined in IsarMathLib's @{text "Finite_ZF"} theory. *} definition IsCompact (infixl "{is compact in}" 90) where "K {is compact in} T ≡ (K ⊆ ⋃T ∧ (∀ M∈Pow(T). K ⊆ ⋃M ⟶ (∃ N ∈ FinPow(M). K ⊆ ⋃N)))" text{*A basic example of a topology: the powerset of any set is a topology.*} lemma Pow_is_top: shows "Pow(X) {is a topology}" proof - have "∀A∈Pow(Pow(X)). ⋃A ∈ Pow(X)" by fast moreover have "∀U∈Pow(X). ∀V∈Pow(X). U∩V ∈ Pow(X)" by fast ultimately show "Pow(X) {is a topology}" using IsATopology_def by auto qed text{*Empty set is open.*} lemma empty_open: assumes "T {is a topology}" shows "0 ∈ T" proof - have "0 ∈ Pow(T)" by simp with assms have "⋃0 ∈ T" using IsATopology_def by blast thus "0 ∈ T" by simp qed text{*Union of a collection of open sets is open.*} lemma union_open: assumes "T {is a topology}" and "∀A∈𝒜. A ∈ T" shows "(⋃𝒜) ∈ T" using assms IsATopology_def by auto text{*Union of a indexed family of open sets is open.*} lemma union_indexed_open: assumes A1: "T {is a topology}" and A2: "∀i∈I. P(i) ∈ T" shows "(⋃i∈I. P(i)) ∈ T" using assms union_open by simp text{*The intersection of any nonempty collection of topologies on a set $X$ is a topology.*} lemma Inter_tops_is_top: assumes A1: "ℳ ≠ 0" and A2: "∀T∈ℳ. T {is a topology}" shows "(⋂ℳ) {is a topology}" proof - { fix A assume "A∈Pow(⋂ℳ)" with A1 have "∀T∈ℳ. A∈Pow(T)" by auto with A1 A2 have "⋃A ∈ ⋂ℳ" using IsATopology_def by auto } then have "∀A. A∈Pow(⋂ℳ) ⟶ ⋃A ∈ ⋂ℳ" by simp hence "∀A∈Pow(⋂ℳ). ⋃A ∈ ⋂ℳ" by auto moreover { fix U V assume "U ∈ ⋂ℳ" and "V ∈ ⋂ℳ" then have "∀T∈ℳ. U ∈ T ∧ V ∈ T" by auto with A1 A2 have "∀T∈ℳ. U∩V ∈ T" using IsATopology_def by simp } then have "∀ U ∈ ⋂ℳ. ∀ V ∈ ⋂ℳ. U∩V ∈ ⋂ℳ" by auto ultimately show "(⋂ℳ) {is a topology}" using IsATopology_def by simp qed text{*We will now introduce some notation. In Isar, this is done by definining a "locale". Locale is kind of a context that holds some assumptions and notation used in all theorems proven in it. In the locale (context) below called @{text "topology0"} we assume that $T$ is a topology. The interior of the set $A$ (with respect to the topology in the context) is denoted @{text "int(A)"}. The closure of a set $A\subseteq \bigcup T$ is denoted @{text "cl(A)"} and the boundary is @{text "∂A"}.*} locale topology0 = fixes T assumes topSpaceAssum: "T {is a topology}" fixes int defines int_def [simp]: "int(A) ≡ Interior(A,T)" fixes cl defines cl_def [simp]: "cl(A) ≡ Closure(A,T)" fixes boundary ("∂_" [91] 92) defines boundary_def [simp]: "∂A ≡ Boundary(A,T)" text{*Intersection of a finite nonempty collection of open sets is open.*} lemma (in topology0) fin_inter_open_open: assumes "N≠0" "N ∈ FinPow(T)" shows "⋂N ∈ T" using topSpaceAssum assms IsATopology_def inter_two_inter_fin by simp text{*Having a topology $T$ and a set $X$ we can define the induced topology as the one consisting of the intersections of $X$ with sets from $T$. The notion of a collection restricted to a set is defined in ZF1.thy.*} lemma (in topology0) Top_1_L4: shows "(T {restricted to} X) {is a topology}" proof - let ?S = "T {restricted to} X" have "∀A∈Pow(?S). ⋃A ∈ ?S" proof fix A assume A1: "A∈Pow(?S)" have "∀V∈A. ⋃ {U ∈ T. V = U∩X} ∈ T" proof - { fix V let ?M = "{U ∈ T. V = U∩X}" have "?M ∈ Pow(T)" by auto with topSpaceAssum have "⋃?M ∈ T" using IsATopology_def by simp } thus ?thesis by simp qed hence "{⋃{U∈T. V = U∩X}.V∈ A} ⊆ T" by auto with topSpaceAssum have "(⋃V∈A. ⋃{U∈T. V = U∩X}) ∈ T" using IsATopology_def by auto then have "(⋃V∈A. ⋃{U∈T. V = U∩X})∩ X ∈ ?S" using RestrictedTo_def by auto moreover from A1 have "∀V∈A. ∃U∈T. V = U∩X" using RestrictedTo_def by auto hence "(⋃V∈A. ⋃{U∈T. V = U∩X})∩X = ⋃A" by blast ultimately show "⋃A ∈ ?S" by simp qed moreover have "∀U∈?S. ∀V∈?S. U∩V ∈ ?S" proof - { fix U V assume "U∈?S" "V∈?S" then obtain U⇩_{1}V⇩_{1}where "U⇩_{1}∈ T ∧ U = U⇩_{1}∩X" and "V⇩_{1}∈ T ∧ V = V⇩_{1}∩X" using RestrictedTo_def by auto with topSpaceAssum have "U⇩_{1}∩V⇩_{1}∈ T" and "U∩V = (U⇩_{1}∩V⇩_{1})∩X" using IsATopology_def by auto then have " U∩V ∈ ?S" using RestrictedTo_def by auto } thus "∀U∈?S. ∀ V∈?S. U∩V ∈ ?S" by simp qed ultimately show "?S {is a topology}" using IsATopology_def by simp qed section{*Interior of a set*} text{*In section we show basic properties of the interior of a set.*} text{*Interior of a set $A$ is contained in $A$.*} lemma (in topology0) Top_2_L1: shows "int(A) ⊆ A" using Interior_def by auto text{*Interior is open.*} lemma (in topology0) Top_2_L2: shows "int(A) ∈ T" proof - have "{U∈T. U⊆A} ∈ Pow(T)" by auto with topSpaceAssum show "int(A) ∈ T" using IsATopology_def Interior_def by auto qed text{*A set is open iff it is equal to its interior.*} lemma (in topology0) Top_2_L3: shows "U∈T ⟷ int(U) = U" proof assume "U∈T" then show "int(U) = U" using Interior_def by auto next assume A1: "int(U) = U" have "int(U) ∈ T" using Top_2_L2 by simp with A1 show "U∈T" by simp qed text{*Interior of the interior is the interior.*} lemma (in topology0) Top_2_L4: shows "int(int(A)) = int(A)" proof - let ?U = "int(A)" from topSpaceAssum have "?U∈T" using Top_2_L2 by simp then show "int(int(A)) = int(A)" using Top_2_L3 by simp qed text{*Interior of a bigger set is bigger.*} lemma (in topology0) interior_mono: assumes A1: "A⊆B" shows "int(A) ⊆ int(B)" proof - from A1 have "∀ U∈T. (U⊆A ⟶ U⊆B)" by auto then show "int(A) ⊆ int(B)" using Interior_def by auto qed text{*An open subset of any set is a subset of the interior of that set.*} lemma (in topology0) Top_2_L5: assumes "U⊆A" and "U∈T" shows "U ⊆ int(A)" using assms Interior_def by auto text{*If a point of a set has an open neighboorhood contained in the set, then the point belongs to the interior of the set.*} lemma (in topology0) Top_2_L6: assumes "∃U∈T. (x∈U ∧ U⊆A)" shows "x ∈ int(A)" using assms Interior_def by auto text{*A set is open iff its every point has a an open neighbourhood contained in the set. We will formulate this statement as two lemmas (implication one way and the other way). The lemma below shows that if a set is open then every point has a an open neighbourhood contained in the set.*} lemma (in topology0) open_open_neigh: assumes A1: "V∈T" shows "∀x∈V. ∃U∈T. (x∈U ∧ U⊆V)" proof - from A1 have "∀x∈V. V∈T ∧ x ∈ V ∧ V ⊆ V" by simp thus ?thesis by auto qed text{*If every point of a set has a an open neighbourhood contained in the set then the set is open.*} lemma (in topology0) open_neigh_open: assumes A1: "∀x∈V. ∃U∈T. (x∈U ∧ U⊆V)" shows "V∈T" proof - from A1 have "V = int(V)" using Top_2_L1 Top_2_L6 by blast then show "V∈T" using Top_2_L3 by simp qed section{*Closed sets, closure, boundary.*} text{*This section is devoted to closed sets and properties of the closure and boundary operators.*} text{* The carrier of the space is closed.*} lemma (in topology0) Top_3_L1: shows "(⋃T) {is closed in} T" proof - have "⋃T - ⋃T = 0" by auto with topSpaceAssum have "⋃T - ⋃T ∈ T" using IsATopology_def by auto then show ?thesis using IsClosed_def by simp qed text{*Empty set is closed.*} lemma (in topology0) Top_3_L2: shows "0 {is closed in} T" using topSpaceAssum IsATopology_def IsClosed_def by simp text{*The collection of closed covers of a subset of the carrier of topology is never empty. This is good to know, as we want to intersect this collection to get the closure.*} lemma (in topology0) Top_3_L3: assumes A1: "A ⊆ ⋃T" shows "ClosedCovers(A,T) ≠ 0" proof - from A1 have "⋃T ∈ ClosedCovers(A,T)" using ClosedCovers_def Top_3_L1 by auto thus ?thesis by auto qed text{*Intersection of a nonempty family of closed sets is closed. *} lemma (in topology0) Top_3_L4: assumes A1: "K≠0" and A2: "∀D∈K. D {is closed in} T" shows "(⋂K) {is closed in} T" proof - from A2 have I: "∀D∈K. (D ⊆ ⋃T ∧ (⋃T - D)∈ T)" using IsClosed_def by simp then have "{⋃T - D. D∈ K} ⊆ T" by auto with topSpaceAssum have "(⋃ {⋃T - D. D∈ K}) ∈ T" using IsATopology_def by auto moreover from A1 have "⋃ {⋃T - D. D∈ K} = ⋃T - ⋂K" by fast moreover from A1 I have "⋂K ⊆ ⋃T" by blast ultimately show "(⋂K) {is closed in} T" using IsClosed_def by simp qed text{*The union and intersection of two closed sets are closed.*} lemma (in topology0) Top_3_L5: assumes A1: "D⇩_{1}{is closed in} T" "D⇩_{2}{is closed in} T" shows "(D⇩_{1}∩D⇩_{2}) {is closed in} T" "(D⇩_{1}∪D⇩_{2}) {is closed in} T" proof - have "{D⇩_{1},D⇩_{2}} ≠ 0" by simp with A1 have "(⋂ {D⇩_{1},D⇩_{2}}) {is closed in} T" using Top_3_L4 by fast thus "(D⇩_{1}∩D⇩_{2}) {is closed in} T" by simp from topSpaceAssum A1 have "(⋃T - D⇩_{1}) ∩ (⋃T - D⇩_{2}) ∈ T" using IsClosed_def IsATopology_def by simp moreover have "(⋃T - D⇩_{1}) ∩ (⋃T - D⇩_{2}) = ⋃T - (D⇩_{1}∪ D⇩_{2})" by auto moreover from A1 have "D⇩_{1}∪ D⇩_{2}⊆ ⋃T" using IsClosed_def by auto ultimately show "(D⇩_{1}∪D⇩_{2}) {is closed in} T" using IsClosed_def by simp qed text{*Finite union of closed sets is closed. To understand the proof recall that $D\in$@{text "Pow(⋃T)"} means that $D$ is a subset of the carrier of the topology.*} lemma (in topology0) fin_union_cl_is_cl: assumes A1: "N ∈ FinPow({D∈Pow(⋃T). D {is closed in} T})" shows "(⋃N) {is closed in} T" proof - let ?C = "{D∈Pow(⋃T). D {is closed in} T}" have "0∈?C" using Top_3_L2 by simp moreover have "∀A∈?C. ∀B∈?C. A∪B ∈ ?C" using Top_3_L5 by auto moreover note A1 ultimately have "⋃N ∈ ?C" by (rule union_two_union_fin) thus "(⋃N) {is closed in} T" by simp qed text{*Closure of a set is closed.*} lemma (in topology0) cl_is_closed: assumes "A ⊆ ⋃T" shows "cl(A) {is closed in} T" using assms Closure_def Top_3_L3 ClosedCovers_def Top_3_L4 by simp text{*Closure of a bigger sets is bigger.*} lemma (in topology0) top_closure_mono: assumes A1: "A ⊆ ⋃T" "B ⊆ ⋃T" and A2:"A⊆B" shows "cl(A) ⊆ cl(B)" proof - from A2 have "ClosedCovers(B,T)⊆ ClosedCovers(A,T)" using ClosedCovers_def by auto with A1 show ?thesis using Top_3_L3 Closure_def by auto qed text{*Boundary of a set is closed.*} lemma (in topology0) boundary_closed: assumes A1: "A ⊆ ⋃T" shows "∂A {is closed in} T" proof - from A1 have "⋃T - A ⊆ ⋃T" by fast with A1 show "∂A {is closed in} T" using cl_is_closed Top_3_L5 Boundary_def by auto qed text{*A set is closed iff it is equal to its closure.*} lemma (in topology0) Top_3_L8: assumes A1: "A ⊆ ⋃T" shows "A {is closed in} T ⟷ cl(A) = A" proof assume "A {is closed in} T" with A1 show "cl(A) = A" using Closure_def ClosedCovers_def by auto next assume "cl(A) = A" then have "⋃T - A = ⋃T - cl(A)" by simp with A1 show "A {is closed in} T" using cl_is_closed IsClosed_def by simp qed text{*Complement of an open set is closed.*} lemma (in topology0) Top_3_L9: assumes A1: "A∈T" shows "(⋃T - A) {is closed in} T" proof - from topSpaceAssum A1 have "⋃T - (⋃T - A) = A" and "⋃T - A ⊆ ⋃T" using IsATopology_def by auto with A1 show "(⋃T - A) {is closed in} T" using IsClosed_def by simp qed text{*A set is contained in its closure.*} lemma (in topology0) cl_contains_set: assumes "A ⊆ ⋃T" shows "A ⊆ cl(A)" using assms Top_3_L1 ClosedCovers_def Top_3_L3 Closure_def by auto text{*Closure of a subset of the carrier is a subset of the carrier and closure of the complement is the complement of the interior.*} lemma (in topology0) Top_3_L11: assumes A1: "A ⊆ ⋃T" shows "cl(A) ⊆ ⋃T" "cl(⋃T - A) = ⋃T - int(A)" proof - from A1 show "cl(A) ⊆ ⋃T" using Top_3_L1 Closure_def ClosedCovers_def by auto from A1 have "⋃T - A ⊆ ⋃T - int(A)" using Top_2_L1 by auto moreover have I: "⋃T - int(A) ⊆ ⋃T" "⋃T - A ⊆ ⋃T" by auto ultimately have "cl(⋃T - A) ⊆ cl(⋃T - int(A))" using top_closure_mono by simp moreover from I have "(⋃T - int(A)) {is closed in} T" using Top_2_L2 Top_3_L9 by simp with I have "cl((⋃T) - int(A)) = ⋃T - int(A)" using Top_3_L8 by simp ultimately have "cl(⋃T - A) ⊆ ⋃T - int(A)" by simp moreover from I have "⋃T - A ⊆ cl(⋃T - A)" using cl_contains_set by simp hence "⋃T - cl(⋃T - A) ⊆ A" and "⋃T - A ⊆ ⋃T" by auto then have "⋃T - cl(⋃T - A) ⊆ int(A)" using cl_is_closed IsClosed_def Top_2_L5 by simp hence "⋃T - int(A) ⊆ cl(⋃T - A)" by auto ultimately show "cl(⋃T - A) = ⋃T - int(A)" by auto qed text{*Boundary of a set is the closure of the set minus the interior of the set.*} lemma (in topology0) Top_3_L12: assumes A1: "A ⊆ ⋃T" shows "∂A = cl(A) - int(A)" proof - from A1 have "∂A = cl(A) ∩ (⋃T - int(A))" using Boundary_def Top_3_L11 by simp moreover from A1 have "cl(A) ∩ (⋃T - int(A)) = cl(A) - int(A)" using Top_3_L11 by blast ultimately show "∂A = cl(A) - int(A)" by simp qed text{*If a set $A$ is contained in a closed set $B$, then the closure of $A$ is contained in $B$.*} lemma (in topology0) Top_3_L13: assumes A1: "B {is closed in} T" "A⊆B" shows "cl(A) ⊆ B" proof - from A1 have "B ⊆ ⋃T" using IsClosed_def by simp with A1 show "cl(A) ⊆ B" using ClosedCovers_def Closure_def by auto qed (*text{*If two open sets are disjoint, then we can close one of them and they will still be disjoint.*} lemma (in topology0) open_disj_cl_disj: assumes A1: "U∈T" "V∈T" and A2: "U∩V = 0" shows "cl(U) ∩ V = 0" proof - from topSpaceAssum A1 have I: "U ⊆ ⋃T" using IsATopology_def by auto with A2 have "U ⊆ ⋃T - V" by auto moreover from A1 have "(⋃T - V) {is closed in} T" using Top_3_L9 by simp ultimately have "cl(U) - (⋃T - V) = 0" using Top_3_L13 by blast moreover from I have "cl(U) ⊆ ⋃T" using cl_is_closed IsClosed_def by simp then have "cl(U) -(⋃T - V) = cl(U) ∩ V" by auto ultimately show "cl(U) ∩ V = 0" by simp qed;*) text{*If a set is disjoint with an open set, then we can close it and it will still be disjoint.*} lemma (in topology0) disj_open_cl_disj: assumes A1: "A ⊆ ⋃T" "V∈T" and A2: "A∩V = 0" shows "cl(A) ∩ V = 0" proof - from assms have "A ⊆ ⋃T - V" by auto moreover from A1 have "(⋃T - V) {is closed in} T" using Top_3_L9 by simp ultimately have "cl(A) - (⋃T - V) = 0" using Top_3_L13 by blast moreover from A1 have "cl(A) ⊆ ⋃T" using cl_is_closed IsClosed_def by simp then have "cl(A) -(⋃T - V) = cl(A) ∩ V" by auto ultimately show ?thesis by simp qed text{*A reformulation of @{text "disj_open_cl_disj"}: If a point belongs to the closure of a set, then we can find a point from the set in any open neighboorhood of the point.*} lemma (in topology0) cl_inter_neigh: assumes "A ⊆ ⋃T" and "U∈T" and "x ∈ cl(A) ∩ U" shows "A∩U ≠ 0" using assms disj_open_cl_disj by auto text{*A reverse of @{text "cl_inter_neigh"}: if every open neiboorhood of a point has a nonempty intersection with a set, then that point belongs to the closure of the set.*} lemma (in topology0) inter_neigh_cl: assumes A1: "A ⊆ ⋃T" and A2: "x∈⋃T" and A3: "∀U∈T. x∈U ⟶ U∩A ≠ 0" shows "x ∈ cl(A)" proof - { assume "x ∉ cl(A)" with A1 obtain D where "D {is closed in} T" and "A⊆D" and "x∉D" using Top_3_L3 Closure_def ClosedCovers_def by auto let ?U = "(⋃T) - D" from A2 `D {is closed in} T` `x∉D` `A⊆D` have "?U∈T" "x∈?U" and "?U∩A = 0" unfolding IsClosed_def by auto with A3 have False by auto } thus ?thesis by auto qed end