Theory Topology_ZF

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written for Isabelle/Isar.

    Copyright (C) 2005, 2006  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 Finite1 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. Hence, we decided to define a topology as 
  a collection of sets that contains the empty set and 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$. 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. 
  Closed set is one such that it is contained
  in the carrier of the topology (i.e. $\bigcup T$) and its complement is 
  open (i.e. belongs to the topology). 
  The closure of a set is the intersection of all closed sets that contain it.
  To prove varius properties of closure we will often use the collection of 
  closed sets that contain a given set $A$. Such collection does not have a 
  name in romantic math. We will call it @{text "ClosedCovers(A,T)"}.
  The closure of a set $A$ is defined as the intersection of the collection 
  of the closed sets $D$ such that $A\subseteq D$.
  We also define boundary  of a set as the intersection of its closure with 
  the closure of the complement (with respect to the carrier).
  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 Fin($M$) is the collection of finite subsets of M 
  (finite powerset of $M$), defined in the @{text "Finite"} theory of 
  Isabelle/ZF.*}

constdefs
  IsATopology ("_ {is a topology}" [90] 91)
  "T {is a topology} ≡ ( 0 ∈ T) ∧ ( ∀M∈Pow(T). \<Union>M ∈ T ) ∧ 
  ( ∀U∈T. ∀ V∈T. U∩V ∈ T)"

  "Interior(A,T) ≡ \<Union> {U∈T. U⊆A}"

  IsClosed (infixl "{is closed in}" 90)
  "D {is closed in} T ≡ (D ⊆ \<Union>T ∧ \<Union>T - D ∈ T)"

  "ClosedCovers(A,T) ≡ {D ∈ Pow(\<Union>T). D {is closed in} T ∧ A⊆D}"

  "Closure(A,T) ≡ \<Inter> ClosedCovers(A,T)"

  "Boundary(A,T) ≡ Closure(A,T) ∩ Closure(\<Union>T - A,T)"


  IsCompact (infixl "{is compact in}" 90)
  "K {is compact in} T ≡ (K ⊆ \<Union>T ∧ 
  (∀ M∈Pow(T). K ⊆ \<Union>M --> (∃ N∈Fin(M). K ⊆ \<Union>N)))";



text{*A basic example of a topology: the powerset of any set is a topology.*}

lemma Top_1_L1: shows "Pow(X) {is a topology}"
proof -
  have "0 ∈ Pow(X)" by simp
  moreover have "∀A∈Pow(Pow(X)). \<Union>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{*The intersection of any nonempty 
  collection of topologies on a set $X$ is a topology.*}

lemma Top_1_L2: assumes A1: "\<M> ≠ 0" and A2: "∀T∈\<M>. T {is a topology}"
  shows "(\<Inter>\<M>) {is a topology}"
proof -;
  from A1 A2 have "0 ∈ \<Inter>\<M>" using IsATopology_def
    by auto;
  moreover 
  { fix A assume "A∈Pow(\<Inter>\<M>)"
    with A1 have "∀T∈\<M>. A∈Pow(T)" by auto;
    with A1 A2 have "\<Union>A ∈ \<Inter>\<M>" using IsATopology_def
      by auto;
  } then have "∀A. A∈Pow(\<Inter>\<M>) --> \<Union>A ∈ \<Inter>\<M>" by simp;
  hence "∀A∈Pow(\<Inter>\<M>). \<Union>A ∈ \<Inter>\<M>" by auto;
  moreover
  { fix U V assume "U ∈ \<Inter>\<M>" and "V ∈ \<Inter>\<M>"
    then have "∀T∈\<M>. U ∈ T ∧ V ∈ T" by auto;
    with A1 A2 have "∀T∈\<M>. U∩V ∈ T" using IsATopology_def
      by simp;
  } then have "∀ U ∈ \<Inter>\<M>. ∀ V ∈ \<Inter>\<M>. U∩V ∈ \<Inter>\<M>"
    by auto;
  ultimately show "(\<Inter>\<M>) {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 topolgy.
  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) Top_1_L3: assumes "N≠0" "N ∈ Fin(T)"
  shows "\<Inter>N ∈ T"
  using topSpaceAssum prems IsATopology_def Finite1_L5 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 Finite1.thy.*}

lemma (in topology0) Top_1_L4: 
  shows "(T {restricted to} X) {is a topology}"
