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 {
}
moreover {
}
moreover {
}
ultimately have \( \bigcup M\in T \) using CoCardinal_def
assume B: \( M=0 \)
then have \( \bigcup M\in T \) using CoCardinal_def
assume B: \( M=\{0\} \)
then have \( \bigcup M\in T \) using CoCardinal_def
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
moreover {
}
ultimately show \( thesis \) using IsATopology_def
qed
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
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, assmsIt 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 {
}
qed
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 \)
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 {
}
}
}
ultimately show \( thesis \)
qed
assume as: \( \neg ((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 \( \neg ((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
\(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, assmsThe 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 {
}
}
}
ultimately show \( thesis \)
qed
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
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 {
}
moreover {
}
moreover {
}
ultimately show \( thesis \)
qed
assume AS: \( \neg (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
assume AS: \( \neg (A\prec T) \), \( \neg (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
assume AS: \( A\prec T \), \( \neg (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
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
qed
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) \)
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 {
}
ultimately have \( M\in \text{CoCardinal}(X,T) \text{ restricted to } Y \)
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 \)
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 {
}
}
ultimately have \( \bigcup M\in \text{ExcludedSet}(X,Q) \) using ExcludedSet_def
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 {
}
ultimately have \( Q \cap \bigcup M=0 \vee \bigcup M=X \)
assume \( X\in M \)
with A have \( \bigcup M=X \)
moreover {
}
ultimately show \( thesis \) using IsATopology_def
qed
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
We can use topology0 when discussing excluded set topology.
theorem topology0_excludedset:
shows \( topology0(\text{ExcludedSet}(X,T)) \) using topology0_def, excludedset_is_topologyChoosing 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 {
}
ultimately show \( thesis \) using IsClosed_def, union_excludedset, ExcludedSet_def
qed
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
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
qed
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 \)
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 {
}
}
ultimately show \( thesis \)
qed
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
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 {
}
moreover {
}
ultimately show \( thesis \)
qed
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
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
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 {
}
ultimately have \( M \in \text{ExcludedSet}(X,T) \text{ restricted to } Y \)
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 \)
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 {
}
ultimately show \( thesis \) using IsATopology_def
qed
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
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_topologyChoosing 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 {
}
moreover {
}
ultimately show \( thesis \) using IsClosed_def, union_includedset, assms
qed
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 \)
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
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 {
}
ultimately show \( thesis \)
qed
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
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 {
}
ultimately show \( thesis \)
qed
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
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 {
}
moreover {
}
ultimately show \( thesis \)
qed
assume \( \neg (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
assume \( \neg (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
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 \( \neg (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 {
}
ultimately have \( M \in \text{IncludedSet}(X,T) \text{ restricted to } Y \)
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 \)
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) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8