This theory deals with some concrete examples of topologies.

In this section we define and prove the basic properties of the co-cardinal topology on a set \(X\).

The collection of subsets of a set whose complement is strictly bounded by a cardinal is a topology given some assumptions on the cardinal.

** definition **

\( \text{CoCardinal}(X,T) \equiv \{F\in Pow(X).\ X-F \prec T\}\cup \{0\} \)

For any set and any infinite cardinal we prove that
\( \text{CoCardinal}(X,Q) \) forms a topology. The proof is done
with an infinite cardinal, but it is obvious that the set *Q*
can be any set equipollent with an infinite cardinal.
It is a topology also if the set where the topology is defined is
too small or the cardinal too large; in this case, as it is later proved the topology
is a discrete topology. And the last case corresponds with \( "Q=1" \) which translates
in the indiscrete topology.

** lemma ** CoCar_is_topology:

** assumes **\( InfCard (Q) \)

We can use theorems proven in *topology0* context for the co-cardinal topology.

** theorem ** topology0_CoCardinal:

** assumes **\( \text{InfCard}(T) \)

It can also be proven that if \( \text{CoCardinal}(X,T) \) is a topology,
\( X\neq 0, \text{Card}(T) \) and \( T\neq 0 \); then *T* is an infinite cardinal, \( X\prec T \)
or \( T=1 \).
It follows from the fact that the union of two closed sets is closed. Choosing the appropriate cardinals, the cofinite and the cocountable topologies
are obtained.

The cofinite topology is a very special topology because it is closely related to the separation axiom \(T_1\). It also appears naturally in algebraic geometry.

** definition **

\( CoFinite X \equiv \text{CoCardinal}(X,nat) \)

Cocountable topology in fact consists of the empty set and all cocountable subsets of \(X\).

** definition **

\( CoCountable X \equiv \text{CoCardinal}(X,\text{csucc}(nat)) \)

There are several assertions that can be done to the \( \text{CoCardinal}(X,T) \) topology. In each case, we will not assume sufficient conditions for \( \text{CoCardinal}(X,T) \) to be a topology, but they will be enough to do the calculations in every posible case.

The topology is defined in the set \(X\)

** lemma ** union_cocardinal:

** assumes **\( T\neq 0 \)

The closed sets are the small subsets of \(X\) and \(X\) itself.

** lemma ** closed_sets_cocardinal:

** assumes **\( T\neq 0 \)

{
** assume **A: \( D \subseteq X \), \( X - D \in \text{CoCardinal}(X,T) \), \( D \neq X \)
** from **A(1,3) ** have ** \( X-(X-D)=D \), \( X-D\neq 0 \)
** with **A(2) ** have ** \( D\prec T \)** using ** CoCardinal_def
** } **
** with **assms ** have ** \( D \text{ is closed in } \text{CoCardinal}(X,T) \longrightarrow (D\in Pow(X) \wedge D\prec T)\vee D=X \)** using ** IsClosed_def, union_cocardinal
** moreover ** {
** assume **A: \( D \prec T \), \( D \subseteq X \)
** from **A(2) ** have ** \( X-(X-D)=D \)
** with **A(1) ** have ** \( X-(X-D)\prec T \)
** then **** have ** \( X-D\in \text{CoCardinal}(X,T) \)** using ** CoCardinal_def
** } **
** with **assms ** have ** \( (D\in Pow(X) \wedge D\prec T)\longrightarrow D \text{ is closed in } \text{CoCardinal}(X,T) \)** using ** union_cocardinal, IsClosed_def ** moreover ** ** have ** \( X-X=0 \)
** then **** have ** \( X-X\in \text{CoCardinal}(X,T) \)** using ** CoCardinal_def
** with **assms ** have ** \( X\text{ is closed in } \text{CoCardinal}(X,T) \)** using ** union_cocardinal, IsClosed_def ** ultimately **** show ** \( thesis \)
** qed **

The interior of a set is itself if it is open or *0* if
it isn't open.

** lemma ** interior_set_cocardinal:

** assumes **noC: \( T\neq 0 \)** and **\( A\subseteq X \)

\(X\) is a closed set that contains \(A\).
This lemma is necessary because we cannot use the lemmas proven in the
*topology0* context since \(T\neq 0\) is too weak for \( \text{CoCardinal}(X,T) \)
to be a topology.