proof -
  let ?S = "T {restricted to} X"
  from topSpaceAssum have "0 ∈ ?S"
    using IsATopology_def RestrictedTo_def by auto;
  moreover have "∀A∈Pow(?S). \<Union>A ∈ ?S"
  proof
    fix A assume A1: "A∈Pow(?S)"
    from topSpaceAssum have "∀V∈A. \<Union> {U ∈ T. V = U∩X} ∈ T"
      using IsATopology_def by auto;
    hence "{\<Union>{U∈T. V = U∩X}.V∈ A} ⊆ T" by auto;
    with topSpaceAssum have "(\<Union>V∈A. \<Union>{U∈T. V = U∩X}) ∈ T"
      using IsATopology_def by auto;
    then have "(\<Union>V∈A. \<Union>{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 "(\<Union>V∈A. \<Union>{U∈T. V = U∩X})∩X = \<Union>A" by fast;
    ultimately show "\<Union>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 U1 V1 where 
        "U1 ∈ T ∧ U = U1∩X" and "V1 ∈ T ∧ V = V1∩X"
        using RestrictedTo_def by auto;
      with topSpaceAssum have "U1∩V1 ∈ T" and "U∩V = (U1∩V1)∩X"
        using IsATopology_def by auto;
      then have " U∩V ∈ ?S" using RestrictedTo_def by auto
    } then show "∀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"
  using topSpaceAssum IsATopology_def Interior_def
  by auto;

text{*A set is open iff it is equal to its interior.*}

lemma (in topology0) Top_2_L3:  "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 prems 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 prems 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) Top_2_L7: 
  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
  then show ?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) Top_2_L8: 
  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 "(\<Union>T) {is closed in} T"
proof -
  have "\<Union>T - \<Union>T = 0" by auto;
  with topSpaceAssum have "\<Union>T - \<Union>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 ⊆ \<Union>T" shows "ClosedCovers(A,T) ≠ 0"
proof -
  from A1 have "\<Union>T ∈ ClosedCovers(A,T)" using ClosedCovers_def Top_3_L1
    by auto;
  then show ?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 "(\<Inter>K) {is closed in} T"
proof -
  from A2 have I: "∀D∈K. (D ⊆ \<Union>T ∧ (\<Union>T - D)∈ T)"
    using IsClosed_def by simp;
  then have "{\<Union>T - D. D∈ K} ⊆ T" by auto;
  with topSpaceAssum have "(\<Union> {\<Union>T - D. D∈ K}) ∈ T" 
    using IsATopology_def by auto;
  moreover from A1 have "\<Union> {\<Union>T - D. D∈ K} = \<Union>T - \<Inter>K" by fast;
  moreover from A1 I have "\<Inter>K ⊆ \<Union>T" by blast;
  ultimately show "(\<Inter>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: "D1 {is closed in} T"   "D2 {is closed in} T"
  shows 
  "(D1∩D2) {is closed in} T"
  "(D1∪D2) {is closed in} T"
proof -
  have "{D1,D2} ≠ 0" by simp
  with A1 have "(\<Inter> {D1,D2}) {is closed in} T" using Top_3_L4
    by fast;
  thus "(D1∩D2) {is closed in} T" by simp;
  from topSpaceAssum A1 have "(\<Union>T - D1) ∩ (\<Union>T - D2) ∈ T"
    using IsClosed_def IsATopology_def by simp;
  moreover have "(\<Union>T - D1) ∩ (\<Union>T - D2) = \<Union>T - (D1 ∪ D2)" 
    by auto;
  moreover from A1 have "D1 ∪ D2 ⊆ \<Union>T" using IsClosed_def
    by auto;
  ultimately show "(D1∪D2) {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(\<Union>T)"} means
  that $D$ is as subset of the carrier of the topology.*} 

lemma (in topology0) Top_3_L6: 
  assumes A1: "N ∈ Fin({D∈Pow(\<Union>T). D {is closed in} T})"
  shows "(\<Union>N) {is closed in} T"
proof -
  let ?C = "{D∈Pow(\<Union>T). D {is closed in} T}"
  have "0∈?C" using Top_3_L2 by simp;
  moreover have "∀A B. ((A∈?C ∧  B∈?C) --> A∪B ∈ ?C)"
    using Top_3_L5 by auto;
  ultimately have "\<Union>N ∈ ?C" by (rule Finite1_L3);
  thus "(\<Union>N) {is closed in} T" by simp;
