Theory Topology_ZF_1

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics 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\_1.thy}*}

theory Topology_ZF_1 imports Topology_ZF Fol1 

begin

section{*Separation axioms.*}

text{*Topological spaces cas be classified according to certain properties
  called "separation axioms". This section defines what it means that a 
  topological space is $T_0$, $T_1$ or $T_2$.*}

text{*A topology on $X$ is $T_0$ if for every pair of distinct points of $X$
  there is an open set that contains only one of them.
  A topology is $T_1$ if for every such pair there exist an open set that 
  contains the first point but not the second.
  A topology is $T_2$ (Hausdorff) if for every pair of points there exist a 
  pair of disjoint open sets each containing one of the points.*}

constdefs
  
  isT0 ("_ {is T0}" [90] 91)
  "T {is T0} ≡ ∀ x y. ((x ∈ \<Union>T ∧ y ∈ \<Union>T ∧  x≠y) --> 
  (∃U∈T. (x∈U ∧ y∉U) ∨ (y∈U ∧ x∉U)))"

  isT1 ("_ {is T1}" [90] 91)
  "T {is T1} ≡ ∀ x y. ((x ∈ \<Union>T ∧ y ∈ \<Union>T ∧  x≠y) --> 
  (∃U∈T. (x∈U ∧ y∉U)))"

  isT2 ("_ {is T2}" [90] 91)
  "T {is T2} ≡ ∀ x y. ((x ∈ \<Union>T ∧ y ∈ \<Union>T ∧  x≠y) -->
  (∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0))";

text{*If a topology is $T_1$ then it is $T_0$. 
  We don't really assume here that $T$ is a topology on $X$. 
  Instead, we prove the relation between isT0 condition and isT1. *}

lemma T1_is_T0: assumes A1: "T {is T1}" shows "T {is T0}"
proof -
  from A1 have "∀ x y. x ∈ \<Union>T ∧ y ∈ \<Union>T ∧ x≠y --> 
    (∃U∈T. x∈U ∧ y∉U)"
    using isT1_def by simp;
  then have "∀ x y. x ∈ \<Union>T ∧ y ∈ \<Union>T ∧ x≠y --> 
    (∃U∈T. x∈U ∧ y∉U ∨ y∈U ∧ x∉U)"
    by auto;
  then show "T {is T0}" using isT0_def by simp;
qed;

text{*If a topology is $T_2$ then it is $T_1$.*}

lemma T2_is_T1: assumes A1: "T {is T2}" shows "T {is T1}"
proof -
  { fix x y assume "x ∈ \<Union>T"  "y ∈ \<Union>T"  "x≠y"
    with A1 have "∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0"
      using isT2_def by auto;
    then have "∃U∈T. x∈U ∧ y∉U" by auto;
  } then have "∀ x y. x ∈ \<Union>T ∧ y ∈ \<Union>T ∧  x≠y --> 
      (∃U∈T. x∈U ∧ y∉U)" by simp;
  then show "T {is T1}" using isT1_def by simp;
qed;

text{*In a $T_0$ space two points that can not be separated 
  by an open set are equal. Proof by contradiction.*}

lemma Top_1_1_L1: assumes A1: "T {is T0}" and A2: "x ∈ \<Union>T"  "y ∈ \<Union>T"
  and A3: "∀U∈T. (x∈U <-> y∈U)" 
  shows "x=y"
proof -
  { assume "x≠y"
    with A1 A2 have "∃U∈T. x∈U ∧ y∉U ∨ y∈U ∧ x∉U"
      using isT0_def by simp;
    with A3 have False by auto;
  } then show "x=y" by auto;
qed;

text{*In a $T_2$ space two points can be separated by an open set with its 
  boundary.*}

lemma (in topology0) Top_1_1_L2:
  assumes A1: "T {is T2}"  and A2: "x ∈ \<Union>T"  "y ∈ \<Union>T"   "x≠y"
  shows "∃U∈T. (x∈U ∧ y ∉ cl(U))"
proof -
  from A1 A2 have "∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0"
    using isT2_def by simp;
  then obtain U V where "U∈T"  "V∈T"  "x∈U"  "y∈V"  "U∩V=0"
    by auto;
  then have "U∈T ∧ x∈U ∧ y∈ V ∧ cl(U) ∩ V = 0" using Top_3_L14 
    by simp;
  then show "∃U∈T. (x∈U ∧ y ∉ cl(U))" by auto;
qed;