** lemma ** X_closedcov_cocardinal:

** assumes **\( T\neq 0 \), \( A\subseteq X \)

The closure of a set is itself if it is closed or \(X\) if it isn't closed.

** lemma ** closure_set_cocardinal:

** assumes **\( T\neq 0 \), \( A\subseteq X \)

{
** assume **\( A \prec T \)
** with **assms ** have ** \( A \text{ is closed in } \text{CoCardinal}(X,T) \)** using ** closed_sets_cocardinal
** with **assms(2) ** have ** \( A\in \{D \in Pow(X).\ D \text{ is closed in } \text{CoCardinal}(X,T) \wedge A\subseteq D\} \)
** with **assms(1) ** have ** S: \( A\in Closed \text{Covers}(A,\text{CoCardinal}(X,T)) \)** using ** ClosedCovers_def** using ** union_cocardinal
** hence ** l1: \( \bigcap Closed \text{Covers}(A,\text{CoCardinal}(X,T))\subseteq A \)
** from **S ** have ** l2: \( A \subseteq \bigcap Closed \text{Covers}(A,\text{CoCardinal}(X,T)) \)** unfolding ** ClosedCovers_def
** from **l1, l2 ** have ** \( \text{Closure}(A,\text{CoCardinal}(X,T))=A \)** using ** Closure_def
** } **
** moreover ** {
** assume **as: \( \neg A \prec T \)
{
** fix **\( U \) ** assume **\( A\subseteq U \)
** then **** have ** Q: \( A \preceq U \)** using ** subset_imp_lepoll
{
** assume **\( U\prec T \)
** with **Q ** have ** \( A\prec T \)** using ** lesspoll_trans1
** with **as ** have ** \( False \)
** } **
** hence ** \( \neg U \prec T \)
** with **assms(1) ** have ** \( \neg (U \text{ is closed in } \text{CoCardinal}(X,T)) \vee U=X \)** using ** closed_sets_cocardinal
** } **
** with **assms(1) ** have ** \( \forall U\in Pow(X).\ U\text{ is closed in }\text{CoCardinal}(X,T) \wedge A\subseteq U\longrightarrow U=X \)
** with **assms(1) ** have ** \( Closed \text{Covers}(A,\text{CoCardinal}(X,T))\subseteq \{X\} \)** using ** union_cocardinal** using ** ClosedCovers_def
** with **assms ** have ** \( Closed \text{Covers}(A,\text{CoCardinal}(X,T))=\{X\} \)** using ** X_closedcov_cocardinal
** then **** have ** \( \text{Closure}(A,\text{CoCardinal}(X,T)) = X \)** using ** Closure_def
** } **
** ultimately **** show ** \( thesis \)
** qed **

The boundary of a set is empty if \(A\) and \(X-A\) are closed,
*X* if not \(A\) neither \(X-A\) are closed and; if only one is closed,
then the closed one is its boundary.

** lemma ** boundary_cocardinal:

** assumes **\( T\neq 0 \), \( A\subseteq X \)

If the set is too small or the cardinal too large, then the topology is just the discrete topology.

** lemma ** discrete_cocardinal:

** assumes **\( X\prec T \)

{
** fix **\( U \) ** assume **\( U\in \text{CoCardinal}(X,T) \)
** then **** have ** \( U \in Pow(X) \)** using ** CoCardinal_def
** } **
** then **** show ** \( \text{CoCardinal}(X,T) \subseteq Pow(X) \)
{
** fix **\( U \) ** assume **A: \( U \in Pow(X) \)
** then **** have ** \( X-U \subseteq X \)
** then **** have ** \( X-U \preceq X \)** using ** subset_imp_lepoll
** then **** have ** \( X-U\prec T \)** using ** lesspoll_trans1, assms
** with **A ** have ** \( U\in \text{CoCardinal}(X,T) \)** using ** CoCardinal_def
** } **
** then **** show ** \( Pow(X) \subseteq \text{CoCardinal}(X,T) \)
** qed **

If the cardinal is taken as \( T=1 \) then the topology is indiscrete.

** lemma ** indiscrete_cocardinal:

