# Theory Topology_ZF

theory Topology_ZF
imports Finite_ZF Fol1
(*     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 APARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOTLIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS ORBUSINESS 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 THEUSE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.*)header{*\isaheader{Topology\_ZF.thy}*}theory Topology_ZF imports ZF1 Finite_ZF Fol1begintext{* 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). \<Union>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) ≡ \<Union> {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 ⊆ \<Union>T ∧ \<Union>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(\<Union>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) ≡ \<Inter> 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(\<Union>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 ⊆ \<Union>T ∧   (∀ M∈Pow(T). K ⊆ \<Union>M --> (∃ N ∈ FinPow(M). K ⊆ \<Union>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)). \<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 autoqed;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 "\<Union>0 ∈ T" using IsATopology_def by blast  thus "0 ∈ T" by simpqedtext{*Union of a collection of open sets is open.*}lemma union_open: assumes "T {is a topology}" and "∀A∈\<A>. A ∈ T"  shows "(\<Union>\<A>) ∈ 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 "(\<Union>i∈I. P(i)) ∈ T"  using assms union_open by simptext{*The intersection of any nonempty collection of topologies on a set $X$ is a topology.*}lemma Inter_tops_is_top:   assumes A1: "\<M> ≠ 0" and A2: "∀T∈\<M>. T {is a topology}"  shows "(\<Inter>\<M>) {is a topology}"proof -  { 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 simpqed;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 "\<Inter>N ∈ T"  using topSpaceAssum assms IsATopology_def inter_two_inter_fin   by simptext{*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). \<Union>A ∈ ?S"  proof    fix A assume A1: "A∈Pow(?S)"    have "∀V∈A. \<Union> {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 "\<Union>?M ∈ T" using IsATopology_def by simp      } thus ?thesis by simp    qed    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 blast    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 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 simpqed;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 autotext{*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 autoqedtext{*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 autonext assume A1: "int(U) = U"  have "int(U) ∈ T" using Top_2_L2 by simp  with A1 show "U∈T" by simpqed  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 simpqedtext{*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 autoqedtext{*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 autotext{*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 autotext{*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 autoqedtext{*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 simpqedsection{*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 simpqedtext{*Empty set is closed.*}lemma (in topology0) Top_3_L2: shows "0 {is closed in} T"  using topSpaceAssum  IsATopology_def IsClosed_def by simptext{*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  thus ?thesis by autoqedtext{*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 simpqedtext{*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 "(\<Inter> {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 "(\<Union>T - D⇩1) ∩ (\<Union>T - D⇩2) ∈ T"    using IsClosed_def IsATopology_def by simp  moreover have "(\<Union>T - D⇩1) ∩ (\<Union>T - D⇩2) = \<Union>T - (D⇩1 ∪ D⇩2)"     by auto  moreover from A1 have "D⇩1 ∪ D⇩2 ⊆ \<Union>T" using IsClosed_def    by auto  ultimately show "(D⇩1∪D⇩2) {is closed in} T" using IsClosed_def    by simpqedtext{*Finite union of closed sets is closed. To understand the proof   recall that $D\in$@{text "Pow(\<Union>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(\<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∈?C. ∀B∈?C. A∪B ∈ ?C"    using Top_3_L5 by auto  moreover note A1  ultimately have "\<Union>N ∈ ?C" by (rule union_two_union_fin)  thus "(\<Union>N) {is closed in} T" by simpqedtext{*Closure of a set is closed.*}lemma (in topology0) cl_is_closed: assumes "A ⊆ \<Union>T"  shows "cl(A) {is closed in} T"  using assms Closure_def Top_3_L3 ClosedCovers_def Top_3_L4  by simptext{*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 autoqedtext{*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 cl_is_closed Top_3_L5 Boundary_def by autoqedtext{*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 autonext assume "cl(A) = A"  then have "\<Union>T - A = \<Union>T - cl(A)" by simp  with A1 show "A {is closed in} T" using cl_is_closed IsClosed_def    by simpqedtext{*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 simpqedtext{*A set is contained in its closure.*}lemma (in topology0) cl_contains_set: assumes "A ⊆ \<Union>T" shows "A ⊆ cl(A)"  using assms Top_3_L1 ClosedCovers_def Top_3_L3 Closure_def by autotext{*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 cl_contains_set 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 cl_is_closed 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 autoqed 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 simpqedtext{*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 autoqed(*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 ⊆ \<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 cl_is_closed IsClosed_def by simp  then have "cl(U) -(\<Union>T - V) = cl(U) ∩ V" by auto  ultimately show "cl(U) ∩ V = 0" by simpqed;*)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 ⊆ \<Union>T"  "V∈T" and  A2: "A∩V = 0"  shows "cl(A) ∩ V = 0"proof -  from assms have "A ⊆ \<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(A) - (\<Union>T - V) = 0"     using Top_3_L13 by blast  moreover from A1 have "cl(A) ⊆ \<Union>T" using cl_is_closed IsClosed_def by simp  then have "cl(A) -(\<Union>T - V) = cl(A) ∩ V" by auto  ultimately show ?thesis by simpqedtext{*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 ⊆ \<Union>T" and "U∈T" and "x ∈ cl(A) ∩ U"  shows "A∩U ≠ 0" using assms disj_open_cl_disj by autotext{*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 ⊆ \<Union>T" and A2: "x∈\<Union>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 = "(\<Union>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 autoqedend