text{*In a $T_2$ space compact sets are closed. Doing a formal proof of this 
  theorem gave me an interesting insight into the role of 
  the Axiom of Choice in romantic proofs.

  A typical romantic proof of this fact goes like this: we want to show 
  that the complement of $K$ is open. To do this, 
  choose an arbitrary point $y\in K^c$.
  Since $X$ is $T_2$, for every point $x\in K$ we can find an 
  open set $U_x$ such that $y\notin \overline{U_x}$. 
  Obviously $\{U_x\}_{x\in K}$ covers $K$, so select a finite subcollection
  that covers $K$, and so on. I have never realized that 
  such reasoning requires (an) Axiom of Choice. 
  Namely, suppose we have a lemma that 
  states "In $T_2$ spaces, if $x\neq y$, then there is an open set 
  $U$ such that $x\in U$ and $y\notin \overline{U}$" (like our 
  @{text "Top_1_1_L2"} above). This only states that
  the set of such open sets $U$ is not empty. To get the collection 
  $\{U_x \}_{x\in K}$ in the above proof we have to select one such set 
  among many for every $x\in K$ and this is where we use (an) Axiom of Choice. 
  Probably in 99/100 cases when a romatic calculus proof states something like
  $\forall \varepsilon \exists \delta_\varepsilon \cdots$ the proof uses 
  Axiom of Choice. In the proof below we avoid using Axiom of Choice 
  (read it to find out how). It is an interesting question which such calculus 
  proofs can be reformulated so that the usage of AC is avoided. I remember 
  Sierpi\'{n}ski published a paper in 1919 (or was it 1914? my memory is not 
  that good any more) where he showed that one needs an Axiom of Choice to show
  the equivalence of the Heine and Cauchy definitions of limits.
 *}

theorem (in topology0) in_t2_compact_is_cl:
  assumes A1: "T {is T2}" and A2: "K {is compact in} T"
  shows "K {is closed in} T"
proof -
  { fix y assume A3: "y ∈ \<Union>T"  "y∉K" 
    have "∃U∈T. y∈U ∧ U ⊆ \<Union>T - K"
    proof -
      let ?B = "\<Union>x∈K.{V∈T. x∈V ∧ y∉ cl(V)}"
      have I: "?B ∈ Pow(T)"  "Fin(?B) ⊆ Pow(?B)" 
        using Fin.dom_subset by auto;
      from A2 A3 have "∀x∈K. x ∈ \<Union>T ∧ y ∈ \<Union>T ∧ x≠y"
        using IsCompact_def by auto;
      with A1 have "∀x∈K. {V∈T. x∈V ∧ y ∉ cl(V)} ≠ 0"
        using Top_1_1_L2 by auto;
      hence "K ⊆ \<Union>?B" by blast;
      with A2 I have "∃N ∈ Fin(?B). K ⊆ \<Union>N" using IsCompact_def 
        by auto;
      then obtain N where D1: "N ∈ Fin(?B)"  "K ⊆ \<Union>N" 
        by auto;
      with I have "N ⊆ ?B" by auto;
      hence II: "∀V∈N. V∈?B" by auto;
      let ?M = "{cl(V). V∈N}"
      let ?C = "{D∈Pow(\<Union>T). D {is closed in} T}"
      from topSpaceAssum have
        "∀V∈?B. (cl(V) {is closed in} T)"
        "∀V∈?B. (cl(V) ∈ Pow(\<Union>T))"
        using IsATopology_def Top_3_L7 IsClosed_def 
        by auto;(*blast no-go*)
      hence "∀V∈?B. cl(V) ∈ ?C" by simp;
      moreover from D1 have "N ∈ Fin(?B)" by simp;
      ultimately have "?M ∈ Fin(?C)" by (rule Finite1_L6);
      then have "\<Union>T - \<Union>?M ∈ T" using Top_3_L6 IsClosed_def 
        by simp;
      moreover from A3 II have "y ∈ \<Union>T - \<Union>?M" by simp;
      moreover have "\<Union>T - \<Union>?M ⊆ \<Union>T - K"
      proof -
        from II have "\<Union>N ⊆ \<Union>?M" using Top_3_L10 by auto;
        with D1 show "\<Union>T - \<Union>?M ⊆ \<Union>T - K" by auto;
      qed;
      ultimately have "∃U. U∈T ∧ y ∈ U ∧ U ⊆ \<Union>T - K"
        by auto;
      then show "∃U∈T. y∈U ∧ U ⊆ \<Union>T - K" by auto;
    qed;
  } then have "∀y ∈ \<Union>T - K. ∃U∈T. y∈U ∧ U ⊆ \<Union>T - K"
    by auto;
  with A2 show "K {is closed in} T" 
    using Top_2_L8 IsCompact_def IsClosed_def by auto;
qed;  

section{*Bases and subbases.*}

