(*

This file is a part of IsarMathLib -

a library of formalized mathematics written for Isabelle/Isar.

Copyright (C) 2012 Daniel de la Concepcion

This program is free software; Redistribution and use in source and binary forms,

with or without modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice,

this list of conditions and the following disclaimer.

2. Redistributions in binary form must reproduce the above copyright notice,

this list of conditions and the following disclaimer in the documentation and/or

other materials provided with the distribution.

3. The name of the author may not be used to endorse or promote products

derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED

WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF

MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.

IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,

SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,

PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;

OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,

WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR

OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,

EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)

header{*\isaheader{Topology\_ZF\_examples.thy}*}

theory Topology_ZF_examples imports Topology_ZF Cardinal_ZF

begin

text{*

This theory deals with some concrete examples of topologies.

*}

section{*CoCardinal Topology of a set $X$*}

subsection{*CoCardinal topology is a topology.*}

text{*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 Cocardinal ("CoCardinal _ _" 50) where

"CoCardinal X T ≡ {F∈Pow(X). X-F \<prec> T}∪ {0}"

text{*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 @{text "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 @{prop "Q=1"} which translates

in the indiscrete topology.*}

lemma CoCar_is_topology:

assumes "InfCard (Q)"

shows "(CoCardinal X Q) {is a topology}"

proof-

let ?T="(CoCardinal X Q)"

{

fix M

assume A:"M∈Pow(?T)"

hence "M⊆?T" by auto

then have "M⊆Pow(X)" using Cocardinal_def by auto

then have "\<Union>M∈Pow(X)" by auto

moreover

{

assume B:"M=0"

then have "\<Union>M∈?T" using Cocardinal_def by auto

}

moreover

{

assume B:"M={0}"

then have "\<Union>M∈?T" using Cocardinal_def by auto

}

moreover

{

assume B:"M ≠0" "M≠{0}"

from B obtain T where C:"T∈M" and "T≠0" by auto

with A have D:"X-T \<prec> (Q)" using Cocardinal_def by auto

from C have "X-\<Union>M⊆X-T" by blast

with D have "X-\<Union>M\<prec> (Q)" using subset_imp_lepoll lesspoll_trans1 by blast

}

ultimately have "\<Union>M∈?T" using Cocardinal_def by auto

}

moreover

{

fix U and V

assume "U∈?T" and "V∈?T"

hence A:"U=0 ∨ (U∈Pow(X) ∧ X-U\<prec> (Q))" and

B:"V=0 ∨ (V∈Pow(X) ∧ X-V\<prec> (Q))" using Cocardinal_def by auto

hence D:"U∈Pow(X)""V∈Pow(X)" by auto

have C:"X-(U ∩ V)=(X-U)∪(X-V)" by fast

with A B C have "U∩V=0∨(U∩V∈Pow(X) ∧ X-(U ∩ V)\<prec> (Q))" using less_less_imp_un_less assms

by auto

hence "U∩V∈?T" using Cocardinal_def by auto

}

ultimately show ?thesis using IsATopology_def by auto

qed

theorem topology0_CoCardinal:

assumes "InfCard(T)"

shows "topology0(CoCardinal X T)"

using topology0_def CoCar_is_topology assms by auto

text{*It can also be proven that, if @{text "CoCardinal X T"} is a topology,

@{prop "X≠0"}, @{prop "Card(T)"} and @{prop "T≠0"}; then @{text "T"} is an infinite cardinal, @{prop "X\<prec>T"}

or @{text "T=1"}.

It follows from the fact that the union of two closed sets is closed. *}

text{*Choosing the appropriate cardinals, the cofinite and the cocountable topologies

are obtained.*}

text{*The cofinite topology is a very special topology because is extremely

related to the separation axiom $T_1$. It also appears naturally

in algebraic geometry.*}

definition

Cofinite ("CoFinite _" 90) where

"CoFinite X ≡ CoCardinal X nat"

definition

Cocountable ("CoCountable _" 90) where

"CoCountable X ≡ CoCardinal X csucc(nat)"

subsection{*Total set, Closed sets, Interior, Closure and Boundary*}

text{*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.*}

text{*The topology is defined in the set $X$*}

lemma union_cocardinal:

assumes "T≠0"

shows "\<Union> (CoCardinal X T)=X"

proof-

have X:"X-X=0" by auto

have "0 \<lesssim> 0" by auto

with assms have "0\<prec>1""1 \<lesssim>T" using not_0_is_lepoll_1 lepoll_imp_lesspoll_succ by auto

then have "0\<prec>T" using lesspoll_trans2 by auto

with X have "(X-X)\<prec>T" by auto

then have "X∈(CoCardinal X T)" using Cocardinal_def by auto

hence "X⊆\<Union> (CoCardinal X T)" by blast

then show "\<Union> (CoCardinal X T)=X" using Cocardinal_def by auto

qed

text{*The closed sets are the small subsets of $X$ and $X$ itself.*}

lemma closed_sets_cocardinal:

assumes "T≠0"

shows "D {is closed in} (CoCardinal X T) <-> (D∈Pow(X) & D\<prec>T)∨ D=X"

proof-

{

assume A:"D ⊆ X" "X - D ∈ (CoCardinal X T) "" D ≠ X"

from A(1,3) have "X-(X-D)=D" "X-D≠0" by (safe,blast+)

with A(2) have "D\<prec>T" using Cocardinal_def by simp

}

with assms have "D {is closed in} (CoCardinal X T) --> (D∈Pow(X) & D\<prec>T)∨ D=X" using IsClosed_def

union_cocardinal by auto

moreover

{

assume A:"D \<prec> T""D ⊆ X"

from A(2) have "X-(X-D)=D" by blast

with A(1) have "X-(X-D)\<prec> T" by auto

then have "X-D∈ (CoCardinal X T)" using Cocardinal_def by auto

}

with assms have "(D∈Pow(X) & D\<prec>T)--> D {is closed in} (CoCardinal X T)" using union_cocardinal

IsClosed_def by auto

moreover

have "X-X=0" by auto

then have "X-X∈ (CoCardinal X T)"using Cocardinal_def by auto

with assms have "X{is closed in} (CoCardinal X T)" using union_cocardinal

IsClosed_def by auto

ultimately show ?thesis by auto

qed

text{*The interior of a set is itself if it is open or @{text "0"} if

it isn't open.*}

lemma interior_set_cocardinal:

assumes noC: "T≠0" and "A⊆X"

shows "Interior(A,(CoCardinal X T))= (if ((X-A) \<prec> T) then A else 0)"

proof-

from assms(2) have dif_dif:"X-(X-A)=A" by blast

{

assume "(X-A) \<prec> T"

then have "(X-A)∈Pow(X) &(X-A) \<prec> T" by auto

with noC have "(X-A) {is closed in} (CoCardinal X T)" using closed_sets_cocardinal

by auto

with noC have "X-(X-A)∈(CoCardinal X T)" using IsClosed_def union_cocardinal

by auto

with dif_dif have "A∈(CoCardinal X T)" by auto

hence "A∈{U∈(CoCardinal X T). U ⊆ A}" by auto

hence a1:"A⊆\<Union>{U∈(CoCardinal X T). U ⊆ A}" by auto

have a2:"\<Union>{U∈(CoCardinal X T). U ⊆ A}⊆A" by blast

from a1 a2 have "Interior(A,(CoCardinal X T))=A" using Interior_def by auto}

moreover

{

assume as:"~((X-A) \<prec> T)"

{

fix U

assume "U ⊆A"

hence "X-A ⊆ X-U" by blast

then have Q:"X-A \<lesssim> X-U" using subset_imp_lepoll by auto

{

assume "X-U\<prec> T"

with Q have "X-A\<prec> T" using lesspoll_trans1 by auto

with as have "False" by auto

}

hence "~((X-U) \<prec> T)" by auto

then have "U∉(CoCardinal X T)∨U=0" using Cocardinal_def by auto

}

hence "{U∈(CoCardinal X T). U ⊆ A}⊆{0}" by blast

then have "Interior(A,(CoCardinal X T))=0" using Interior_def by auto

}

ultimately show ?thesis by auto

qed

text{*$X$ is a closed set that contains $A$.

This lemma is necessary because we cannot

use the lemmas proven in the @{text "topology0"} context since

@{prop "T≠0"} is too weak for

@{text "CoCardinal X T"} to be a topology.*}

lemma X_closedcov_cocardinal:

assumes "T≠0""A⊆X"

shows "X∈ClosedCovers(A,(CoCardinal X T))" using ClosedCovers_def

using union_cocardinal closed_sets_cocardinal assms by auto

text{*The closure of a set is itself if it is closed or @{text "X"} if

it isn't closed.*}

lemma closure_set_cocardinal:

assumes "T≠0""A⊆X"

shows "Closure(A,(CoCardinal X T))=(if (A \<prec> T) then A else X)"

proof-

{

assume "A \<prec> T"

with assms have "A {is closed in} (CoCardinal X T)" using closed_sets_cocardinal by auto

with assms(2) have "A∈ {D ∈ Pow(X). D {is closed in} (CoCardinal X T) ∧ A⊆D}" by auto

with assms(1) have S:"A∈ClosedCovers(A,(CoCardinal X T))" using ClosedCovers_def

using union_cocardinal by auto

hence l1:"\<Inter>ClosedCovers(A,(CoCardinal X T))⊆A" by blast

from S have l2:"A⊆\<Inter>ClosedCovers(A,(CoCardinal X T))"

using ClosedCovers_def[where T="CoCardinal X T" and A="A"] by auto

from l1 l2 have "Closure(A,(CoCardinal X T))=A" using Closure_def

by auto

}

moreover

{

assume as:"¬ A \<prec> T"

{

fix U

assume "A⊆U"

then have Q:"A \<lesssim> U" using subset_imp_lepoll by auto

{

assume "U\<prec> T"

with Q have "A\<prec> T" using lesspoll_trans1 by auto

with as have "False" by auto

}

hence "¬ U \<prec> T" by auto

with assms(1) have "¬(U {is closed in} (CoCardinal X T)) ∨ U=X" using closed_sets_cocardinal

by auto

}

with assms(1) have "∀U∈Pow(X). U{is closed in}(CoCardinal X T)∧A⊆U-->U=X"

by auto

with assms(1) have "ClosedCovers(A,(CoCardinal X T))⊆{X}"

using union_cocardinal using ClosedCovers_def by auto

with assms have "ClosedCovers(A,(CoCardinal X T))={X}" using X_closedcov_cocardinal

by auto

then have " Closure(A, CoCardinal X T) = X " using Closure_def by auto

}

ultimately show ?thesis by auto

qed

text{*The boundary of a set is @{text "0"} if $A$ and $X-A$ are closed,

@{text "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≠0""A ⊆X"

shows "Boundary(A,(CoCardinal X T))=(if A\<prec> T then (if (X-A)\<prec> T then 0 else A) else (if (X-A)\<prec> T then X-A else X))"

proof-

{

assume AS:"A\<prec> T""X-A\<prec> T"

from AS(2) assms have "Closure(X-A,(CoCardinal X T))=X-A" using closure_set_cocardinal[where A="X-A" and T="T" and X="X"] by auto

moreover

from AS(1) assms have "Closure(A,(CoCardinal X T))=A"

using closure_set_cocardinal by auto

with calculation assms(1) have "Boundary(A,(CoCardinal X T))=0"using Boundary_def using

union_cocardinal by auto

}

moreover

{

assume AS:"~(A\<prec> T)""X-A\<prec> T"

from AS(2) assms have "Closure(X-A,(CoCardinal X T))=X-A" using closure_set_cocardinal[where A="X-A" and T="T" and X="X"] by auto

moreover

from AS(1) assms have "Closure(A,(CoCardinal X T))=X"

using closure_set_cocardinal by auto

with calculation assms(1) have "Boundary(A,(CoCardinal X T))=X-A" using Boundary_def

union_cocardinal by auto

}

moreover

{

assume AS:"~(A\<prec> T)""~(X-A\<prec> T)"

from AS(2) assms have "Closure(X-A,(CoCardinal X T))=X" using closure_set_cocardinal[where A="X-A" and T="T" and X="X"] by auto

moreover

from AS(1) assms have "Closure(A,(CoCardinal X T))=X"

using closure_set_cocardinal by auto

with calculation assms(1) have "Boundary(A,(CoCardinal X T))=X"using Boundary_def

union_cocardinal by auto

}

moreover

{

assume AS:"A\<prec> T""~(X-A\<prec> T)"

from AS(2) assms have "Closure(X-A,(CoCardinal X T))=X" using closure_set_cocardinal[where A="X-A" and T="T" and X="X"] by auto

moreover

from AS(1) assms have "Closure(A,(CoCardinal X T))=A"

using closure_set_cocardinal by auto

with calculation assms have "Boundary(A,(CoCardinal X T))=A" using Boundary_def

union_cocardinal by auto

}

ultimately show ?thesis by auto

qed

subsection{*Special cases and subspaces*}

text{*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 "(CoCardinal X T)=(Pow (X))"

proof

{

fix U

assume "U∈(CoCardinal X T)"

then have "U∈Pow (X)" using Cocardinal_def by auto

}

then show "(CoCardinal X T)⊆(Pow (X))" by auto

{

fix U

assume A:"U∈Pow(X)"

then have "X-U ⊆ X" by auto

then have "X-U \<lesssim>X" using subset_imp_lepoll by auto

then have "X-U\<prec> T" using lesspoll_trans1 assms by auto

with A have "U∈(CoCardinal X T)" using Cocardinal_def

by auto

}

then show "Pow(X)⊆(CoCardinal X T)" by auto

qed

text{*If the cardinal is taken as @{prop "T=1"} then the topology

is indiscrete.*}

lemma indiscrete_cocardinal:

shows "(CoCardinal X 1)={0,X}"

proof

{

fix Q

assume "Q∈(CoCardinal X 1)"

then have "Q∈Pow(X)""Q=0∨X-Q\<prec>1" using Cocardinal_def by auto

then have "Q∈Pow(X)""Q=0∨X-Q=0" using lesspoll_succ_iff lepoll_0_iff by (safe,blast)

then have "Q=0∨Q=X" by blast

}

then show "(CoCardinal X 1) ⊆ {0, X}" by auto

have "0∈(CoCardinal X 1)" using Cocardinal_def by auto

moreover

have "0\<prec>1""X-X=0" using lesspoll_succ_iff by auto

then have "X∈(CoCardinal X 1)" using Cocardinal_def by auto

ultimately show "{0, X} ⊆ (CoCardinal X 1) " by auto

qed

text{*The topological subspaces of the @{text "CoCardinal X T"} topology

are also CoCardinal topologies.*}

lemma subspace_cocardinal:

shows "(CoCardinal X T) {restricted to} Y=(CoCardinal (Y ∩ X) T)"

proof

{

fix M

assume "M∈((CoCardinal X T) {restricted to} Y)"

then obtain A where A1:"A:(CoCardinal X T)" "M=Y ∩ A" using RestrictedTo_def by auto

then have "M∈Pow(X ∩ Y)" using Cocardinal_def by auto

moreover

from A1 have "(Y ∩ X)-M=(Y ∩ X)-A" using Cocardinal_def by auto

have "(Y ∩ X)-A ⊆ X-A" by blast

with `(Y ∩ X)-M=(Y ∩ X)-A` have "(Y ∩ X)-M⊆ X-A" by auto

then have "(Y ∩ X)-M \<lesssim> X-A" using subset_imp_lepoll by auto

with A1 have "(Y ∩ X)-M \<prec> T ∨ M=0" using lesspoll_trans1 using Cocardinal_def

by (cases "A=0",simp,cases "Y ∩ A=0",simp+)

ultimately have "M∈(CoCardinal (Y ∩ X) T)" using Cocardinal_def

by auto

}

then show "(CoCardinal X T) {restricted to} Y ⊆(CoCardinal (Y ∩ X) T)" by auto

{

fix M

let ?A="M ∪ (X-Y)"

assume A:"M∈(CoCardinal (Y ∩ X) T)"

{

assume "M=0"

hence "M=0 ∩ Y" by auto

then have "M∈(CoCardinal X T) {restricted to} Y" using RestrictedTo_def

Cocardinal_def by auto

}

moreover

{

assume AS:"M≠0"

from A AS have A1:"(M∈Pow(Y ∩ X) ∧ (Y ∩ X)-M\<prec> T)" using Cocardinal_def by auto

hence "?A∈Pow(X)" by blast

moreover

have "X-?A=(Y ∩ X)-M" by blast

with A1 have "X-?A\<prec> T" by auto

ultimately have "?A∈(CoCardinal X T)" using Cocardinal_def by auto

then have AT:"Y ∩ ?A∈(CoCardinal X T) {restricted to} Y" using RestrictedTo_def

by auto

have "Y ∩ ?A=Y ∩ M" by blast

also with A1 have "…=M" by auto

finally have "Y ∩ ?A=M".

with AT have "M∈(CoCardinal X T) {restricted to} Y"

by auto

}

ultimately have "M∈(CoCardinal X T) {restricted to} Y" by auto

}

then show "(CoCardinal (Y ∩ X) T) ⊆ (CoCardinal X T) {restricted to} Y" by auto

qed

section{*Excluded Set Topology*}

text{*In this seccion, we consider all the subsets of a set

which have empty intersection with a fixed set.*}

subsection{*Excluded set topology is a topology.*}

definition

ExcludedSet ("ExcludedSet _ _" 50) where

"ExcludedSet X U ≡ {F∈Pow(X). U ∩ F=0}∪ {X}"

text{*For any set; we prove that

@{text "ExcludedSet X Q"} forms a topology.*}

theorem excludedset_is_topology:

shows "(ExcludedSet X Q) {is a topology}"

proof-

{

fix M

assume "M∈Pow(ExcludedSet X Q)"

then have A:"M⊆{F∈Pow(X). Q ∩ F=0}∪ {X}" using ExcludedSet_def by auto

hence "\<Union>M∈Pow(X)" by auto

moreover

{

have B:"Q ∩\<Union>M=\<Union>{Q ∩T. T∈M}" by auto

{

assume "X∉M"

with A have "M⊆{F∈Pow(X). Q ∩ F=0}" by auto

with B have "Q ∩ \<Union>M=0" by auto

}

moreover

{

assume "X∈M"

with A have "\<Union>M=X" by auto

}

ultimately have "Q ∩ \<Union>M=0 ∨ \<Union>M=X" by auto

}

ultimately have "\<Union>M∈(ExcludedSet X Q)" using ExcludedSet_def by auto

}

moreover

{

fix U V

assume "U∈(ExcludedSet X Q)" "V∈(ExcludedSet X Q)"

then have "U∈Pow(X)""V∈Pow(X)""U=X∨ U ∩ Q=0""V=X∨ V ∩ Q=0" using ExcludedSet_def by auto

hence "U∈Pow(X)""V∈Pow(X)""(U ∩ V)=X ∨ Q∩(U ∩ V)=0" by auto

then have "(U ∩ V)∈(ExcludedSet X Q)" using ExcludedSet_def by auto

}

ultimately show ?thesis using IsATopology_def by auto

qed

theorem topology0_excludedset:

shows "topology0(ExcludedSet X T)"

using topology0_def excludedset_is_topology by auto

text{*Choosing a singleton set, it is considered a point excluded

topology.*}

definition

ExcludedPoint ("ExcludedPoint _ _" 90) where

"ExcludedPoint X p≡ ExcludedSet X {p}"

subsection{*Total set, Closed sets, Interior, Closure and Boundary*}

text{*The topology is defined in the set $X$*}

lemma union_excludedset:

shows "\<Union> (ExcludedSet X T)=X"

proof-

have "X∈(ExcludedSet X T)" using ExcludedSet_def by auto

then show ?thesis using ExcludedSet_def by auto

qed

text{*The closed sets are those which contain the set @{text "(X ∩ T)"} and @{text "0"}.*}

lemma closed_sets_excludedset:

shows "D {is closed in} (ExcludedSet X T) <-> (D∈Pow(X) & (X ∩ T) ⊆D)∨ D=0"

proof-

{

fix x

assume A:"D ⊆ X" "X - D ∈ (ExcludedSet X T) "" D ≠ 0""x:T""x:X"

from A(1) have B:"X-(X-D)=D" by auto

from A(2) have "T∩(X-D)=0∨ X-D=X" using ExcludedSet_def by auto

hence "T∩(X-D)=0∨ X-(X-D)=X-X" by auto

with B have "T∩(X-D)=0∨ D=X-X" by auto

hence "T∩(X-D)=0∨ D=0" by auto

with A(3) have "T∩(X-D)=0" by auto

with A(4) have "x∉X-D" by auto

with A(5) have "x∈D" by auto

}

moreover

{

assume A:"X∩T⊆D""D⊆X"

from A(1) have "X-D⊆X-(X∩T)" by auto

also have "…=X-T" by auto

finally have "T∩(X-D)=0" by auto

moreover

have "X-D∈Pow(X)" by auto

ultimately have "X-D∈(ExcludedSet X T)" using ExcludedSet_def by auto

}

ultimately show ?thesis using IsClosed_def union_excludedset

ExcludedSet_def by auto

qed

text{*The interior of a set is itself if it is @{text "X"} or

the difference with the set @{text"T"}*}

lemma interior_set_excludedset:

assumes "A⊆X"

shows "Interior(A,(ExcludedSet X T))= (if A=X then X else A-T)"

proof-

{

assume A:"A≠X"

from assms have "A-T∈(ExcludedSet X T)" using ExcludedSet_def by auto

then have "A-T⊆Interior(A,(ExcludedSet X T))"

using Interior_def by auto

moreover

{

fix U

assume "U∈(ExcludedSet X T)""U⊆A"

then have "T∩U=0 ∨ U=X""U⊆A" using ExcludedSet_def by auto

with A assms have "T∩U=0""U⊆A" by auto

then have "U-T=U""U-T⊆A-T" by (safe,blast+)

then have "U⊆A-T" by auto

}

then have "Interior(A,(ExcludedSet X T))⊆A-T" using Interior_def by auto

ultimately have "Interior(A,(ExcludedSet X T))=A-T" by auto

}

moreover

have "X∈(ExcludedSet X T)" using ExcludedSet_def

union_excludedset by auto

then have "Interior(X,(ExcludedSet X T))=X" using topology0.Top_2_L3

topology0_excludedset by auto

ultimately show ?thesis by auto

qed

text{*The closure of a set is itself if it is @{text "0"} or

the union with @{text "T"}.*}

lemma closure_set_excludedset:

assumes "A⊆X"

shows "Closure(A,(ExcludedSet X T))=(if A=0 then 0 else A ∪(X∩ T))"

proof-

have "0∈ClosedCovers(0,(ExcludedSet X T))" using ClosedCovers_def

closed_sets_excludedset by auto

then have "Closure(0,(ExcludedSet X T))⊆0" using Closure_def by auto

hence "Closure(0,(ExcludedSet X T))=0" by blast

moreover

{

assume A:"A≠0"

then have "(A ∪(X∩ T)) {is closed in} (ExcludedSet X T)"

using closed_sets_excludedset[of "A ∪(X∩ T)"] assms A

by blast

then have "(A ∪(X∩ T))∈ {D ∈ Pow(X). D {is closed in} (ExcludedSet X T) ∧ A⊆D}"

using assms by auto

then have "(A ∪(X∩ T))∈ClosedCovers(A,(ExcludedSet X T))" unfolding ClosedCovers_def

using union_excludedset by auto

then have l1:"\<Inter>ClosedCovers(A,(ExcludedSet X T))⊆(A ∪(X∩ T))" by blast

{

fix U

assume "U∈ClosedCovers(A,(ExcludedSet X T))"

then have "U{is closed in}(ExcludedSet X T)""A⊆U" using ClosedCovers_def

union_excludedset by auto

then have "U=0∨(X∩T)⊆U""A⊆U" using closed_sets_excludedset

by auto

then have "(X∩T)⊆U""A⊆U" using A by auto

then have "(X∩T)∪A⊆U" by auto

}

then have "(A ∪(X∩ T))⊆\<Inter>ClosedCovers(A,(ExcludedSet X T))" using topology0.Top_3_L3

topology0_excludedset union_excludedset assms by auto

with l1 have "\<Inter>ClosedCovers(A,(ExcludedSet X T))=(A ∪(X∩ T))" by auto

then have "Closure(A, ExcludedSet X T) = (A ∪(X∩ T)) "

using Closure_def by auto

}

ultimately show ?thesis by auto

qed

text{*The boundary of a set is @{text "0"} if $A$ is @{text "X"}

or @{text "0"}, and @{text "X∩T"} in other case.*}

lemma boundary_excludedset:

assumes "A ⊆X"

shows "Boundary(A,(ExcludedSet X T))=(if A=0∨A=X then 0 else X∩T)"

proof-

{

have "Closure(0,(ExcludedSet X T))=0""Closure(X - 0,(ExcludedSet X T))=X"

using closure_set_excludedset by auto

then have "Boundary(0,(ExcludedSet X T))=0"using Boundary_def using

union_excludedset assms by auto

}

moreover

{

have "X-X=0" by blast

then have "Closure(X,(ExcludedSet X T))=X""Closure(X-X,(ExcludedSet X T))=0"

using closure_set_excludedset by auto

then have "Boundary(X,(ExcludedSet X T))=0"unfolding Boundary_def using

union_excludedset by auto

}

moreover

{

assume AS:"(A≠0)∧(A≠X)"

then have "(A≠0)""(X-A≠0)" using assms by (safe,blast)

then have "Closure(A,(ExcludedSet X T))=A ∪ (X∩T)""Closure(X-A,(ExcludedSet X T))=(X-A) ∪ (X∩T)"

using closure_set_excludedset[where A="A" and X="X"] assms closure_set_excludedset[where A="X-A"

and X="X"] by auto

then have "Boundary(A,(ExcludedSet X T))=X∩T" unfolding Boundary_def using

union_excludedset by auto

}

ultimately show ?thesis by auto

qed

subsection{*Special cases and subspaces*}

text{*The topology is equal in the sets @{text "T"} and

@{text "X∩T"}.*}

lemma smaller_excludedset:

shows "(ExcludedSet X T)=(ExcludedSet X (X∩T))"

using ExcludedSet_def by (simp,blast)

text{*If the set which is excluded is disjoint with @{text "X"},

then the topology is discrete.*}

lemma empty_excludedset:

assumes "T∩X=0"

shows "(ExcludedSet X T)=Pow(X)"

using smaller_excludedset assms ExcludedSet_def by (simp,blast)

text{*The topological subspaces of the @{text "ExcludedSet X T"} topology

are also ExcludedSet topologies.*}

lemma subspace_excludedset:

shows "(ExcludedSet X T) {restricted to} Y=(ExcludedSet (Y ∩ X) T)"

proof

{

fix M

assume "M∈((ExcludedSet X T) {restricted to} Y)"

then obtain A where A1:"A:(ExcludedSet X T)" "M=Y ∩ A" unfolding RestrictedTo_def by auto

then have "M∈Pow(X ∩ Y)" unfolding ExcludedSet_def by auto

moreover

from A1 have "T∩M=0∨M=Y∩X" unfolding ExcludedSet_def by blast

ultimately have "M∈(ExcludedSet (Y ∩ X) T)" unfolding ExcludedSet_def

by auto

}

then show "(ExcludedSet X T) {restricted to} Y ⊆(ExcludedSet (Y ∩ X) T)" by auto

{

fix M

let ?A="M ∪ ((X∩Y-T)-Y)"

assume A:"M∈(ExcludedSet (Y ∩ X) T)"

{

assume "M=Y ∩ X"

then have "M∈(ExcludedSet X T) {restricted to} Y" unfolding RestrictedTo_def

ExcludedSet_def by auto

}

moreover

{

assume AS:"M≠Y ∩ X"

from A AS have A1:"(M∈Pow(Y ∩ X) ∧ T∩M=0)" unfolding ExcludedSet_def by auto

then have "?A∈Pow(X)" by blast

moreover

have "T∩?A=T∩M" by blast

with A1 have "T∩?A=0" by auto

ultimately have "?A∈(ExcludedSet X T)" unfolding ExcludedSet_def by auto

then have AT:"Y ∩ ?A∈(ExcludedSet X T) {restricted to} Y"unfolding RestrictedTo_def

by auto

have "Y ∩ ?A=Y ∩ M" by blast

also have "…=M" using A1 by auto

finally have "Y ∩ ?A=M".

then have "M∈(ExcludedSet X T) {restricted to} Y" using AT

by auto

}

ultimately have "M∈(ExcludedSet X T) {restricted to} Y" by auto

}

then show "(ExcludedSet (Y ∩ X) T) ⊆ (ExcludedSet X T) {restricted to} Y" by auto

qed

section{*Included Set Topology*}

text{*In this section we consider the subsets of a set which

contain a fixed set.*}

text{*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.*}

subsection{*Included set topology is a topology.*}

definition

IncludedSet ("IncludedSet _ _" 50) where

"IncludedSet X U ≡ {F∈Pow(X). U ⊆ F}∪ {0}"

text{*For any set; we prove that

@{text "IncludedSet X Q"} forms a topology.*}

theorem includedset_is_topology:

shows "(IncludedSet X Q) {is a topology}"

proof-

{

fix M

assume "M∈Pow(IncludedSet X Q)"

then have A:"M⊆{F∈Pow(X). Q ⊆ F}∪ {0}" using IncludedSet_def by auto

then have "\<Union>M∈Pow(X)" by auto

moreover

have"Q ⊆\<Union>M∨ \<Union>M=0" using A by blast

ultimately have "\<Union>M∈(IncludedSet X Q)" using IncludedSet_def by auto

}

moreover

{

fix U V

assume "U∈(IncludedSet X Q)" "V∈(IncludedSet X Q)"

then have "U∈Pow(X)""V∈Pow(X)""U=0∨ Q⊆U""V=0∨ Q⊆V" using IncludedSet_def by auto

then have "U∈Pow(X)""V∈Pow(X)""(U ∩ V)=0 ∨ Q⊆(U ∩ V)" by auto

then have "(U ∩ V)∈(IncludedSet X Q)" using IncludedSet_def by auto

}

ultimately show ?thesis using IsATopology_def by auto

qed

theorem topology0_includedset:

shows "topology0(IncludedSet X T)"

using topology0_def includedset_is_topology by auto

text{*Choosing a singleton set, it is considered a point excluded

topology. In the following lemmas and theorems, when neccessary

it will be considered that @{prop "T≠0"} and @{prop "T⊆X"}.

Theese cases will appear in the special cases section.*}

definition

IncludedPoint ("IncludedPoint _ _" 90) where

"IncludedPoint X p≡ IncludedSet X {p}"

subsection{*Total set, Closed sets, Interior, Closure and Boundary*}

text{*The topology is defined in the set $X$.*}

lemma union_includedset:

assumes "T⊆X "

shows "\<Union> (IncludedSet X T)=X"

proof-

from assms have "X∈(IncludedSet X T)" using IncludedSet_def by auto

then show "\<Union> (IncludedSet X T)=X" using IncludedSet_def by auto

qed

text{*The closed sets are those which are disjoint with @{text "T"}

and @{text "X"}.*}

lemma closed_sets_includedset:

assumes "T⊆X"

shows "D {is closed in} (IncludedSet X T) <-> (D∈Pow(X) & (D ∩ T)=0)∨ D=X"

proof-

have "X-X=0" by blast

then have "X-X∈(IncludedSet X T)" using IncludedSet_def by auto

moreover

{

assume A:"D ⊆ X" "X - D ∈ (IncludedSet X T) "" D ≠ X"

from A(2) have "T⊆(X-D)∨ X-D=0" using IncludedSet_def by auto

with A(1) have "T⊆(X-D)∨ D=X" by blast

with A(3) have "T⊆(X-D)" by auto

hence "D∩T=0" by blast

}

moreover

{

assume A:"D∩T=0""D⊆X"

from A(1) assms have "T⊆(X-D)" by blast

then have "X-D∈(IncludedSet X T)" using IncludedSet_def by auto

}

ultimately show ?thesis using IsClosed_def union_includedset assms by auto

qed

text{*The interior of a set is itself if it is open or

@{text"0"} if it isn't.*}

lemma interior_set_includedset:

assumes "A⊆X"

shows "Interior(A,(IncludedSet X T))= (if T⊆A then A else 0)"

proof-

{

fix x

assume A:"Interior(A, IncludedSet X T) ≠ 0 ""x∈T"

have "Interior(A,IncludedSet X T)∈(IncludedSet X T)" using

topology0.Top_2_L2 topology0_includedset by auto

with A(1) have "T⊆Interior(A, IncludedSet X T)" using IncludedSet_def

by auto

with A(2) have "x∈Interior(A, IncludedSet X T)" by auto

then have "x∈A" using topology0.Top_2_L1 topology0_includedset by auto}

moreover

{

assume "T⊆A"

with assms have "A∈(IncludedSet X T)" using IncludedSet_def by auto

then have "Interior(A,IncludedSet X T)=A" using topology0.Top_2_L3

topology0_includedset by auto

}

ultimately show ?thesis by auto

qed

text{*The closure of a set is itself if it is closed or

@{text "X"} if it isn't.*}

lemma closure_set_includedset:

assumes "A⊆X""T⊆X"

shows "Closure(A,(IncludedSet X T))= (if T∩A=0 then A else X)"

proof-

{

assume AS:"T∩A=0"

then have "A {is closed in} (IncludedSet X T)" using closed_sets_includedset

assms by auto

with assms(1) have "Closure(A,(IncludedSet X T))=A" using topology0.Top_3_L8

topology0_includedset union_includedset assms(2) by auto

}

moreover

{

assume AS:"T∩A≠0"

have "X∈ClosedCovers(A,(IncludedSet X T))" using ClosedCovers_def

closed_sets_includedset union_includedset assms by auto

then have l1:"\<Inter>ClosedCovers(A,(IncludedSet X T))⊆X" using Closure_def

by auto

moreover

{

fix U

assume "U∈ClosedCovers(A,(IncludedSet X T))"

then have "U{is closed in}(IncludedSet X T)""A⊆U" using ClosedCovers_def

by auto

then have "U=X∨(T∩U)=0""A⊆U" using closed_sets_includedset assms(2)

by auto

then have "U=X∨(T∩A)=0" by auto

then have "U=X" using AS by auto

}

then have "X⊆\<Inter>ClosedCovers(A,(IncludedSet X T))" using topology0.Top_3_L3

topology0_includedset union_includedset assms by auto

ultimately have "\<Inter>ClosedCovers(A,(IncludedSet X T))=X" by auto

then have "Closure(A, IncludedSet X T) = X "

using Closure_def by auto

}

ultimately show ?thesis by auto

qed

text{*The boundary of a set is @{text "X-A"} if $A$ contains @{text "T"}

completely, is @{text "A"} if $X-A$ contains @{text "T"}

completely

and @{text "X"} if @{text "T"} is divided between the two sets.

The case where @{prop "T=0"} is considered as an special case.*}

lemma boundary_includedset:

assumes "A ⊆X""T ⊆X""T≠0"

shows "Boundary(A,(IncludedSet X T))=(if T⊆A then X-A else (if T∩A=0 then A else X))"

proof-

{

assume AS:"(T⊆A)"

then have "T∩A≠0""T∩(X-A)=0" using assms(2,3) by (auto,blast)

then have "Closure(A,(IncludedSet X T))=X""Closure(X-A,(IncludedSet X T))=(X-A)"

using closure_set_includedset[where A="A" and X="X"and T="T"] assms(1,2) closure_set_includedset[where A="X-A"

and X="X"and T="T"] by auto

then have "Boundary(A,(IncludedSet X T))=X-A" unfolding Boundary_def using

union_includedset assms(2) by auto

}

moreover

{

assume AS:"~(T⊆A)""T∩A=0"

then have "T∩A=0""T∩(X-A)≠0" using assms(2) by (safe,blast+)

then have "Closure(A,(IncludedSet X T))=A""Closure(X-A,(IncludedSet X T))=X"

using closure_set_includedset[where A="A" and X="X"and T="T"] assms(1,2) closure_set_includedset[where A="X-A"

and X="X"and T="T"] by auto

then have "Boundary(A,(IncludedSet X T))=A" unfolding Boundary_def using

union_includedset assms(1,2) by auto

}

moreover

{

assume AS:"~(T⊆A)""T∩A≠0"

then have "T∩A≠0""T∩(X-A)≠0" using assms(2) by (safe,blast+)

then have "Closure(A,(IncludedSet X T))=X""Closure(X-A,(IncludedSet X T))=X"

using closure_set_includedset[where A="A" and X="X"and T="T"] assms(1,2) closure_set_includedset[where A="X-A"

and X="X"and T="T"] by auto

then have "Boundary(A,(IncludedSet X T))=X" unfolding Boundary_def using

union_includedset assms(2) by auto

}

ultimately show ?thesis by auto

qed

subsection{*Special cases and subspaces*}

text{*The topology is discrete if @{prop "T=0"}*}

lemma smaller_includedset:

shows "(IncludedSet X 0)=Pow(X)"

using IncludedSet_def by (simp,blast)

text{*If the set which is included is not a subset of @{text "X"},

then the topology is trivial.*}

lemma empty_includedset:

assumes "~(T⊆X)"

shows "(IncludedSet X T)={0}"

using assms IncludedSet_def by (simp,blast)

text{*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 @{prop "Y⊆X"} then @{text "IncludedSet (Y ∩ X) (Y∩T)"}

is never trivial. There is no need of a separate proof because

the only subspace of the trivial topology is itself.*}

lemma subspace_includedset:

assumes "T⊆X"

shows "(IncludedSet X T) {restricted to} Y=(IncludedSet (Y ∩ X) (Y∩T))"

proof

{

fix M

assume "M∈((IncludedSet X T) {restricted to} Y)"

then obtain A where A1:"A:(IncludedSet X T)" "M=Y ∩ A" unfolding RestrictedTo_def by auto

then have "M∈Pow(X ∩ Y)" unfolding IncludedSet_def by auto

moreover

from A1 have "Y∩T⊆M∨M=0" unfolding IncludedSet_def by blast

ultimately have "M∈(IncludedSet (Y ∩ X) (Y∩T))" unfolding IncludedSet_def

by auto

}

then show "(IncludedSet X T) {restricted to} Y ⊆(IncludedSet (Y ∩ X) (Y∩T))" by auto

{

fix M

let ?A="M ∪ T"

assume A:"M∈(IncludedSet (Y ∩ X) (Y∩T))"

{

assume "M=0"

then have "M∈(IncludedSet X T) {restricted to} Y" unfolding RestrictedTo_def

IncludedSet_def by auto

}

moreover

{

assume AS:"M≠0"

from A AS have A1:"(M∈Pow(Y ∩ X) ∧ Y ∩T⊆M)" unfolding IncludedSet_def by auto

then have "?A∈Pow(X)" using assms by blast

moreover

have "T⊆?A" by blast

ultimately have "?A∈(IncludedSet X T)" unfolding IncludedSet_def by auto

then have AT:"Y ∩ ?A∈(IncludedSet X T) {restricted to} Y"unfolding RestrictedTo_def

by auto

from A1 have "Y ∩ ?A=Y ∩ M" by blast

also with A1 have "…=M" by auto

finally have "Y ∩ ?A=M".

with AT have "M∈(IncludedSet X T) {restricted to} Y"

by auto

}

ultimately have "M∈(IncludedSet X T) {restricted to} Y" by auto

}

thus "(IncludedSet (Y ∩ X) (Y ∩ T)) ⊆ (IncludedSet X T) {restricted to} Y" by auto

qed

end