IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Topology_ZF_examples imports Topology_ZF Cardinal_ZF
begin

This theory deals with some concrete examples of topologies.

CoCardinal Topology

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

shows \( \text{CoCardinal}(X,Q) \text{ is a topology } \)proof
let \( T = \text{CoCardinal}(X,Q) \)
{
fix \( M \)
assume A: \( M\in Pow(T) \)
hence \( M\subseteq T \)
then have \( M\subseteq Pow(X) \) using CoCardinal_def
then have \( \bigcup M\in Pow(X) \)
moreover {
assume B: \( M=0 \)
then have \( \bigcup M\in T \) using CoCardinal_def
} moreover {
assume B: \( M=\{0\} \)
then have \( \bigcup M\in T \) using CoCardinal_def
} moreover {
assume B: \( M \neq 0 \), \( M\neq \{0\} \)
from B obtain \( T \) where C: \( T\in M \) and \( T\neq 0 \)
with A have D: \( X-T \prec (Q) \) using CoCardinal_def
from C have \( X-\bigcup M\subseteq X-T \)
with D have \( X-\bigcup M\prec (Q) \) using subset_imp_lepoll, lesspoll_trans1
} ultimately have \( \bigcup M\in T \) using CoCardinal_def
}
moreover {
fix \( U \) \( and \) \( V \)
assume \( U\in T \) and \( V\in T \)
then have A: \( U=0 \vee (U\in Pow(X) \wedge X-U\prec (Q)) \) and B: \( V=0 \vee (V\in Pow(X) \wedge X-V\prec (Q)) \) using CoCardinal_def
hence D: \( U\in Pow(X) \), \( V\in Pow(X) \)
have C: \( X-(U \cap V)=(X-U)\cup (X-V) \)
with A, B, C have \( U\cap V=0\vee (U\cap V\in Pow(X) \wedge X-(U \cap V)\prec (Q)) \) using less_less_imp_un_less, assms
then have \( U\cap V\in T \) using CoCardinal_def
} ultimately show \( thesis \) using IsATopology_def
qed

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

theorem topology0_CoCardinal:

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

shows \( topology0(\text{CoCardinal}(X,T)) \) using topology0_def, CoCar_is_topology, assms

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

Total set, Closed sets, Interior, Closure and Boundary

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

shows \( \bigcup \text{CoCardinal}(X,T) = X \)proof
have X: \( X-X=0 \)
have \( 0 \preceq 0 \)
with assms have \( 0\prec 1 \), \( 1 \preceq T \) using not_0_is_lepoll_1, lepoll_imp_lesspoll_succ
then have \( 0\prec T \) using lesspoll_trans2
with X have \( (X-X)\prec T \)
then have \( X\in \text{CoCardinal}(X,T) \) using CoCardinal_def
hence \( X\subseteq \bigcup \text{CoCardinal}(X,T) \)
then show \( \bigcup \text{CoCardinal}(X,T)=X \) using CoCardinal_def
qed

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

lemma closed_sets_cocardinal:

assumes \( T\neq 0 \)

shows \( D \text{ is closed in } \text{CoCardinal}(X,T) \longleftrightarrow (D\in Pow(X) \wedge D\prec T) \vee D=X \)proof
{
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 \)

shows \( \text{Interior}(A,\text{CoCardinal}(X,T))= (\text{if }((X-A) \prec T)\text{ then }A\text{ else }0) \)proof
from assms(2) have dif_dif: \( X-(X-A)=A \)
{
assume \( (X-A) \prec T \)
then have \( (X-A)\in Pow(X) \wedge (X-A) \prec T \)
with noC have \( (X-A) \text{ is closed in } \text{CoCardinal}(X,T) \) using closed_sets_cocardinal
with noC have \( X-(X-A)\in \text{CoCardinal}(X,T) \) using IsClosed_def, union_cocardinal
with dif_dif have \( A\in \text{CoCardinal}(X,T) \)
hence \( A\in \{U\in \text{CoCardinal}(X,T).\ U \subseteq A\} \)
hence a1: \( A\subseteq \bigcup \{U\in \text{CoCardinal}(X,T).\ U \subseteq A\} \)
have a2: \( \bigcup \{U\in \text{CoCardinal}(X,T).\ U \subseteq A\}\subseteq A \)
from a1, a2 have \( \text{Interior}(A,\text{CoCardinal}(X,T))=A \) using Interior_def
}
moreover {
assume as: \( ~((X-A) \prec T) \)
{
fix \( U \)
assume \( U \subseteq A \)
hence \( X-A \subseteq X-U \)
then have Q: \( X-A \preceq X-U \) using subset_imp_lepoll
{
assume \( X-U\prec T \)
with Q have \( X-A\prec T \) using lesspoll_trans1
with as have \( False \)
}
hence \( ~((X-U) \prec T) \)
then have \( U\notin \text{CoCardinal}(X,T)\vee U=0 \) using CoCardinal_def
}
hence \( \{U\in \text{CoCardinal}(X,T).\ U \subseteq A\}\subseteq \{0\} \)
then have \( \text{Interior}(A,\text{CoCardinal}(X,T))=0 \) using Interior_def
} ultimately show \( thesis \)
qed

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