text{*A base of topology is a collection of open sets such that every 
  open set is a union of the sets from the base. A subbase is a collection 
  of open sets such that finite intersection of those sets form a base.
  Below we formulate a condition that we will prove to be necessary and 
  sufficient for a collection $B$ of open sets to form a base. 
  It says that for any two sets $U,V$ from the collection $B$ we can
  find a point $x\in U\cap V$ with a neighboorhod from $B$ contained in $U\cap V$.
  *}

constdefs

  IsAbaseFor (infixl "{is a base for}" 65)
  "B {is a base for} T ≡ B⊆T ∧ T = {\<Union>A. A∈Pow(B)}"

  IsAsubBaseFor (infixl "{is a subbase for}" 65)
  "B {is a subbase for} T ≡ 
  B ⊆ T ∧ {\<Inter>A. A∈Fin(B)} {is a base for} T"

  SatisfiesBaseCondition ("_ {satisfies the base condition}" [50] 50)  
  "B {satisfies the base condition} ≡ 
  ∀U V. ((U∈B ∧ V∈B) --> (∀x ∈ U∩V. ∃W∈B. x∈W ∧ W ⊆ U∩V))"

text{*Each open set is a union of some sets from the base.*}

lemma Top_1_2_L1: assumes "B {is a base for} T"  and "U∈T" 
  shows "∃A∈Pow(B). U = \<Union>A"
  using prems IsAbaseFor_def by simp;

text{*A necessary conditionfor a collection of sets to be a base for some 
  topology : every point in the intersection
  of two sets in the base has a neighboorhood from the base contained
  in the intersection.*}

lemma Top_1_2_L2: 
  assumes A1:"∃T. T {is a topology} ∧ B {is a base for} T"
  and A2: "V∈B"  "W∈B"
  shows "∀ x ∈ V∩W. ∃U∈B. x∈U ∧ U ⊆ V ∩ W"
proof -
  from A1 obtain T where 
    D1: "T {is a topology}"   "B {is a base for} T"
    by auto;
  then have "B ⊆ T" using IsAbaseFor_def by auto;
  with A2 have "V∈T" and "W∈T" using IsAbaseFor_def by auto;
  with D1 have "∃A∈Pow(B). V∩W = \<Union>A" using IsATopology_def Top_1_2_L1
    by auto;
  then obtain A where "A ⊆ B" and "V ∩ W = \<Union>A" by auto;
  then show "∀ x ∈ V∩W. ∃U∈B. (x∈U ∧ U ⊆ V ∩ W)" by auto;
qed;

text{*We will construct a topology as the collection of unions of (would-be)
  base. First we prove that if the collection of sets satisfies the 
  condition we want to show to be sufficient, the the intersection belongs
  to what we will define as topology (am I clear here?). Having this fact 
  ready simplifies the proof of the next lemma. There is not much topology
  here, just some set theory.*}

lemma Top_1_2_L3:
  assumes A1: "∀x∈ V∩W . ∃U∈B. x∈U ∧ U ⊆ V∩W"
  shows "V∩W ∈ {\<Union>A. A∈Pow(B)}"
proof
  let ?A = "\<Union>x∈V∩W. {U∈B. x∈U ∧ U ⊆ V∩W}"
  show "?A∈Pow(B)" by auto;
  from A1 show "V∩W = \<Union>?A" by blast;
qed;

text{*The next lemma is needed when proving that the would-be topology is
  closed with respect to taking intersections. We show here that intersection
  of two sets from this (would-be) topology can be written as union of sets 
  from the topology.*}

lemma Top_1_2_L4:
  assumes A1:  "U1 ∈ {\<Union>A. A∈Pow(B)}"   "U2 ∈ {\<Union>A. A∈Pow(B)}"
  and A2: "B {satisfies the base condition}"
  shows "∃C. C ⊆ {\<Union>A. A∈Pow(B)} ∧ U1∩U2 = \<Union>C"
proof -
  from A1 A2 obtain A1 A2 where 
    D1: "A1∈ Pow(B)"  "U1 = \<Union>A1"  "A2 ∈ Pow(B)"  "U2 = \<Union>A2" 
    by auto;
  let ?C = "\<Union>U∈A1.{U∩V. V∈A2}"
  from D1 have "(∀U∈A1. U∈B) ∧ (∀V∈A2. V∈B)" by auto;
  with A2 have "?C ⊆ {\<Union>A . A ∈ Pow(B)}"
    using Top_1_2_L3 SatisfiesBaseCondition_def by auto;
  moreover from D1 have "U1 ∩ U2 = \<Union>?C" by auto;
  ultimately show ?thesis by auto;
qed;

text{*If $B$ satisfies the base condition, then the collection of unions
  of sets from $B$ is a topology and $B$ is a base for this topology.*}