{
** fix **\( Q \) ** assume **\( Q \in \text{CoCardinal}(X,1) \)
** then **** have ** \( Q \in Pow(X) \)** and **\( Q=0 \vee X-Q\prec 1 \)** using ** CoCardinal_def
** then **** have ** \( Q \in Pow(X) \)** and **\( Q=0 \vee X-Q=0 \)** using ** lesspoll_succ_iff, lepoll_0_iff
** then **** have ** \( Q=0 \vee Q=X \)
** } **
** then **** show ** \( \text{CoCardinal}(X,1) \subseteq \{0, X\} \)
** have ** \( 0 \in \text{CoCardinal}(X,1) \)** using ** CoCardinal_def
** moreover ** ** have ** \( 0\prec 1 \)** and **\( X-X=0 \)** using ** lesspoll_succ_iff
** then **** have ** \( X\in \text{CoCardinal}(X,1) \)** using ** CoCardinal_def ** ultimately **** show ** \( \{0, X\} \subseteq \text{CoCardinal}(X,1) \)
** qed **

The topological subspaces of the \( \text{CoCardinal}(X,T) \) topology are also CoCardinal topologies.

** lemma ** subspace_cocardinal:

{
** fix **\( M \) ** assume **\( M \in (\text{CoCardinal}(X,T) \text{ restricted to } Y) \)
** then **** obtain **\( A \)** where **A1: \( A \in \text{CoCardinal}(X,T) \), \( M=Y \cap A \)** using ** RestrictedTo_def
** then **** have ** \( M \in Pow(X \cap Y) \)** using ** CoCardinal_def
** moreover ** ** from **A1 ** have ** \( (Y \cap X)-M = (Y \cap X)-A \)** using ** CoCardinal_def
** with **\( (Y \cap X)-M = (Y \cap X)-A \) ** have ** \( (Y \cap X)-M\subseteq X-A \)
** then **** have ** \( (Y \cap X)-M \preceq X-A \)** using ** subset_imp_lepoll
** with **A1 ** have ** \( (Y \cap X)-M \prec T \vee M=0 \)** using ** lesspoll_trans1, CoCardinal_def ** ultimately **** have ** \( M \in \text{CoCardinal}(Y\cap X, T) \)** using ** CoCardinal_def
** } **
** then **** show ** \( \text{CoCardinal}(X,T) \text{ restricted to } Y \subseteq \text{CoCardinal}(Y\cap X,T) \)
{
** fix **\( M \) ** let **\( A = M \cup (X-Y) \) ** assume **A: \( M \in \text{CoCardinal}(Y \cap X,T) \)
{
** assume **\( M=0 \)
** hence ** \( M=0 \cap Y \)
** then **** have ** \( M\in \text{CoCardinal}(X,T) \text{ restricted to } Y \)** using ** RestrictedTo_def, CoCardinal_def
** } **
** moreover ** {
** assume **AS: \( M\neq 0 \)
** from **A, AS ** have ** A1: \( (M\in Pow(Y \cap X) \wedge (Y \cap X)-M\prec T) \)** using ** CoCardinal_def
** hence ** \( A\in Pow(X) \)
** moreover ** ** have ** \( X-A=(Y \cap X)-M \)
** with **A1 ** have ** \( X-A\prec T \) ** ultimately **** have ** \( A\in \text{CoCardinal}(X,T) \)** using ** CoCardinal_def
** then **** have ** AT: \( Y \cap A\in \text{CoCardinal}(X,T) \text{ restricted to } Y \)** using ** RestrictedTo_def ** have ** \( Y \cap A=Y \cap M \)
** also ** ** from **A1 ** have ** \( \ldots =M \)
** finally **** have ** \( Y \cap A=M \)
** with **AT ** have ** \( M\in \text{CoCardinal}(X,T) \text{ restricted to } Y \)
** } **
** ultimately **** have ** \( M\in \text{CoCardinal}(X,T) \text{ restricted to } Y \)
** } **
** then **** show ** \( \text{CoCardinal}(Y \cap X, T) \subseteq \text{CoCardinal}(X,T) \text{ restricted to } Y \)
** qed **

In this section, we consider all the subsets of a set which have empty intersection with a fixed set.

The excluded set topology consists of subsets of \(X\) that are disjoint with a fixed set \(U\).

** definition **

\( \text{ExcludedSet}(X,U) \equiv \{F\in Pow(X).\ U \cap F=0\}\cup \{X\} \)

For any set; we prove that \( \text{ExcludedSet}(X,Q) \) forms a topology.

