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 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 \( \text{Interior}(A,T) \) to denote the interior of A.
definition
\( \text{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 \( Closed \text{Covers}(A,T) \).
definition
\( Closed \text{Covers}(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
\( \text{Closure}(A,T) \equiv \bigcap Closed \text{Covers}(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
\( \text{Boundary}(A,T) \equiv \text{Closure}(A,T) \cap \text{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 \( \text{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 \text{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 \( T \text{ is a topology } \)
shows \( 0 \in T \)proof have \( 0 \in Pow(T) \)
with assms have \( \bigcup 0 \in T \) using IsATopology_def
thus \( 0 \in T \)
qed
The carrier is open.
lemma carr_open:
assumes \( T \text{ is a topology } \)
shows \( (\bigcup T) \in T \) using assms, IsATopology_defUnion of a collection of open sets is open.
lemma union_open:
assumes \( T \text{ is a topology } \) and \( \forall A\in \mathcal{A} .\ A \in T \)
shows \( (\bigcup \mathcal{A} ) \in T \) using assms, IsATopology_defUnion of a indexed family of open sets is open.
lemma union_indexed_open:
assumes A1: \( T \text{ is a topology } \) and A2: \( \forall i\in I.\ P(i) \in T \)
shows \( (\bigcup i\in I.\ P(i)) \in T \) using assms, union_openThe 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
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\in \bigcup T \)
shows \( \{x\} \text{ is compact in } T \) using assms, singleton_in_finpow unfolding IsCompact_defWe 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 \text{Interior}(A,T) \)
defines \( cl(A) \equiv \text{Closure}(A,T) \)
defines \( \partial A \equiv \text{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 \text{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 this 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
The intersection of interiors is a equal to the interior of intersections.
lemma (in topology0) int_inter_int:
shows \( int(A) \cap int(B) = int(A\cap B) \)proof have \( int(A) \cap int(B) \subseteq A\cap B \) using Top_2_L1
moreover
have \( int(A) \cap int(B) \in T \) using Top_2_L2, IsATopology_def, topSpaceAssum
ultimately show \( int(A) \cap int(B) \subseteq int(A\cap B) \) using Top_2_L5
have \( A\cap B \subseteq A \) and \( A\cap B \subseteq B \)
then have \( int(A\cap B) \subseteq int(A) \) and \( int(A\cap B) \subseteq int(B) \) using interior_mono
thus \( int(A\cap B) \subseteq int(A) \cap int(B) \)
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 \( Closed \text{Covers}(A,T) \neq 0 \)proof from A1 have \( \bigcup T \in Closed \text{Covers}(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 \text{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, hence the complement of the closure is open.
lemma (in topology0) cl_is_closed:
assumes \( A \subseteq \bigcup T \)
shows \( cl(A) \text{ is closed in } T \) and \( \bigcup T - cl(A) \in T \) using assms, Top_3_L3, Top_3_L4, Closure_def, ClosedCovers_def, IsClosed_defClosure of a bigger sets is bigger.
lemma (in topology0) top_closure_mono:
assumes A1: \( B \subseteq \bigcup T \) and A2: \( A\subseteq B \)
shows \( cl(A) \subseteq cl(B) \)proof from A2 have \( Closed \text{Covers}(B,T)\subseteq Closed \text{Covers}(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 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 \subseteq \bigcup T \), \( V\in T \) and A2: \( A\cap V = 0 \)
shows \( cl(A) \cap V = 0 \)proof from assms have \( A \subseteq \bigcup T - V \)
moreover
from A1 have \( (\bigcup T - V) \text{ is closed in } T \) using Top_3_L9
ultimately have \( cl(A) - (\bigcup T - V) = 0 \) using Top_3_L13
moreover
qed
from A1 have \( cl(A) \subseteq \bigcup T \) using cl_is_closed, IsClosed_def
then have \( cl(A) -(\bigcup T - V) = cl(A) \cap V \)
ultimately show \( thesis \)
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 \subseteq \bigcup T \) and \( U\in T \) and \( x \in cl(A) \cap U \)
shows \( A\cap U \neq 0 \) using assms, disj_open_cl_disjA 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 \subseteq \bigcup T \) and A2: \( x\in \bigcup T \) and A3: \( \forall U\in T.\ x\in U \longrightarrow U\cap A \neq 0 \)
shows \( x \in cl(A) \)proof{
}
assume \( x \notin cl(A) \)
with A1 obtain \( D \) where \( D \text{ is closed in } T \) and \( A\subseteq D \) and \( x\notin D \) using Top_3_L3, Closure_def, ClosedCovers_def
let \( U = (\bigcup T) - D \)
from A2, \( D \text{ is closed in } T \), \( x\notin D \), \( A\subseteq D \) have \( U\in T \), \( x\in U \) and \( U\cap A = 0 \) unfolding IsClosed_def
with A3 have \( False \)
thus \( thesis \)
qed
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 union_open:
assumes \( T \text{ is a topology } \) and \( \forall A\in \mathcal{A} .\ A \in T \)
shows \( (\bigcup \mathcal{A} ) \in T \) lemma singleton_in_finpow:
assumes \( x \in X \)
shows \( \{x\} \in \text{FinPow}(X) \)Definition of IsCompact:
\( 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 \text{FinPow}(M).\ K \subseteq \bigcup N))) \)
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 \text{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:
\( \text{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) \) lemma (in topology0) Top_2_L5:
assumes \( U\subseteq A \) and \( U\in T \)
shows \( U \subseteq int(A) \) lemma (in topology0) interior_mono:
assumes \( A\subseteq B \)
shows \( int(A) \subseteq int(B) \)Definition of IsClosed:
\( D \text{ is closed in } T \equiv (D \subseteq \bigcup T \wedge \bigcup T - D \in T) \)
Definition of ClosedCovers:
\( Closed \text{Covers}(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 \text{FinPow}(C) \)
shows \( \bigcup N \in C \) lemma (in topology0) Top_3_L3:
assumes \( A \subseteq \bigcup T \)
shows \( Closed \text{Covers}(A,T) \neq 0 \)Definition of Closure:
\( \text{Closure}(A,T) \equiv \bigcap Closed \text{Covers}(A,T) \)
lemma (in topology0) cl_is_closed:
assumes \( A \subseteq \bigcup T \)
shows \( cl(A) \text{ is closed in } T \) and \( \bigcup T - cl(A) \in T \)Definition of Boundary:
\( \text{Boundary}(A,T) \equiv \text{Closure}(A,T) \cap \text{Closure}(\bigcup T - A,T) \)
lemma (in topology0) top_closure_mono:
assumes \( 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_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 \) lemma (in topology0) disj_open_cl_disj:
assumes \( A \subseteq \bigcup T \), \( V\in T \) and \( A\cap V = 0 \)
shows \( cl(A) \cap V = 0 \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8