theorem Top_1_2_T1:
  assumes A1: "B {satisfies the base condition}"
  and A2: "T = {\<Union>A. A∈Pow(B)}"
  shows "T {is a topology}" and "B {is a base for} T"
proof -
  show "T {is a topology}"
  proof -
    from A2 have "0∈T" by auto;
    moreover have I: "∀C∈Pow(T). \<Union>C ∈ T"
    proof -
      { fix C assume A3: "C ∈ Pow(T)"
        let ?Q = "\<Union> {\<Union>{A∈Pow(B). U = \<Union>A}. U∈C}"
        from A2 A3 have "∀U∈C. ∃A∈Pow(B). U = \<Union>A" by auto;
        then have "\<Union>?Q = \<Union>C" using  Finite1_L8 by simp;
        moreover from A2 have "\<Union>?Q ∈ T" by auto;
        ultimately have "\<Union>C ∈ T" by simp;
      } thus "∀C∈Pow(T). \<Union>C ∈ T" by auto;
    qed;
    moreover have "∀U∈T. ∀ V∈T. U∩V ∈ T"
    proof -
      { fix U V assume  "U ∈ T"  "V ∈ T"
        with A1 A2 have "∃C.(C ⊆ T ∧ U∩V = \<Union>C)"
          using Top_1_2_L4 by simp;
        then obtain C where "C ⊆ T" and  "U∩V = \<Union>C"
          by auto;
        with I have "U∩V ∈ T" by simp;
      } then show "∀U∈T. ∀ V∈T. U∩V ∈ T" by simp;
    qed
    ultimately show "T {is a topology}" using IsATopology_def
      by simp;
  qed;
  from A2 have "B⊆T" by auto;
  with A2 show "B {is a base for} T" using IsAbaseFor_def 
    by simp;
qed;

text{*The carrier of the base and topology are the same.*}

lemma Top_1_2_L5: assumes "B {is a base for} T"
  shows "\<Union>T = \<Union>B"
  using prems IsAbaseFor_def by auto;

section{*Product topology*}

text{*In this section we consider a topology defined on a product of two sets.*}

text{*Given two topological spaces we can define a topology on the product of 
  the carriers such that the cartesian products of the sets of the topologies 
  are a base for the product topology. Recall that for two collections $S,T$ 
  of sets the product collection
  is defined (in @{text "ZF1.thy"}) as the collections of cartesian 
  products $A\times B$, where $A\in S, B\in T$.*}

constdefs

  "ProductTopology(T,S) ≡ {\<Union>W. W ∈ Pow(ProductCollection(T,S))}"


text{*The product collection satisfies the base condition.*}

lemma Top_1_4_L1: 
  assumes A1: "T {is a topology}"   "S {is a topology}"
  and A2: "A ∈ ProductCollection(T,S)"  "B ∈ ProductCollection(T,S)"
  shows "∀x∈(A∩B). ∃W∈ProductCollection(T,S). (x∈W ∧ W ⊆ A ∩ B)"
proof
  fix x assume A3: "x ∈ A∩B"
  from A2 obtain U1 V1 U2 V2 where 
    D1: "U1∈T"  "V1∈S"   "A=U1×V1"  "U2∈T"  "V2∈S"   "B=U2×V2"
    using ProductCollection_def by auto;
  let ?W = "(U1∩U2) × (V1∩V2)";
  from A1 D1 have "U1∩U2 ∈ T" and "V1∩V2 ∈ S"
    using IsATopology_def by auto;
  then have "?W ∈ ProductCollection(T,S)" using ProductCollection_def 
    by auto;
  moreover from A3 D1 have "x∈?W" and "?W ⊆ A∩B" by auto;
  ultimately have "∃W. (W ∈ ProductCollection(T,S) ∧ x∈W ∧ W ⊆ A∩B)"
    by auto;
  thus "∃W∈ProductCollection(T,S). (x∈W ∧ W ⊆ A ∩ B)" by auto;
qed;

text{*The product topology is indeed a topology on the product.*}

theorem Top_1_4_T1: assumes A1: "T {is a topology}"  "S {is a topology}"
  shows 
  "ProductTopology(T,S) {is a topology}"
  "ProductCollection(T,S) {is a base for} ProductTopology(T,S)"
  "\<Union> ProductTopology(T,S) = \<Union>T × \<Union>S"
proof -
  from A1 show 
    "ProductTopology(T,S) {is a topology}"
    "ProductCollection(T,S) {is a base for} ProductTopology(T,S)"
    using Top_1_4_L1 ProductCollection_def 
      SatisfiesBaseCondition_def ProductTopology_def Top_1_2_T1 
    by auto;
  then show "\<Union> ProductTopology(T,S) = \<Union>T × \<Union>S"
    using Top_1_2_L5 ZF1_1_L6 by simp;
qed;

end