** theorem ** excludedset_is_topology:

{
** fix **\( M \) ** assume **\( M \in Pow(\text{ExcludedSet}(X,Q)) \)
** then **** have ** A: \( M\subseteq \{F\in Pow(X).\ Q \cap F=0\}\cup \{X\} \)** using ** ExcludedSet_def
** hence ** \( \bigcup M\in Pow(X) \)
** moreover ** {
** have ** B: \( Q \cap \bigcup M=\bigcup \{Q \cap T.\ T\in M\} \)
{
** assume **\( X\notin M \)
** with **A ** have ** \( M\subseteq \{F\in Pow(X).\ Q \cap F=0\} \)
** with **B ** have ** \( Q \cap \bigcup M=0 \)
** } **
** moreover ** {
** assume **\( X\in M \)
** with **A ** have ** \( \bigcup M=X \)
** } **
** ultimately **** have ** \( Q \cap \bigcup M=0 \vee \bigcup M=X \)
** } **
** ultimately **** have ** \( \bigcup M\in \text{ExcludedSet}(X,Q) \)** using ** ExcludedSet_def
** } **
** moreover ** {
** fix **\( U \) \( V \) ** assume **\( U\in \text{ExcludedSet}(X,Q) \), \( V\in \text{ExcludedSet}(X,Q) \)
** then **** have ** \( U\in Pow(X) \), \( V\in Pow(X) \), \( U=X\vee U \cap Q=0 \), \( V=X\vee V \cap Q=0 \)** using ** ExcludedSet_def
** hence ** \( U\in Pow(X) \), \( V\in Pow(X) \), \( (U \cap V)=X \vee Q\cap (U \cap V)=0 \)
** then **** have ** \( (U \cap V)\in \text{ExcludedSet}(X,Q) \)** using ** ExcludedSet_def
** } **
** ultimately **** show ** \( thesis \)** using ** IsATopology_def
** qed **

We can use *topology0* when discussing excluded set topology.

** theorem ** topology0_excludedset:

Choosing a singleton set, it is considered a point in excluded topology.

** definition **

\( \text{ExcludedPoint}(X,p) \equiv \text{ExcludedSet}(X,\{p\}) \)

Here we discuss what are closed sets, interior, closure and boundary in excluded set topology.

The topology is defined in the set \(X\)

** lemma ** union_excludedset:

The closed sets are those which contain the set \( (X \cap T) \) and *0*.

** lemma ** closed_sets_excludedset:

{
** fix **\( x \) ** assume **A: \( D \subseteq X \), \( X-D \in \text{ExcludedSet}(X,T) \), \( D\neq 0 \), \( x\in T \), \( x\in X \)
** from **A(1) ** have ** B: \( X-(X-D)=D \)
** from **A(2) ** have ** \( T\cap (X-D)=0\vee X-D=X \)** using ** ExcludedSet_def
** hence ** \( T\cap (X-D)=0\vee X-(X-D)=X-X \)
** with **B ** have ** \( T\cap (X-D)=0\vee D=X-X \)
** hence ** \( T\cap (X-D)=0\vee D=0 \)
** with **A(3) ** have ** \( T\cap (X-D)=0 \)
** with **A(4) ** have ** \( x\notin X-D \)
** with **A(5) ** have ** \( x\in D \)
** } **
** moreover ** {
** assume **A: \( X\cap T\subseteq D \), \( D\subseteq X \)
** from **A(1) ** have ** \( X-D\subseteq X-(X\cap T) \)
** also ** ** have ** \( \ldots = X-T \)
** finally **** have ** \( T\cap (X-D) = 0 \)
** moreover ** ** have ** \( X-D \in Pow(X) \)
** ultimately **** have ** \( X-D \in \text{ExcludedSet}(X,T) \)** using ** ExcludedSet_def
** } **
** ultimately **** show ** \( thesis \)** using ** IsClosed_def, union_excludedset, ExcludedSet_def
** qed **

The interior of a set is itself if it is *X* or the difference with the set *T*

** lemma ** interior_set_excludedset:

** assumes **\( A\subseteq X \)