qed;

text{*Closure of a set is closed.*}

lemma (in topology0) Top_3_L7: assumes "A ⊆ \<Union>T"
  shows "cl(A) {is closed in} T"
  using prems 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 ⊆ \<Union>T"  "B ⊆ \<Union>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 ⊆ \<Union>T" shows "∂A {is closed in} T"
proof -;
  from A1 have "\<Union>T - A ⊆ \<Union>T" by fast;
  with A1 show "∂A {is closed in} T"
    using Top_3_L7 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 ⊆ \<Union>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 "\<Union>T - A = \<Union>T - cl(A)" by simp;
  with A1 show "A {is closed in} T" using Top_3_L7 IsClosed_def
    by simp;
qed;

text{*Complement of an open set is closed.*}

lemma (in topology0) Top_3_L9: 
  assumes A1: "A∈T" 
  shows "(\<Union>T - A) {is closed in} T"
proof -
  from topSpaceAssum A1 have "\<Union>T - (\<Union>T - A) = A" and "\<Union>T - A ⊆ \<Union>T"
    using IsATopology_def by auto;
  with A1 show "(\<Union>T - A) {is closed in} T" using IsClosed_def by simp
qed;

text{*A set is contained in its closure.*}

lemma (in topology0) Top_3_L10: assumes "A ⊆ \<Union>T" shows "A ⊆ cl(A)"
  using prems 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 ⊆ \<Union>T" 
  shows 
  "cl(A) ⊆ \<Union>T"
  "cl(\<Union>T - A) = \<Union>T - int(A)"
proof -
  from A1 show "cl(A) ⊆ \<Union>T" using Top_3_L1 Closure_def ClosedCovers_def
    by auto;
  from A1 have "\<Union>T - A ⊆ \<Union>T - int(A)" using Top_2_L1
    by auto;
  moreover have I: "\<Union>T - int(A) ⊆ \<Union>T"   "\<Union>T - A ⊆ \<Union>T" by auto;
  ultimately have "cl(\<Union>T - A) ⊆ cl(\<Union>T - int(A))"
    using top_closure_mono by simp;
  moreover
  from I have "(\<Union>T - int(A)) {is closed in} T"
    using Top_2_L2 Top_3_L9 by simp;
  with I have "cl((\<Union>T) - int(A)) = \<Union>T - int(A)"
    using Top_3_L8 by simp;
  ultimately have "cl(\<Union>T - A) ⊆ \<Union>T - int(A)" by simp;
  moreover
  from I have "\<Union>T - A ⊆ cl(\<Union>T - A)" using Top_3_L10 by simp;
  hence "\<Union>T - cl(\<Union>T - A) ⊆ A" and "\<Union>T - A ⊆ \<Union>T"  by auto;
  then have "\<Union>T - cl(\<Union>T - A) ⊆ int(A)"
    using Top_3_L7 IsClosed_def Top_2_L5 by simp;
  hence "\<Union>T - int(A) ⊆  cl(\<Union>T - A)" by auto;
  ultimately show "cl(\<Union>T - A) = \<Union>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 ⊆ \<Union>T"
  shows "∂A = cl(A) - int(A)"
proof -
  from A1 have "∂A = cl(A) ∩ (\<Union>T - int(A))" 
    using Boundary_def Top_3_L11 by simp;
  moreover from A1 have 
    "cl(A) ∩ (\<Union>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 ⊆ \<Union>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) Top_3_L14:
  assumes A1: "U∈T"  "V∈T" and  A2: "U∩V = 0"
  shows "cl(U) ∩ V = 0"
proof -
  from topSpaceAssum A1 have I: "U ⊆ \<Union>T" using IsATopology_def
    by auto;
  with A2 have  "U ⊆ \<Union>T - V" by auto;
  moreover from A1 have "(\<Union>T - V) {is closed in} T" using Top_3_L9 
    by simp;
  ultimately have "cl(U) - (\<Union>T - V) = 0" 
    using Top_3_L13 by blast;
  moreover 
  from I have "cl(U) ⊆ \<Union>T" using Top_3_L7 IsClosed_def by simp;
  then have "cl(U) -(\<Union>T - V) = cl(U) ∩ V" by auto;
  ultimately show "cl(U) ∩ V = 0" by simp;
qed;

end