shows \( X\in Closed \text{Covers}(A,\text{CoCardinal}(X,T)) \) using ClosedCovers_def using union_cocardinal, closed_sets_cocardinal, assms

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

shows \( \text{Closure}(A,\text{CoCardinal}(X,T))=(\text{if }(A \prec T)\text{ then }A\text{ else }X) \)proof
{
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 \)

shows \( \text{Boundary}(A,\text{CoCardinal}(X,T)) = (\text{if }A\prec T\text{ then }(\text{if } (X-A)\prec T\text{ then }0\text{ else }A)\text{ else }(\text{if } (X-A)\prec T\text{ then }X-A\text{ else }X)) \)proof
from assms(2) have \( X-A \subseteq X \)
{
assume AS: \( A\prec T \), \( X-A \prec T \)
with assms, \( X-A \subseteq X \) have \( \text{Closure}(X-A,\text{CoCardinal}(X,T)) = X-A \) and \( \text{Closure}(A,\text{CoCardinal}(X,T)) = A \) using closure_set_cocardinal
with assms(1) have \( \text{Boundary}(A,\text{CoCardinal}(X,T)) = 0 \) using Boundary_def, union_cocardinal
}
moreover {
assume AS: \( ~(A\prec T) \), \( X-A \prec T \)
with assms, \( X-A \subseteq X \) have \( \text{Closure}(X-A,\text{CoCardinal}(X,T)) = X-A \) and \( \text{Closure}(A,\text{CoCardinal}(X,T)) = X \) using closure_set_cocardinal
with assms(1) have \( \text{Boundary}(A,\text{CoCardinal}(X,T))=X-A \) using Boundary_def, union_cocardinal
} moreover {
assume AS: \( ~(A\prec T) \), \( ~(X-A \prec T) \)
with assms, \( X-A \subseteq X \) have \( \text{Closure}(X-A,\text{CoCardinal}(X,T))=X \) and \( \text{Closure}(A,\text{CoCardinal}(X,T))=X \) using closure_set_cocardinal
with assms(1) have \( \text{Boundary}(A,\text{CoCardinal}(X,T))=X \) using Boundary_def, union_cocardinal
} moreover {
assume AS: \( A\prec T \), \( ~(X-A\prec T) \)
with assms, \( X-A \subseteq X \) have \( \text{Closure}(X-A,\text{CoCardinal}(X,T))=X \) and \( \text{Closure}(A,\text{CoCardinal}(X,T)) = A \) using closure_set_cocardinal
with assms have \( \text{Boundary}(A,\text{CoCardinal}(X,T))=A \) using Boundary_def, union_cocardinal
} ultimately show \( thesis \)
qed

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