{
** assume **A: \( A\neq X \)
** from **assms ** have ** \( A-T \in \text{ExcludedSet}(X,T) \)** using ** ExcludedSet_def
** then **** have ** \( A-T\subseteq \text{Interior}(A,\text{ExcludedSet}(X,T)) \)** using ** Interior_def
** moreover ** {
** fix **\( U \) ** assume **\( U \in \text{ExcludedSet}(X,T) \), \( U\subseteq A \)
** then **** have ** \( T\cap U=0 \vee U=X \), \( U\subseteq A \)** using ** ExcludedSet_def
** with **A, assms ** have ** \( T\cap U=0 \), \( U\subseteq A \)
** then **** have ** \( U-T=U \), \( U-T\subseteq A-T \)
** then **** have ** \( U\subseteq A-T \)
** } **
** then **** have ** \( \text{Interior}(A,\text{ExcludedSet}(X,T))\subseteq A-T \)** using ** Interior_def ** ultimately **** have ** \( \text{Interior}(A,\text{ExcludedSet}(X,T))=A-T \)
** } **
** moreover ** ** have ** \( X\in \text{ExcludedSet}(X,T) \)** using ** ExcludedSet_def, union_excludedset
** then **** have ** \( \text{Interior}(X,\text{ExcludedSet}(X,T)) = X \)** using ** Top_2_L3, topology0_excludedset ** ultimately **** show ** \( thesis \)
** qed **

The closure of a set is itself if it is *0* or
the union with *T*.

** lemma ** closure_set_excludedset:

** assumes **\( A\subseteq X \)

The boundary of a set is *0* if \(A\) is *X* or *0*, and \( X\cap T \) in other case.

** lemma ** boundary_excludedset:

** assumes **\( A\subseteq X \)

{
** have ** \( \text{Closure}(0,\text{ExcludedSet}(X,T))=0 \), \( \text{Closure}(X - 0,\text{ExcludedSet}(X,T))=X \)** using ** closure_set_excludedset
** then **** have ** \( \text{Boundary}(0,\text{ExcludedSet}(X,T)) = 0 \)** using ** Boundary_def** using ** union_excludedset, assms
** } **
** moreover ** {
** have ** \( X-X=0 \)
** then **** have ** \( \text{Closure}(X,\text{ExcludedSet}(X,T)) = X \)** and **\( \text{Closure}(X-X,\text{ExcludedSet}(X,T)) = 0 \)** using ** closure_set_excludedset
** then **** have ** \( \text{Boundary}(X,\text{ExcludedSet}(X,T)) = 0 \)** unfolding ** Boundary_def** using ** union_excludedset
** } **
** moreover ** {
** assume **\( A\neq 0 \)** and **\( A\neq X \)
** then **** have ** \( X-A\neq 0 \)** using ** assms
** with **assms, \( A\neq 0 \), \( A\subseteq X \) ** have ** \( \text{Closure}(A,\text{ExcludedSet}(X,T)) = A \cup (X\cap T) \)** using ** closure_set_excludedset
** moreover ** ** from **\( A\subseteq X \) ** have ** \( X-A \subseteq X \)
** with **\( X-A\neq 0 \) ** have ** \( \text{Closure}(X-A,\text{ExcludedSet}(X,T)) = (X-A) \cup (X\cap T) \)** using ** closure_set_excludedset ** ultimately **** have ** \( \text{Boundary}(A,\text{ExcludedSet}(X,T)) = X\cap T \)** using ** Boundary_def, union_excludedset
** } **
** ultimately **** show ** \( thesis \)
** qed **

This section provides some miscellaneous facts about excluded set topologies.

The excluded set topology is equal in the sets *T* and \( X\cap T \).

** lemma ** smaller_excludedset:

If the set which is excluded is disjoint with *X*,
then the topology is discrete.

** lemma ** empty_excludedset:

** assumes **\( T\cap X=0 \)

The topological subspaces of the *ExcludedSet X T* topology
are also ExcludedSet topologies.

** lemma ** subspace_excludedset:

