This theory file provides basic definitions and properties of topology, open and closed sets, closure and boundary.

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 \( \text{ClosedCovers}(A,T) \).

** Definition **

\( \text{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 **

\( \text{Closure}(A,T) \equiv \bigcap \text{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 **

\( \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:

Empty set is open.

** lemma ** empty_open:

** assumes **\( T \text{ is a topology } \)

The carrier is open.

** lemma ** carr_open:

** assumes **\( T \text{ is a topology } \)

Union 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 \)

Union 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 \)

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 } \)

{
** 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 ** {
** 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
** qed **

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 \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) \)

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:

{
** 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 **

{
** 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 **

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:

Interior is open.

** lemma ** **(in** topology0**)** Top_2_L2:

A set is open iff it is equal to its interior.

** lemma ** **(in** topology0**)** Top_2_L3:

Interior of the interior is the interior.

** lemma ** **(in** topology0**)** Top_2_L4:

Interior of a bigger set is bigger.

** lemma ** **(in** topology0**)** interior_mono:

** assumes **A1: \( A\subseteq B \)

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 \)

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 **\( \exists U\in T.\ (x\in U \wedge U\subseteq A) \)

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\in T \)

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) \)

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:

Empty set is closed.

** lemma ** **(in** topology0**)** Top_3_L2:

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 \subseteq \bigcup T \)

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 \)

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 \)

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\}) \)

Closure of a set is closed.

** lemma ** **(in** topology0**)** cl_is_closed:

** assumes **\( A \subseteq \bigcup T \)

Closure 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 \)

Boundary of a set is closed.

** lemma ** **(in** topology0**)** boundary_closed:

** assumes **A1: \( A \subseteq \bigcup T \)

A set is closed iff it is equal to its closure.

** lemma ** **(in** topology0**)** Top_3_L8:

** assumes **A1: \( A \subseteq \bigcup T \)

Complement of an open set is closed.

** lemma ** **(in** topology0**)** Top_3_L9:

** assumes **A1: \( A\in T \)

A set is contained in its closure.

** lemma ** **(in** topology0**)** cl_contains_set:

** assumes **\( A \subseteq \bigcup T \)

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 \subseteq \bigcup T \)

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 \)

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 \)

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 \)

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 \)

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 \subseteq \bigcup T \)** and **A2: \( x\in \bigcup T \)** and **A3: \( \forall U\in T.\ x\in U \longrightarrow U\cap A \neq 0 \)

{
** 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 **

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) \)

** assumes **\( T \text{ is a topology } \)** and **\( \forall A\in \mathcal{A} .\ A \in T \)

** assumes **\( \forall V\in T.\ \forall W\in T.\ V \cap W \in T \)** and **\( N \neq 0 \)** and **\( N \in \text{FinPow}(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\} \)

** assumes **\( \exists U\in T.\ (x\in U \wedge U\subseteq A) \)

Definition of IsClosed:
\( D \text{ is closed in } T \equiv (D \subseteq \bigcup T \wedge \bigcup T - D \in T) \)

Definition of ClosedCovers:
\( \text{ClosedCovers}(A,T) \equiv \{D \in Pow(\bigcup T).\ D \text{ is closed in } T \wedge A\subseteq D\} \)

** assumes **\( K\neq 0 \)** and **\( \forall D\in K.\ D \text{ is closed in } T \)

** assumes **\( D_1 \text{ is closed in } T \), \( D_2 \text{ is closed in } T \)

** assumes **\( 0 \in C \)** and **\( \forall A\in C.\ \forall B\in C.\ A\cup B \in C \)** and **\( N \in \text{FinPow}(C) \)

Definition of Closure:
\( \text{Closure}(A,T) \equiv \bigcap \text{ClosedCovers}(A,T) \)

** assumes **\( A \subseteq \bigcup T \)

** assumes **\( A \subseteq \bigcup T \)

Definition of Boundary:
\( \text{Boundary}(A,T) \equiv \text{Closure}(A,T) \cap \text{Closure}(\bigcup T - A,T) \)

** assumes **\( A \subseteq \bigcup T \), \( B \subseteq \bigcup T \)** and **\( A\subseteq B \)

** assumes **\( A\in T \)

** assumes **\( A \subseteq \bigcup T \)

** assumes **\( A \subseteq \bigcup T \)

** assumes **\( U\subseteq A \)** and **\( U\in T \)

** assumes **\( A \subseteq \bigcup T \)

** assumes **\( B \text{ is closed in } T \), \( A\subseteq B \)

** assumes **\( A \subseteq \bigcup T \), \( V\in T \)** and **\( A\cap V = 0 \)