shows \( \text{CoCardinal}(X,T) = Pow(X) \)proof
{
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:

shows \( \text{CoCardinal}(X,1) = \{0,X\} \)proof
{
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:

shows \( \text{CoCardinal}(X,T) \text{ restricted to } Y = \text{CoCardinal}(Y\cap X,T) \)proof
{
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

Excluded Set Topology

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:

shows \( \text{ExcludedSet}(X,Q) \text{ is a topology } \)proof
{
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:

shows \( topology0(\text{ExcludedSet}(X,T)) \) using topology0_def, excludedset_is_topology

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

definition

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

Total set, closed sets, interior, closure and boundary

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:

shows \( \bigcup \text{ExcludedSet}(X,T) = X \)proof
have \( X \in \text{ExcludedSet}(X,T) \) using ExcludedSet_def
then show \( thesis \) using ExcludedSet_def
qed

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

lemma closed_sets_excludedset:

shows \( D \text{ is closed in }\text{ExcludedSet}(X,T) \longleftrightarrow (D\in Pow(X) \wedge (X \cap T) \subseteq D) \vee D=0 \)proof
{
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 \)

shows \( \text{Interior}(A,\text{ExcludedSet}(X,T)) = (\text{if }A=X\text{ then }X\text{ else }A-T) \)proof
{
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 \)

shows \( \text{Closure}(A,\text{ExcludedSet}(X,T))=(\text{if }A=0\text{ then }0\text{ else }A \cup (X\cap T)) \)proof
have \( 0\in Closed \text{Covers}(0,\text{ExcludedSet}(X,T)) \) using ClosedCovers_def, closed_sets_excludedset
then have \( \text{Closure}(0,\text{ExcludedSet}(X,T))\subseteq 0 \) using Closure_def
hence \( \text{Closure}(0,\text{ExcludedSet}(X,T))=0 \)
moreover {
assume A: \( A\neq 0 \)
with assms have \( (A\cup (X\cap T)) \text{ is closed in }\text{ExcludedSet}(X,T) \) using closed_sets_excludedset
then have \( (A \cup (X\cap T))\in \{D \in Pow(X).\ D \text{ is closed in }\text{ExcludedSet}(X,T) \wedge A\subseteq D\} \) using assms
then have \( (A \cup (X\cap T))\in Closed \text{Covers}(A,\text{ExcludedSet}(X,T)) \) unfolding ClosedCovers_def using union_excludedset
then have l1: \( \bigcap Closed \text{Covers}(A,\text{ExcludedSet}(X,T)) \subseteq (A \cup (X\cap T)) \)
{
fix \( U \)
assume \( U\in Closed \text{Covers}(A,\text{ExcludedSet}(X,T)) \)
then have \( U\text{ is closed in }\text{ExcludedSet}(X,T) \) and \( A\subseteq U \) using ClosedCovers_def, union_excludedset
then have \( U=0\vee (X\cap T)\subseteq U \) and \( A\subseteq U \) using closed_sets_excludedset
with A have \( (X\cap T)\subseteq U \), \( A\subseteq U \)
hence \( (X\cap T)\cup A\subseteq U \)
}
with assms have \( (A \cup (X\cap T)) \subseteq \bigcap Closed \text{Covers}(A,\text{ExcludedSet}(X,T)) \) using Top_3_L3, topology0_excludedset, union_excludedset
with l1 have \( \bigcap Closed \text{Covers}(A,\text{ExcludedSet}(X,T)) = (A\cup (X\cap T)) \)
then have \( \text{Closure}(A, \text{ExcludedSet}(X,T)) = A\cup (X\cap T) \) using Closure_def
} ultimately show \( thesis \)
qed

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

shows \( \text{Boundary}(A,\text{ExcludedSet}(X,T)) = (\text{if }A=0\vee A=X\text{ then }0\text{ else }X\cap T) \)proof
{
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

Special cases and subspaces

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:

shows \( \text{ExcludedSet}(X,T) = \text{ExcludedSet}(X,(X\cap T)) \)proof
show \( \text{ExcludedSet}(X,T) \subseteq \text{ExcludedSet}(X, X\cap T) \) and \( \text{ExcludedSet}(X, X\cap T) \subseteq \text{ExcludedSet}(X,T) \) unfolding ExcludedSet_def
qed

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

lemma empty_excludedset:

assumes \( T\cap X=0 \)

shows \( \text{ExcludedSet}(X,T) = Pow(X) \)proof
from assms show \( \text{ExcludedSet}(X,T) \subseteq Pow(X) \) using smaller_excludedset, ExcludedSet_def
from assms show \( Pow(X) \subseteq \text{ExcludedSet}(X,T) \) unfolding ExcludedSet_def
qed

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

lemma subspace_excludedset:

shows \( \text{ExcludedSet}(X,T) \text{ restricted to } Y = \text{ExcludedSet}(Y \cap X, T) \)proof
{
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

Included Set Topology

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:

shows \( \text{IncludedSet}(X,Q) \text{ is a topology } \)proof
{
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:

shows \( topology0(\text{IncludedSet}(X,T)) \) using topology0_def, includedset_is_topology

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

Basic topological notions in included set topology

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

shows \( \bigcup \text{IncludedSet}(X,T) = X \)proof
from assms have \( X \in \text{IncludedSet}(X,T) \) using IncludedSet_def
then show \( \bigcup \text{IncludedSet}(X,T) = X \) using IncludedSet_def
qed

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

lemma closed_sets_includedset:

assumes \( T\subseteq X \)

shows \( D \text{ is closed in } \text{IncludedSet}(X,T) \longleftrightarrow (D\in Pow(X) \wedge (D \cap T)=0)\vee D=X \)proof
have \( X-X=0 \)
then have \( X-X\in \text{IncludedSet}(X,T) \) using IncludedSet_def
moreover {
assume A: \( D \subseteq X \), \( X - D \in \text{IncludedSet}(X,T) \), \( D \neq X \)
from A(2) have \( T\subseteq (X-D)\vee X-D=0 \) using IncludedSet_def
with A(1) have \( T\subseteq (X-D)\vee D=X \)
with A(3) have \( T\subseteq (X-D) \)
hence \( D\cap T=0 \)
} moreover {
assume A: \( D\cap T=0 \), \( D\subseteq X \)
from A(1), assms have \( T\subseteq (X-D) \)
then have \( X-D\in \text{IncludedSet}(X,T) \) using IncludedSet_def
} ultimately show \( thesis \) using IsClosed_def, union_includedset, assms
qed

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

shows \( \text{Interior}(A,\text{IncludedSet}(X,T))= (\text{if }T\subseteq A\text{ then }A\text{ else }0) \)proof
{
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 \)

shows \( \text{Closure}(A,\text{IncludedSet}(X,T)) = (\text{if }T\cap A=0\text{ then }A\text{ else }X) \)proof
{
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 \)

shows \( \text{Boundary}(A,\text{IncludedSet}(X,T))=(\text{if }T\subseteq A\text{ then }X-A\text{ else }(\text{if }T\cap A=0\text{ then }A\text{ else }X)) \)proof
from \( A\subseteq X \) have \( X-A \subseteq X \)
{
assume \( T\subseteq A \)
with assms(2,3) have \( T\cap A\neq 0 \) and \( T\cap (X-A)=0 \)
with assms(1,2), \( X-A \subseteq X \) have \( \text{Closure}(A,\text{IncludedSet}(X,T)) = X \) and \( \text{Closure}(X-A,\text{IncludedSet}(X,T)) = (X-A) \) using closure_set_includedset
with assms(2) have \( \text{Boundary}(A,\text{IncludedSet}(X,T)) = X-A \) using Boundary_def, union_includedset
}
moreover {
assume \( ~(T\subseteq A) \) and \( T\cap A=0 \)
with assms(2) have \( T\cap (X-A)\neq 0 \)
with assms(1,2), \( T\cap A=0 \), \( X-A \subseteq X \) have \( \text{Closure}(A,\text{IncludedSet}(X,T)) = A \) and \( \text{Closure}(X-A,\text{IncludedSet}(X,T)) = X \) using closure_set_includedset
with assms(1,2) have \( \text{Boundary}(A,\text{IncludedSet}(X,T))=A \) using Boundary_def, union_includedset
} moreover {
assume \( ~(T\subseteq A) \) and \( T\cap A \neq 0 \)
with assms(1,2) have \( T\cap (X-A) \neq 0 \)
with assms(1,2), \( T\cap A\neq 0 \), \( X-A \subseteq X \) have \( \text{Closure}(A,\text{IncludedSet}(X,T)) = X \) and \( \text{Closure}(X-A,\text{IncludedSet}(X,T)) = X \) using closure_set_includedset
with assms(2) have \( \text{Boundary}(A,\text{IncludedSet}(X,T)) = X \) using Boundary_def, union_includedset
} ultimately show \( thesis \)
qed

Special cases and subspaces

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:

shows \( \text{IncludedSet}(X,0) = Pow(X) \)proof
show \( \text{IncludedSet}(X,0) \subseteq Pow(X) \) and \( Pow(X) \subseteq \text{IncludedSet}(X,0) \) unfolding IncludedSet_def
qed

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

lemma empty_includedset:

assumes \( ~(T\subseteq X) \)

shows \( \text{IncludedSet}(X,T) = \{0\} \)proof
from assms show \( \text{IncludedSet}(X,T) \subseteq \{0\} \) and \( \{0\} \subseteq \text{IncludedSet}(X,T) \) unfolding IncludedSet_def
qed

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

shows \( \text{IncludedSet}(X,T) \text{ restricted to } Y = \text{IncludedSet}(Y\cap X,Y\cap T) \)proof
{
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
end
Definition of CoCardinal: \( \text{CoCardinal}(X,T) \equiv \{F\in Pow(X).\ X-F \prec T\}\cup \{0\} \)
lemma less_less_imp_un_less:

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

shows \( A \cup B\prec 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) \)
lemma CoCar_is_topology:

assumes \( InfCard (Q) \)

shows \( \text{CoCardinal}(X,Q) \text{ is a topology } \)
Definition of IsClosed: \( D \text{ is closed in } T \equiv (D \subseteq \bigcup T \wedge \bigcup T - D \in T) \)
lemma union_cocardinal:

assumes \( T\neq 0 \)

shows \( \bigcup \text{CoCardinal}(X,T) = X \)
lemma closed_sets_cocardinal:

assumes \( T\neq 0 \)

shows \( D \text{ is closed in } \text{CoCardinal}(X,T) \longleftrightarrow (D\in Pow(X) \wedge D\prec T) \vee D=X \)
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) \)
lemma X_closedcov_cocardinal:

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

shows \( X\in Closed \text{Covers}(A,\text{CoCardinal}(X,T)) \)
lemma closure_set_cocardinal:

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

shows \( \text{Closure}(A,\text{CoCardinal}(X,T))=(\text{if }(A \prec T)\text{ then }A\text{ else }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\} \)
theorem excludedset_is_topology: shows \( \text{ExcludedSet}(X,Q) \text{ is a topology } \)
lemma union_excludedset: shows \( \bigcup \text{ExcludedSet}(X,T) = X \)
lemma (in topology0) Top_2_L3: shows \( U\in T \longleftrightarrow int(U) = U \)
theorem topology0_excludedset: shows \( topology0(\text{ExcludedSet}(X,T)) \)
lemma closed_sets_excludedset: shows \( D \text{ is closed in }\text{ExcludedSet}(X,T) \longleftrightarrow (D\in Pow(X) \wedge (X \cap T) \subseteq D) \vee D=0 \)
lemma (in topology0) Top_3_L3:

assumes \( A \subseteq \bigcup T \)

shows \( Closed \text{Covers}(A,T) \neq 0 \)
lemma closure_set_excludedset:

assumes \( A\subseteq X \)

shows \( \text{Closure}(A,\text{ExcludedSet}(X,T))=(\text{if }A=0\text{ then }0\text{ else }A \cup (X\cap T)) \)
lemma smaller_excludedset: shows \( \text{ExcludedSet}(X,T) = \text{ExcludedSet}(X,(X\cap T)) \)
Definition of IncludedSet: \( \text{IncludedSet}(X,U) \equiv \{F\in Pow(X).\ U \subseteq F\} \cup \{0\} \)
theorem includedset_is_topology: shows \( \text{IncludedSet}(X,Q) \text{ is a topology } \)
lemma union_includedset:

assumes \( T\subseteq X \)

shows \( \bigcup \text{IncludedSet}(X,T) = X \)
lemma (in topology0) Top_2_L2: shows \( int(A) \in T \)
theorem topology0_includedset: shows \( topology0(\text{IncludedSet}(X,T)) \)
lemma (in topology0) Top_2_L1: shows \( int(A) \subseteq A \)
lemma closed_sets_includedset:

assumes \( T\subseteq X \)

shows \( D \text{ is closed in } \text{IncludedSet}(X,T) \longleftrightarrow (D\in Pow(X) \wedge (D \cap T)=0)\vee D=X \)
lemma (in topology0) Top_3_L8:

assumes \( A \subseteq \bigcup T \)

shows \( A \text{ is closed in } T \longleftrightarrow cl(A) = A \)
lemma closure_set_includedset:

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

shows \( \text{Closure}(A,\text{IncludedSet}(X,T)) = (\text{if }T\cap A=0\text{ then }A\text{ else }X) \)