{
** fix **\( M \) ** assume **\( M\in (\text{ExcludedSet}(X,T) \text{ restricted to } Y) \)
** then **** obtain **\( A \)** where **A1: \( A:\text{ExcludedSet}(X,T) \), \( M=Y \cap A \)** unfolding ** RestrictedTo_def
** then **** have ** \( M\in Pow(X \cap Y) \)** unfolding ** ExcludedSet_def
** moreover ** ** from **A1 ** have ** \( T\cap M=0\vee M=Y\cap X \)** unfolding ** ExcludedSet_def
** ultimately **** have ** \( M \in \text{ExcludedSet}(Y \cap X,T) \)** unfolding ** ExcludedSet_def
** } **
** then **** show ** \( \text{ExcludedSet}(X,T) \text{ restricted to } Y \subseteq \text{ExcludedSet}(Y\cap X,T) \)
{
** fix **\( M \) ** let **\( A = M \cup ((X\cap Y-T)-Y) \) ** assume **A: \( M \in \text{ExcludedSet}(Y\cap X,T) \)
{
** assume **\( M = Y \cap X \)
** then **** have ** \( M \in \text{ExcludedSet}(X,T) \text{ restricted to } Y \)** unfolding ** RestrictedTo_def, ExcludedSet_def
** } **
** moreover ** {
** assume **AS: \( M\neq Y \cap X \)
** from **A, AS ** have ** A1: \( (M\in Pow(Y \cap X) \wedge T\cap M=0) \)** unfolding ** ExcludedSet_def
** then **** have ** \( A\in Pow(X) \)
** moreover ** ** have ** \( T\cap A=T\cap M \)
** with **A1 ** have ** \( T\cap A=0 \) ** ultimately **** have ** \( A \in \text{ExcludedSet}(X,T) \)** unfolding ** ExcludedSet_def
** then **** have ** AT: \( Y \cap A \in \text{ExcludedSet}(X,T) \text{ restricted to } Y \)** unfolding ** RestrictedTo_def ** have ** \( Y \cap A=Y \cap M \)
** also ** ** have ** \( \ldots =M \)** using ** A1
** finally **** have ** \( Y\cap A = M \)
** with **AT ** have ** \( M \in \text{ExcludedSet}(X,T) \text{ restricted to } Y \)
** } **
** ultimately **** have ** \( M \in \text{ExcludedSet}(X,T) \text{ restricted to } Y \)
** } **
** then **** show ** \( \text{ExcludedSet}(Y \cap X,T) \subseteq \text{ExcludedSet}(X,T) \text{ restricted to } Y \)
** qed **

In this section we consider the subsets of a set which contain a fixed set. The family defined in this section and the one in the previous section are dual; meaning that the closed set of one are the open sets of the other.

We define the included set topology as the collection of supersets of some fixed subset of the space \(X\).

** definition **

\( \text{IncludedSet}(X,U) \equiv \{F\in Pow(X).\ U \subseteq F\} \cup \{0\} \)

In the next theorem we prove that *IncludedSet X Q* forms a topology.

** theorem ** includedset_is_topology:

{
** fix **\( M \) ** assume **\( M \in Pow(\text{IncludedSet}(X,Q)) \)
** then **** have ** A: \( M\subseteq \{F\in Pow(X).\ Q \subseteq F\}\cup \{0\} \)** using ** IncludedSet_def
** then **** have ** \( \bigcup M\in Pow(X) \)
** moreover ** ** have ** \( Q \subseteq \bigcup M\vee \bigcup M=0 \)** using ** A
** ultimately **** have ** \( \bigcup M\in \text{IncludedSet}(X,Q) \)** using ** IncludedSet_def
** } **
** moreover ** {
** fix **\( U \) \( V \) ** assume **\( U\in \text{IncludedSet}(X,Q) \), \( V\in \text{IncludedSet}(X,Q) \)
** then **** have ** \( U\in Pow(X) \), \( V\in Pow(X) \), \( U=0\vee Q\subseteq U \), \( V=0\vee Q\subseteq V \)** using ** IncludedSet_def
** then **** have ** \( U\in Pow(X) \), \( V\in Pow(X) \), \( (U \cap V)=0 \vee Q\subseteq (U \cap V) \)
** then **** have ** \( (U \cap V)\in \text{IncludedSet}(X,Q) \)** using ** IncludedSet_def
** } **
** ultimately **** show ** \( thesis \)** using ** IsATopology_def
** qed **

We can reference the theorems proven in the *topology0* context when discussing
the included set topology.

** theorem ** topology0_includedset:

Choosing a singleton set, it is considered a point excluded topology. In the following lemmas and theorems, when neccessary it will be considered that \( T\neq 0 \) and \( T\subseteq X \). These cases will appear in the special cases section.

** definition **

\( IncludedPoint X p \equiv \text{IncludedSet}(X,\{p\}) \)

