Theory Topology_ZF

(* 
    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.

*)

section ‹Topology - introduction›

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.› 

subsection‹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 ‹Pow(T)› 
  is the powerset of $T$, so that if $M\in$ ‹ 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 ‹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 ‹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 ‹FinPow(M)› is the collection of finite subsets of $M$ 
  (finite powerset of $M$), defined in IsarMathLib's ‹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‹The carrier is open.›
lemma carr_open: assumes "T {is a topology}" shows "(⋃T) ∈ T"
  using assms IsATopology_def by auto

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‹Singletons are compact. Interestingly we do not have
  to assume that $T$ is a topology for this.
  Note singletons do not have to be closed, we need the
  the space to be $T_1$ for that (see ‹Topology_ZF_1)›. ›

lemma singl_compact: 
  assumes "x∈⋃T" shows "{x} {is compact in} T"
  using assms singleton_in_finpow unfolding IsCompact_def
  by auto

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 ‹topology0› we assume that $T$ is a topology.
  The interior of the set $A$ (with respect to the topology in the context)
  is denoted ‹int(A)›. The closure of a set $A\subseteq \bigcup T$ is 
  denoted ‹cl(A)› and the boundary is ‹∂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

subsection‹Interior of a set›

text‹In this 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

text‹The intersection of interiors is a equal to the interior of intersections.›

lemma (in topology0) int_inter_int: shows "int(A) ∩ int(B) = int(A∩B)"
proof
  have "int(A) ∩ int(B) ⊆ A∩B" using Top_2_L1 by auto  
  moreover have "int(A) ∩ int(B) ∈ T" using Top_2_L2 IsATopology_def topSpaceAssum 
    by auto
  ultimately show "int(A) ∩ int(B) ⊆ int(A∩B)" using Top_2_L5 by simp
  have "A∩B ⊆ A" and "A∩B ⊆ B" by auto 
  then have "int(A∩B) ⊆ int(A)" and "int(A∩B) ⊆ int(B)" using interior_mono by auto
  thus "int(A∩B) ⊆ int(A) ∩ int(B)" by auto
qed 

subsection‹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$‹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, hence the complement of the closure is open.›

lemma (in topology0) cl_is_closed: assumes "A ⊆ ⋃T"
  shows "cl(A) {is closed in} T" and "⋃T - cl(A) ∈ T"
  using assms Top_3_L3 Top_3_L4 Closure_def ClosedCovers_def IsClosed_def
  by auto

text‹Closure of a bigger sets is bigger.›

lemma (in topology0) top_closure_mono: 
  assumes A1: "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 ‹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  ‹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