# Theory Topology_ZF

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

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}"  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 ("∂_"  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