This section discusses total set, closed sets, interior, closure and boundary for included set topology.

The topology is defined in the set \(X\).

** lemma ** union_includedset:

** assumes **\( T\subseteq X \)

The closed sets are those which are disjoint with *T*
and *X*.

** lemma ** closed_sets_includedset:

** assumes **\( T\subseteq X \)

The interior of a set is itself if it is open or the empty set if it isn't.

** lemma ** interior_set_includedset:

** assumes **\( A\subseteq X \)

{
** fix **\( x \) ** assume **A: \( \text{Interior}(A,\text{IncludedSet}(X,T)) \neq 0 \), \( x\in T \)
** have ** \( \text{Interior}(A,\text{IncludedSet}(X,T)) \in \text{IncludedSet}(X,T) \)** using ** Top_2_L2, topology0_includedset
** with **A(1) ** have ** \( T \subseteq \text{Interior}(A,\text{IncludedSet}(X,T)) \)** using ** IncludedSet_def
** with **A(2) ** have ** \( x \in \text{Interior}(A,\text{IncludedSet}(X,T)) \)
** then **** have ** \( x\in A \)** using ** Top_2_L1, topology0_includedset
** } **
** moreover ** {
** assume **\( T\subseteq A \)
** with **assms ** have ** \( A\in \text{IncludedSet}(X,T) \)** using ** IncludedSet_def
** then **** have ** \( \text{Interior}(A,\text{IncludedSet}(X,T)) = A \)** using ** Top_2_L3, topology0_includedset
** } **
** ultimately **** show ** \( thesis \)
** qed **

The closure of a set is itself if it is closed or the whole space if it is not.

** lemma ** closure_set_includedset:

** assumes **\( A\subseteq X \), \( T\subseteq X \)

{
** assume **AS: \( T\cap A=0 \)
** then **** have ** \( A \text{ is closed in } \text{IncludedSet}(X,T) \)** using ** closed_sets_includedset, assms
** with **assms(1) ** have ** \( \text{Closure}(A,\text{IncludedSet}(X,T))=A \)** using ** Top_3_L8, topology0_includedset, union_includedset, assms(2)
** } **
** moreover ** {
** assume **AS: \( T\cap A \neq 0 \)
** have ** \( X\in Closed \text{Covers}(A,\text{IncludedSet}(X,T)) \)** using ** ClosedCovers_def, closed_sets_includedset, union_includedset, assms
** then **** have ** l1: \( \bigcap Closed \text{Covers}(A,\text{IncludedSet}(X,T))\subseteq X \)** using ** Closure_def
** moreover ** {
** fix **\( U \) ** assume **\( U\in Closed \text{Covers}(A,\text{IncludedSet}(X,T)) \)
** then **** have ** \( U\text{ is closed in }\text{IncludedSet}(X,T) \), \( A\subseteq U \)** using ** ClosedCovers_def
** then **** have ** \( U=X\vee (T\cap U)=0 \), \( A\subseteq U \)** using ** closed_sets_includedset, assms(2)
** then **** have ** \( U=X\vee (T\cap A)=0 \)
** then **** have ** \( U=X \)** using ** AS
** } **
** then **** have ** \( X \subseteq \bigcap Closed \text{Covers}(A,\text{IncludedSet}(X,T)) \)** using ** Top_3_L3, topology0_includedset, union_includedset, assms ** ultimately **** have ** \( \bigcap Closed \text{Covers}(A,\text{IncludedSet}(X,T))=X \)
** then **** have ** \( \text{Closure}(A,\text{IncludedSet}(X,T)) = X \)** using ** Closure_def
** } **
** ultimately **** show ** \( thesis \)
** qed **

The boundary of a set is \( X-A \) if \(A\) contains *T* completely, is *A* if \(X-A\) contains *T*
completely and *X* if *T* is divided between the two sets.
The case where \( T=0 \) is considered as a special case.

** lemma ** boundary_includedset:

** assumes **\( A\subseteq X \), \( T\subseteq X \), \( T\neq 0 \)

In this section we discuss some corner cases when some parameters in our definitions are empty and provide some facts about subspaces in included set topologies.

The topology is discrete if \( T=0 \)

** lemma ** smaller_includedset:

If the set which is included is not a subset of *X*,
then the topology is trivial.

