theory Topology_ZF imports ZF1 Finite_ZF Fol1
begin
This theory file provides basic definitions and properties of topology, open and closed sets, closure and boundary.
Basic definitions and properties
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.
Topology is a collection of sets that contains the empty set and is closed under arbitrary unions and intersections of two sets.
Definition
\( T \text{ is a topology } \equiv ( \forall M \in Pow(T).\ \bigcup M \in T ) \wedge \) \( ( \forall U\in T.\ \forall V\in T.\ U\cap V \in T) \)
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) \equiv \bigcup \{U\in T.\ U \subseteq A\} \)
A set is closed if it is contained in the carrier of topology and its complement is open.
Definition
\( D \text{ is closed in } T \equiv (D \subseteq \bigcup T \wedge \bigcup T - D \in T) \)
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) \equiv \{D \in Pow(\bigcup T).\ D \text{ is closed in } T \wedge A\subseteq D\} \)
The closure of a set \(A\) is defined as the intersection of the collection of closed sets that contain \(A\).
Definition
\( Closure(A,T) \equiv \bigcap ClosedCovers(A,T) \)
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) \equiv Closure(A,T) \cap Closure(\bigcup T - A,T) \)
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
\( K \text{ is compact in } T \equiv (K \subseteq \bigcup T \wedge \) \( (\forall M\in Pow(T).\ K \subseteq \bigcup M \longrightarrow (\exists N \in FinPow(M).\ K \subseteq \bigcup N))) \)
A basic example of a topology: the powerset of any set is a topology.
lemma Pow_is_top:
shows \( Pow(X) \text{ is a topology } \)proof have \( \forall A\in Pow(Pow(X)).\ \bigcup A \in Pow(X) \)
moreover
qed
have \( \forall U\in Pow(X).\ \forall V\in Pow(X).\ U\cap V \in Pow(X) \)
ultimately show \( Pow(X) \text{ is a topology } \) using IsATopology_def
Empty set is open.
lemma empty_open:
assumes A1: \( T \text{ is a topology } \)
shows \( 0 \in T \)proof have \( 0 \in Pow(T) \)
with A1 have \( \bigcup 0 \in T \) using IsATopology_def
thus \( 0 \in T \)
qed
The intersection of any nonempty collection of topologies on a set \(X\) is a topology.
lemma Inter_tops_is_top:
assumes A1: \( \mathcal{M} \neq 0 \) and A2: \( \forall T\in \mathcal{M} .\ T \text{ is a topology } \)
shows \( (\bigcap \mathcal{M} ) \text{ is a topology } \)proof{
}
fix \( A \)
assume \( A\in Pow(\bigcap \mathcal{M} ) \)
with A1 have \( \forall T\in \mathcal{M} .\ A\in Pow(T) \)
with A1, A2 have \( \bigcup A \in \bigcap \mathcal{M} \) using IsATopology_def
then have \( \forall A.\ A\in Pow(\bigcap \mathcal{M} ) \longrightarrow \bigcup A \in \bigcap \mathcal{M} \)
hence \( \forall A\in Pow(\bigcap \mathcal{M} ).\ \bigcup A \in \bigcap \mathcal{M} \)
moreover {
}
qed
fix \( U \) \( V \)
assume \( U \in \bigcap \mathcal{M} \) and \( V \in \bigcap \mathcal{M} \)
then have \( \forall T\in \mathcal{M} .\ U \in T \wedge V \in T \)
with A1, A2 have \( \forall T\in \mathcal{M} .\ U\cap V \in T \) using IsATopology_def
then have \( \forall U \in \bigcap \mathcal{M} .\ \forall V \in \bigcap \mathcal{M} .\ U\cap V \in \bigcap \mathcal{M} \)
ultimately show \( (\bigcap \mathcal{M} ) \text{ is a topology } \) using IsATopology_def
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 \( \partial A \).
Locale topology0
assumes topSpaceAssum: \( T \text{ is a topology } \)
defines \( int(A) \equiv Interior(A,T) \)
defines \( cl(A) \equiv Closure(A,T) \)
defines \( \partial A \equiv Boundary(A,T) \)
Intersection of a finite nonempty collection of open sets is open.
lemma (in topology0) fin_inter_open_open:
assumes \( N\neq 0 \), \( N \in FinPow(T) \)
shows \( \bigcap N \in T \) using topSpaceAssum , assms , IsATopology_def , inter_two_inter_finHaving 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 \text{ restricted to } X) \text{ is a topology } \)proof let \( S = T \text{ restricted to } X \)
have \( \forall A\in Pow(S).\ \bigcup A \in S \)proof
fix \( A \)
assume A1: \( A\in Pow(S) \)
have \( \forall V\in A.\ \bigcup \{U \in T.\ V = U\cap X\} \in T \)proof
{
}
fix \( V \)
let \( M = \{U \in T.\ V = U\cap X\} \)
have \( M \in Pow(T) \)
with topSpaceAssum have \( \bigcup M \in T \) using IsATopology_def
thus \( thesis \)
qed
hence \( \{\bigcup \{U\in T.\ V = U\cap X\}.\ V\in A\} \subseteq T \)
with topSpaceAssum have \( (\bigcup V\in A.\ \bigcup \{U\in T.\ V = U\cap X\}) \in T \) using IsATopology_def
then have \( (\bigcup V\in A.\ \bigcup \{U\in T.\ V = U\cap X\})\cap X \in S \) using RestrictedTo_def
moreover
qed
from A1 have \( \forall V\in A.\ \exists U\in T.\ V = U\cap X \) using RestrictedTo_def
hence \( (\bigcup V\in A.\ \bigcup \{U\in T.\ V = U\cap X\})\cap X = \bigcup A \)
ultimately show \( \bigcup A \in S \)
moreover
qed
have \( \forall U\in S.\ \forall V\in S.\ U\cap V \in S \)proof
ultimately show \( S \text{ is a topology } \) using IsATopology_def
{
}
fix \( U \) \( V \)
assume \( U\in S \), \( V\in S \)
then obtain \( U_1 \) \( V_1 \) where \( U_1 \in T \wedge U = U_1\cap X \) and \( V_1 \in T \wedge V = V_1\cap X \) using RestrictedTo_def
with topSpaceAssum have \( U_1\cap V_1 \in T \) and \( U\cap V = (U_1\cap V_1)\cap X \) using IsATopology_def
then have \( U\cap V \in S \) using RestrictedTo_def
thus \( \forall U\in S.\ \forall V\in S.\ U\cap V \in S \)
qed
Interior of a set
In section we show basic properties of the interior of a set.
Interior of a set \(A\) is contained in \(A\).
lemma (in topology0) Top_2_L1:
shows \( int(A) \subseteq A \) using Interior_defInterior is open.
lemma (in topology0) Top_2_L2:
shows \( int(A) \in T \)proof have \( \{U\in T.\ U\subseteq A\} \in Pow(T) \)
with topSpaceAssum show \( int(A) \in T \) using IsATopology_def , Interior_def
qed
A set is open iff it is equal to its interior.
lemma (in topology0) Top_2_L3:
shows \( U\in T \longleftrightarrow int(U) = U \)proof assume \( U\in T \)
then show \( int(U) = U \) using Interior_def
next
assume A1: \( int(U) = U \)
have \( int(U) \in T \) using Top_2_L2
with A1 show \( U\in T \)
qed
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\in T \) using Top_2_L2
then show \( int(int(A)) = int(A) \) using Top_2_L3
qed
Interior of a bigger set is bigger.
lemma (in topology0) interior_mono:
assumes A1: \( A\subseteq B \)
shows \( int(A) \subseteq int(B) \)proof from A1 have \( \forall U\in T.\ (U\subseteq A \longrightarrow U\subseteq B) \)
then show \( int(A) \subseteq int(B) \) using Interior_def
qed
An open subset of any set is a subset of the interior of that set.
lemma (in topology0) Top_2_L5:
assumes \( U\subseteq A \) and \( U\in T \)
shows \( U \subseteq int(A) \) using assms , Interior_defIf 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 \( \exists U\in T.\ (x\in U \wedge U\subseteq A) \)
shows \( x \in int(A) \) using assms , Interior_defA 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\in T \)
shows \( \forall x\in V.\ \exists U\in T.\ (x\in U \wedge U\subseteq V) \)proof from A1 have \( \forall x\in V.\ V\in T \wedge x \in V \wedge V \subseteq V \)
thus \( thesis \)
qed
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: \( \forall x\in V.\ \exists U\in T.\ (x\in U \wedge U\subseteq V) \)
shows \( V\in T \)proof from A1 have \( V = int(V) \) using Top_2_L1 , Top_2_L6
then show \( V\in T \) using Top_2_L3
qed
Closed sets, closure, boundary.
This section is devoted to closed sets and properties of the closure and boundary operators.
The carrier of the space is closed.
lemma (in topology0) Top_3_L1:
shows \( (\bigcup T) \text{ is closed in } T \)proof have \( \bigcup T - \bigcup T = 0 \)
with topSpaceAssum have \( \bigcup T - \bigcup T \in T \) using IsATopology_def
then show \( thesis \) using IsClosed_def
qed
Empty set is closed.
lemma (in topology0) Top_3_L2:
shows \( 0 \text{ is closed in } T \) using topSpaceAssum , IsATopology_def , IsClosed_defThe 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 \subseteq \bigcup T \)
shows \( ClosedCovers(A,T) \neq 0 \)proof from A1 have \( \bigcup T \in ClosedCovers(A,T) \) using ClosedCovers_def , Top_3_L1
thus \( thesis \)
qed
Intersection of a nonempty family of closed sets is closed.
lemma (in topology0) Top_3_L4:
assumes A1: \( K\neq 0 \) and A2: \( \forall D\in K.\ D \text{ is closed in } T \)
shows \( (\bigcap K) \text{ is closed in } T \)proof from A2 have I: \( \forall D\in K.\ (D \subseteq \bigcup T \wedge (\bigcup T - D)\in T) \) using IsClosed_def
then have \( \{\bigcup T - D.\ D\in K\} \subseteq T \)
with topSpaceAssum have \( (\bigcup \{\bigcup T - D.\ D\in K\}) \in T \) using IsATopology_def
moreover
qed
from A1 have \( \bigcup \{\bigcup T - D.\ D\in K\} = \bigcup T - \bigcap K \)
moreover from A1, I have \( \bigcap K \subseteq \bigcup T \)
ultimately show \( (\bigcap K) \text{ is closed in } T \) using IsClosed_def
The union and intersection of two closed sets are closed.
lemma (in topology0) Top_3_L5:
assumes A1: \( D_1 \text{ is closed in } T \), \( D_2 \text{ is closed in } T \)
shows \( (D_1\cap D_2) \text{ is closed in } T \), \( (D_1\cup D_2) \text{ is closed in } T \)proof have \( \{D_1,D_2\} \neq 0 \)
with A1 have \( (\bigcap \{D_1,D_2\}) \text{ is closed in } T \) using Top_3_L4
thus \( (D_1\cap D_2) \text{ is closed in } T \)
from topSpaceAssum, A1 have \( (\bigcup T - D_1) \cap (\bigcup T - D_2) \in T \) using IsClosed_def , IsATopology_def
moreover
qed
have \( (\bigcup T - D_1) \cap (\bigcup T - D_2) = \bigcup T - (D_1 \cup D_2) \)
moreover from A1 have \( D_1 \cup D_2 \subseteq \bigcup T \) using IsClosed_def
ultimately show \( (D_1\cup D_2) \text{ is closed in } T \) using IsClosed_def
Finite union of closed sets is closed. To understand the proof recall that \(D\in\)\( Pow(\bigcup T) \) means that \(D\) is a subset of the carrier of the topology.
lemma (in topology0) fin_union_cl_is_cl:
assumes A1: \( N \in FinPow(\{D\in Pow(\bigcup T).\ D \text{ is closed in } T\}) \)
shows \( (\bigcup N) \text{ is closed in } T \)proof let \( C = \{D\in Pow(\bigcup T).\ D \text{ is closed in } T\} \)
have \( 0\in C \) using Top_3_L2
moreover
qed
have \( \forall A\in C.\ \forall B\in C.\ A\cup B \in C \) using Top_3_L5
moreover note A1
ultimately have \( \bigcup N \in C \) by (rule union_two_union_fin )
thus \( (\bigcup N) \text{ is closed in } T \)
Closure of a set is closed.
lemma (in topology0) cl_is_closed:
assumes \( A \subseteq \bigcup T \)
shows \( cl(A) \text{ is closed in } T \) using assms , Closure_def , Top_3_L3 , ClosedCovers_def , Top_3_L4Closure of a bigger sets is bigger.
lemma (in topology0) top_closure_mono:
assumes A1: \( A \subseteq \bigcup T \), \( B \subseteq \bigcup T \) and A2: \( A\subseteq B \)
shows \( cl(A) \subseteq cl(B) \)proof from A2 have \( ClosedCovers(B,T)\subseteq ClosedCovers(A,T) \) using ClosedCovers_def
with A1 show \( thesis \) using Top_3_L3 , Closure_def
qed
Boundary of a set is closed.
lemma (in topology0) boundary_closed:
assumes A1: \( A \subseteq \bigcup T \)
shows \( \partial A \text{ is closed in } T \)proof from A1 have \( \bigcup T - A \subseteq \bigcup T \)
with A1 show \( \partial A \text{ is closed in } T \) using cl_is_closed , Top_3_L5 , Boundary_def
qed
A set is closed iff it is equal to its closure.
lemma (in topology0) Top_3_L8:
assumes A1: \( A \subseteq \bigcup T \)
shows \( A \text{ is closed in } T \longleftrightarrow cl(A) = A \)proof assume \( A \text{ is closed in } T \)
with A1 show \( cl(A) = A \) using Closure_def , ClosedCovers_def
next
assume \( cl(A) = A \)
then have \( \bigcup T - A = \bigcup T - cl(A) \)
with A1 show \( A \text{ is closed in } T \) using cl_is_closed , IsClosed_def
qed
Complement of an open set is closed.
lemma (in topology0) Top_3_L9:
assumes A1: \( A\in T \)
shows \( (\bigcup T - A) \text{ is closed in } T \)proof from topSpaceAssum, A1 have \( \bigcup T - (\bigcup T - A) = A \) and \( \bigcup T - A \subseteq \bigcup T \) using IsATopology_def
with A1 show \( (\bigcup T - A) \text{ is closed in } T \) using IsClosed_def
qed
A set is contained in its closure.
lemma (in topology0) cl_contains_set:
assumes \( A \subseteq \bigcup T \)
shows \( A \subseteq cl(A) \) using assms , Top_3_L1 , ClosedCovers_def , Top_3_L3 , Closure_defClosure 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 \subseteq \bigcup T \)
shows \( cl(A) \subseteq \bigcup T \), \( cl(\bigcup T - A) = \bigcup T - int(A) \)proof from A1 show \( cl(A) \subseteq \bigcup T \) using Top_3_L1 , Closure_def , ClosedCovers_def
from A1 have \( \bigcup T - A \subseteq \bigcup T - int(A) \) using Top_2_L1
moreover
have I: \( \bigcup T - int(A) \subseteq \bigcup T \), \( \bigcup T - A \subseteq \bigcup T \)
ultimately have \( cl(\bigcup T - A) \subseteq cl(\bigcup T - int(A)) \) using top_closure_mono
moreover
from I have \( (\bigcup T - int(A)) \text{ is closed in } T \) using Top_2_L2 , Top_3_L9
with I have \( cl((\bigcup T) - int(A)) = \bigcup T - int(A) \) using Top_3_L8
ultimately have \( cl(\bigcup T - A) \subseteq \bigcup T - int(A) \)
moreover
qed
from I have \( \bigcup T - A \subseteq cl(\bigcup T - A) \) using cl_contains_set
hence \( \bigcup T - cl(\bigcup T - A) \subseteq A \) and \( \bigcup T - A \subseteq \bigcup T \)
then have \( \bigcup T - cl(\bigcup T - A) \subseteq int(A) \) using cl_is_closed , IsClosed_def , Top_2_L5
hence \( \bigcup T - int(A) \subseteq cl(\bigcup T - A) \)
ultimately show \( cl(\bigcup T - A) = \bigcup T - int(A) \)
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 \subseteq \bigcup T \)
shows \( \partial A = cl(A) - int(A) \)proof from A1 have \( \partial A = cl(A) \cap (\bigcup T - int(A)) \) using Boundary_def , Top_3_L11
moreover
qed
from A1 have \( cl(A) \cap (\bigcup T - int(A)) = cl(A) - int(A) \) using Top_3_L11
ultimately show \( \partial A = cl(A) - int(A) \)
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 \text{ is closed in } T \), \( A\subseteq B \)
shows \( cl(A) \subseteq B \)proof from A1 have \( B \subseteq \bigcup T \) using IsClosed_def
with A1 show \( cl(A) \subseteq B \) using ClosedCovers_def , Closure_def
qed
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\in T \), \( V\in T \) and A2: \( U\cap V = 0 \)
shows \( cl(U) \cap V = 0 \)proof from topSpaceAssum, A1 have I: \( U \subseteq \bigcup T \) using IsATopology_def
with A2 have \( U \subseteq \bigcup T - V \)
moreover
from A1 have \( (\bigcup T - V) \text{ is closed in } T \) using Top_3_L9
ultimately have \( cl(U) - (\bigcup T - V) = 0 \) using Top_3_L13
moreover
qed
from I have \( cl(U) \subseteq \bigcup T \) using cl_is_closed , IsClosed_def
then have \( cl(U) -(\bigcup T - V) = cl(U) \cap V \)
ultimately show \( cl(U) \cap V = 0 \)
end
Definition of IsATopology:
\( T \text{ is a topology } \equiv ( \forall M \in Pow(T).\ \bigcup M \in T ) \wedge \)
\( ( \forall U\in T.\ \forall V\in T.\ U\cap V \in T) \)
lemma inter_two_inter_fin: assumes \( \forall V\in T.\ \forall W\in T.\ V \cap W \in T \) and \( N \neq 0 \) and \( N \in FinPow(T) \) shows \( (\bigcap N \in T) \)
Definition of RestrictedTo:
\( M \text{ restricted to } X \equiv \{X \cap A .\ A \in M\} \)
Definition of Interior:
\( Interior(A,T) \equiv \bigcup \{U\in T.\ U \subseteq A\} \)
lemma (in topology0) Top_2_L2: shows \( int(A) \in T \)
lemma (in topology0) Top_2_L3: shows \( U\in T \longleftrightarrow int(U) = U \)
lemma (in topology0) Top_2_L1: shows \( int(A) \subseteq A \)
lemma (in topology0) Top_2_L6: assumes \( \exists U\in T.\ (x\in U \wedge U\subseteq A) \) shows \( x \in int(A) \)
Definition of IsClosed:
\( D \text{ is closed in } T \equiv (D \subseteq \bigcup T \wedge \bigcup T - D \in T) \)
Definition of ClosedCovers:
\( ClosedCovers(A,T) \equiv \{D \in Pow(\bigcup T).\ D \text{ is closed in } T \wedge A\subseteq D\} \)
lemma (in topology0) Top_3_L1: shows \( (\bigcup T) \text{ is closed in } T \)
lemma (in topology0) Top_3_L4: assumes \( K\neq 0 \) and \( \forall D\in K.\ D \text{ is closed in } T \) shows \( (\bigcap K) \text{ is closed in } T \)
lemma (in topology0) Top_3_L2: shows \( 0 \text{ is closed in } T \)
lemma (in topology0) Top_3_L5: assumes \( D_1 \text{ is closed in } T \), \( D_2 \text{ is closed in } T \) shows \( (D_1\cap D_2) \text{ is closed in } T \), \( (D_1\cup D_2) \text{ is closed in } T \)
lemma union_two_union_fin: assumes \( 0 \in C \) and \( \forall A\in C.\ \forall B\in C.\ A\cup B \in C \) and \( N \in FinPow(C) \) shows \( \bigcup N \in C \)
Definition of Closure:
\( Closure(A,T) \equiv \bigcap ClosedCovers(A,T) \)
lemma (in topology0) Top_3_L3: assumes \( A \subseteq \bigcup T \) shows \( ClosedCovers(A,T) \neq 0 \)
lemma (in topology0) cl_is_closed: assumes \( A \subseteq \bigcup T \) shows \( cl(A) \text{ is closed in } T \)
Definition of Boundary:
\( Boundary(A,T) \equiv Closure(A,T) \cap Closure(\bigcup T - A,T) \)
lemma (in topology0) top_closure_mono: assumes \( A \subseteq \bigcup T \), \( B \subseteq \bigcup T \) and \( A\subseteq B \) shows \( cl(A) \subseteq cl(B) \)
lemma (in topology0) Top_3_L9: assumes \( A\in T \) shows \( (\bigcup T - A) \text{ is closed in } T \)
lemma (in topology0) Top_3_L8: assumes \( A \subseteq \bigcup T \) shows \( A \text{ is closed in } T \longleftrightarrow cl(A) = A \)
lemma (in topology0) cl_contains_set: assumes \( A \subseteq \bigcup T \) shows \( A \subseteq cl(A) \)
lemma (in topology0) Top_2_L5: assumes \( U\subseteq A \) and \( U\in T \) shows \( U \subseteq int(A) \)
lemma (in topology0) Top_3_L11: assumes \( A \subseteq \bigcup T \) shows \( cl(A) \subseteq \bigcup T \), \( cl(\bigcup T - A) = \bigcup T - int(A) \)
lemma (in topology0) Top_3_L13: assumes \( B \text{ is closed in } T \), \( A\subseteq B \) shows \( cl(A) \subseteq B \)