** lemma ** empty_includedset:

** assumes **\( \neg (T\subseteq X) \)

The topological subspaces of the \( \text{IncludedSet}(X,T) \) topology are also IncludedSet topologies. The trivial case does not fit the idea in the demonstration because if \( Y\subseteq X \) then \( \text{IncludedSet}(Y\cap X, Y\cap T) \) is never trivial. There is no need for a separate proof because the only subspace of the trivial topology is itself.

** lemma ** subspace_includedset:

** assumes **\( T\subseteq X \)

{
** fix **\( M \) ** assume **\( M \in (\text{IncludedSet}(X,T) \text{ restricted to } Y) \)
** then **** obtain **\( A \)** where **A1: \( A:\text{IncludedSet}(X,T) \), \( M = Y\cap A \)** unfolding ** RestrictedTo_def
** then **** have ** \( M \in Pow(X\cap Y) \)** unfolding ** IncludedSet_def
** moreover ** ** from **A1 ** have ** \( Y\cap T\subseteq M \vee M=0 \)** unfolding ** IncludedSet_def
** ultimately **** have ** \( M \in \text{IncludedSet}(Y\cap X, Y\cap T) \)** unfolding ** IncludedSet_def
** } **
** then **** show ** \( \text{IncludedSet}(X,T) \text{ restricted to } Y \subseteq \text{IncludedSet}(Y\cap X, Y\cap T) \)
{
** fix **\( M \) ** let **\( A = M \cup T \) ** assume **A: \( M \in \text{IncludedSet}(Y\cap X, Y\cap T) \)
{
** assume **\( M=0 \)
** then **** have ** \( M\in \text{IncludedSet}(X,T) \text{ restricted to } Y \)** unfolding ** RestrictedTo_def, IncludedSet_def
** } **
** moreover ** {
** assume **AS: \( M\neq 0 \)
** from **A, AS ** have ** A1: \( M\in Pow(Y\cap X) \wedge Y\cap T\subseteq M \)** unfolding ** IncludedSet_def
** then **** have ** \( A\in Pow(X) \)** using ** assms
** moreover ** ** have ** \( T\subseteq A \)
** ultimately **** have ** \( A \in \text{IncludedSet}(X,T) \)** unfolding ** IncludedSet_def
** then **** have ** AT: \( Y \cap A \in \text{IncludedSet}(X,T) \text{ restricted to } Y \)** unfolding ** RestrictedTo_def ** from **A1 ** have ** \( Y \cap A=Y \cap M \)
** also ** ** from **A1 ** have ** \( \ldots =M \)
** finally **** have ** \( Y\cap A = M \)
** with **AT ** have ** \( M \in \text{IncludedSet}(X,T) \text{ restricted to } Y \)
** } **
** ultimately **** have ** \( M \in \text{IncludedSet}(X,T) \text{ restricted to } Y \)
** } **
** thus ** \( \text{IncludedSet}(Y\cap X, Y\cap T) \subseteq \text{IncludedSet}(X,T) \text{ restricted to } Y \)
** qed **

Definition of CoCardinal:
\( \text{CoCardinal}(X,T) \equiv \{F\in Pow(X).\ X-F \prec T\}\cup \{0\} \)

** assumes **\( A\prec Q \)** and **\( B\prec Q \)** and **\( \text{InfCard}(Q) \)

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 **\( InfCard (Q) \)

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

** assumes **\( T\neq 0 \)

Definition of Interior:
\( \text{Interior}(A,T) \equiv \bigcup \{U\in T.\ U \subseteq A\} \)

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

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

** assumes **\( T\neq 0 \), \( A\subseteq X \)

** assumes **\( T\neq 0 \), \( A\subseteq X \)

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

Definition of RestrictedTo:
\( M \text{ restricted to } X \equiv \{X \cap A .\ A \in M\} \)

Definition of ExcludedSet:
\( \text{ExcludedSet}(X,U) \equiv \{F\in Pow(X).\ U \cap F=0\}\cup \{X\} \)

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

** assumes **\( A\subseteq X \)

Definition of IncludedSet:
\( \text{IncludedSet}(X,U) \equiv \{F\in Pow(X).\ U \subseteq F\} \cup \{0\} \)

** assumes **\( T\subseteq X \)

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

** assumes **\( A\subseteq X \), \( T\subseteq X \)