Up to index of Isabelle/ZF/IsarMathLib
theory Topology_ZF_examples(*
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 CardinalArith
begin
text{*
This theory deals with some concrete examples of topologies.
*}
section{*Some new ideas on cardinals*}
text{*All the results of this section are done without assuming
the \emph{Axiom of Choice}. With the \emph{Axiom of Choice} in play, the proofs become easier
and some of the assumptions may be dropped.*}
text{*Since General Topology Theory is closely related to Set Theory, it is very interesting
to make use of all the possibilities of Set Theory to try to classify homeomorphic
topological spaces. These ideas are generally used to prove that two topological
spaces are not homeomorphic.*}
subsection{*cases-type results*}
text{*There exist cardinals which are the successor of another cardinal,
but; as happens with ordinal, there are cardinals which are limit cardinal.*}
definition
"LimitC(i) ≡ Card(i) & 0<i & (∀y. (y<i∧Card(y)) --> csucc(y)<i)"
text{*There are three types of cardinals, the zero one, the succesors
of other cardinals and the limit cardinals.*}
lemma Card_cases_disj:
assumes "Card(i)"
shows "i=0 | (∃j. Card(j) & i=csucc(j)) | LimitC(i)"
proof-
from assms have D:"Ord(i)" using Card_is_Ord by auto
{
assume F:"i≠0"
assume False:"~LimitC(i)"
from F D have "0<i" using Ord_0_lt by auto
with False assms have "∃y. y < i ∧ Card(y) ∧ ¬ csucc(y) < i"
using LimitC_def by blast
then obtain y where " y < i ∧ Card(y) ∧ ¬ csucc(y) < i" by blast
with D have " y < i"" i≤csucc(y)" and O:"Card(y)"
using not_lt_imp_le lt_Ord Card_csucc Card_is_Ord
by auto
with assms have "csucc(y)≤i""i≤csucc(y)" using csucc_le by auto
then have "i=csucc(y)" using le_anti_sym by auto
with O have "∃j. Card(j) & i=csucc(j)" by auto
}
then show ?thesis by auto
qed
lemma Card_cases:
assumes "Card (Q)"
obtains ("0") "Q=0" | (csucc) T where "Card(T)" "Q=csucc(T)" | (limit) "LimitC(Q)"
by (insert Card_cases_disj assms, blast)
text{*Given an ordinal bounded by a cardinal in ordinal order, we can change
to the order of sets.*}
lemma le_imp_lesspoll:
assumes "Card(Q)"
shows "A ≤ Q ==> A \<lesssim> Q"
proof-
assume "A ≤ Q"
then have "A<Q∨A=Q" using le_iff by auto
then have "A≈Q∨A< Q" using eqpoll_refl by auto
with assms have "A≈Q∨A\<prec> Q" using lt_Card_imp_lesspoll by auto
then show "A\<lesssim>Q" using lesspoll_def eqpoll_imp_lepoll by auto
qed
text{*There are two types of infinite cardinals, the natural numbers
and those that have at least one infinite strictly smaller cardinal.*}
lemma InfCard_cases_disj:
assumes "InfCard(Q)"
shows "Q=nat ∨ (∃j. csucc(j)\<lesssim>Q & InfCard(j))"
proof-
{
assume "∀j. ¬ csucc(j) \<lesssim> Q ∨ ¬ InfCard(j)"
then have D:"¬ csucc(nat) \<lesssim> Q" using InfCard_nat by auto
with D assms have "¬(csucc(nat) ≤ Q)" using le_imp_lesspoll InfCard_is_Card by auto
with assms have "Q<(csucc(nat))" using not_le_iff_lt Card_is_Ord Card_csucc Card_is_Ord
Card_is_Ord InfCard_is_Card Card_nat by auto
with assms have "Q≤nat" using Card_lt_csucc_iff InfCard_is_Card Card_nat by auto
with assms have "Q=nat" using InfCard_def le_anti_sym by auto
}
then show ?thesis by auto
qed
lemma InfCard_cases:
assumes "InfCard (Q)"
obtains ("nat") "Q=nat"| predecesor j where "csucc(j)\<lesssim>Q ∧ InfCard(j)"
by (insert InfCard_cases_disj assms,blast)
subsection{*Relations between a cardinal and its successor*}
text{*A set is injective and not bijective to the successor of a cardinal
if and only if it is injective and possibly bijective to the cardinal. *}
lemma Card_less_csucc_eq_le:
assumes "Card(m)"
shows "A \<prec> csucc(m) <-> A \<lesssim> m"
proof
have S:"Ord(csucc(m))" using Card_csucc Card_is_Ord assms by auto
{
assume A:"A \<prec> csucc(m)"
with S have "|A|≈A" using lesspoll_imp_eqpoll by auto
also with A have "…\<prec> csucc(m)" by auto
finally have "|A|\<prec> csucc(m)" by auto
then have "|A|\<lesssim>csucc(m)""~(|A|≈csucc(m))" using lesspoll_def by auto
with S have "||A||≤csucc(m)""|A|≠csucc(m)" using lepoll_cardinal_le by auto
then have "|A|≤csucc(m)""|A|≠csucc(m)" using Card_def Card_cardinal by auto
then have "~(csucc(m)<|A|)" "|A|≠csucc(m)" using le_imp_not_lt by auto
then have C:"csucc(m)<|A| --> |A|<csucc(m)""|A|=csucc(m) --> |A|<csucc(m)""|A|<csucc(m) --> |A|<csucc(m)"
by auto
with S have "Ord(|A|)""Ord(csucc(m))" using Card_cardinal Card_is_Ord by auto
with C have "|A|<csucc(m)" using Ord_linear_lt[where thesis="|A|<csucc(m)"] by auto
with assms have "|A|≤m" using Card_lt_csucc_iff Card_cardinal
by auto
then have "|A|=m∨ |A|< m" using le_iff by auto
then have "|A|≈m∨|A|< m" using eqpoll_refl by auto
then have "|A|≈m∨|A|\<prec> m" using lt_Card_imp_lesspoll assms by auto
then have T:"|A|\<lesssim>m" using lesspoll_def eqpoll_imp_lepoll by auto
from A S have "A≈|A|" using lesspoll_imp_eqpoll eqpoll_sym by auto
also with T have "…\<lesssim>m" by auto
finally show "A\<lesssim>m".
}
{
assume A:"A\<lesssim>m"
from assms have "m\<prec>csucc(m)" using lt_Card_imp_lesspoll Card_csucc Card_is_Ord
lt_csucc by auto
with A show "A\<prec>csucc(m)" using lesspoll_trans1 by auto
}
qed
text{*If the successor of a cardinal is infinite, so is the original
cardinal.*}
lemma csucc_inf_imp_inf:
assumes "Card(j)" and "InfCard(csucc(j))"
shows "InfCard(j)"
proof-
{
assume f:"Finite (j)"
then obtain n where "n∈nat" "j≈n" using Finite_def by auto
with assms(1) have TT: "j=n" "n∈nat"
using cardinal_cong nat_into_Card Card_def by auto
then have Q:"succ(j)∈nat" using nat_succI by auto
with f TT have T:"Finite(succ(j))""Card(succ(j))"
using nat_into_Card nat_succI by (simp,blast)
from T(2) have "Card(succ(j))∧ j≤j" using Card_is_Ord by auto
moreover
then have "Ord(succ(j))" using Card_is_Ord by auto
moreover
{
fix x
assume A:"x≤j"
{
assume "Card(succ(j))∧ j<x"
with A have "False" using lt_trans1 by auto
}
then have "~(Card(succ(j))∧ j<x)" by auto
}
ultimately have "(LEAST L. Card(L) ∧ j < L)=succ(j) "
using Least_equality[where i="succ(j)"] by auto
then have "csucc(j)=succ(j)" using csucc_def by auto
with Q have "csucc(j)∈nat" by auto
then have "csucc(j)<nat" using lt_def Card_nat Card_is_Ord by auto
with assms(2) have "False" using InfCard_def lt_trans2 by auto
}
then have "~(Finite (j))" by auto
with assms(1) show ?thesis using Inf_Card_is_InfCard by auto
qed
text{*Since all the cardinals previous to @{term "nat"}
are finite, it cannot be a successor cardinal; hence it is
a @{term "LimitC"} cardinal.*}
corollary LimitC_nat:
shows "LimitC(nat)"
proof-
note Card_nat
moreover
have "0<nat" using lt_def by auto
moreover
{
fix y
assume AS:"y<nat""Card(y)"
then have ord:"Ord(y)" unfolding lt_def by auto
then have Cacsucc:"Card(csucc(y))" using Card_csucc by auto
{
assume "nat≤csucc(y)"
with Cacsucc have "InfCard(csucc(y))" using InfCard_def by auto
with AS(2) have "InfCard(y)" using csucc_inf_imp_inf by auto
then have "nat≤y" using InfCard_def by auto
with AS(1) have "False" using lt_trans2 by auto
}
then have "~(nat≤csucc(y))" by auto
then have "csucc(y)<nat" using not_le_iff_lt Ord_nat Cacsucc Card_is_Ord by auto
}
ultimately show ?thesis using LimitC_def by auto
qed
subsection{*Main result on cardinals (without the \emph{Axiom of Choice})*}
text{*If two sets are strictly injective to an infinite cardinal,
then so is its union. For the case of successor cardinal, this
theorem is done in the isabelle library in a more general setting;
but that theorem is of not
use in the case where @{prop "LimitC(Q)"} and it also makes use
of the \emph{Axiom of Choice}. The mentioned theorem is in the
theory file @{text "Cardinal_AC.thy"}*}
text{*Note that if $Q$ is finite and different from $1$, let's assume $Q=n$,
then the union of $A$ and $B$ is not bounded by $Q$.
Counterexample: two disjoint sets of $n-1$ elements each
have a union of $2n-2$ elements which are more than $n$.*}
text{*Note also that if $Q=1$ then $A$ and $B$ must be empty
and the union is then empty too; and $Q$ cannot be @{term "0"} because
no set is injective and not bijective to @{term "0"}.*}
text{* The proof is divided in two parts, first the case when
both sets $A$ and $B$ are finite; and second,
the part when at least one of them is infinite.
In the first part, it is used the fact that a finite
union of finite sets is finite. In the second part it
is used the linear order on cardinals (ordinals).
This proof can not be generalized to a setting with
an infinite union easily.*}
lemma less_less_imp_un_less:
assumes "A\<prec>Q" and "B\<prec>Q" and "InfCard(Q)"
shows "A ∪ B\<prec>Q"
proof-
{
assume "Finite (A) & Finite(B)"
then have "Finite(A ∪ B)" using Finite_Un by auto
then obtain n where R:"A ∪ B ≈n" "n∈nat" using Finite_def
by auto
then have "|A ∪ B|<nat" using lt_def cardinal_cong
nat_into_Card Card_def Card_nat Card_is_Ord by auto
with assms(3) have T:"|A ∪ B|<Q" using InfCard_def lt_trans2 by auto
from R have "Ord(n)""A ∪ B \<lesssim> n" using nat_into_Card Card_is_Ord eqpoll_imp_lepoll by auto
then have "A ∪ B≈|A ∪ B|" using lepoll_Ord_imp_eqpoll eqpoll_sym by auto
also with T assms(3) have "…\<prec>Q" using lt_Card_imp_lesspoll InfCard_is_Card
by auto
finally have "A ∪ B\<prec>Q".
}
moreover
{
assume "~(Finite (A) & Finite(B))"
then have A:"~Finite (A) ∨ ~Finite(B)" by auto
from assms have B:"|A|≈A""|B|≈B" using lesspoll_imp_eqpoll lesspoll_imp_eqpoll
InfCard_is_Card Card_is_Ord by auto
from B(1) have Aeq:"∀x. (|A|≈x) --> (A≈x)"
using eqpoll_sym eqpoll_trans by blast
from B(2) have Beq:"∀x. (|B|≈x) --> (B≈x)"
using eqpoll_sym eqpoll_trans by blast
with A Aeq have "~Finite(|A|)∨ ~Finite(|B|)" using Finite_def
by auto
then have D:"InfCard(|A|)∨InfCard(|B|)" using Inf_Card_is_InfCard Inf_Card_is_InfCard Card_cardinal by blast
{
assume AS:"|A| < |B|"
{
assume "~InfCard(|A|)"
with D have "InfCard(|B|)" by auto
}
moreover
{
assume "InfCard(|A|)"
then have "nat≤|A|" using InfCard_def by auto
with AS have "nat<|B|" using lt_trans1 by auto
then have "nat≤|B|" using leI by auto
then have "InfCard(|B|)" using InfCard_def Card_cardinal by auto
}
ultimately have INFB:"InfCard(|B|)" by auto
then have "2<|B|" using InfCard_def lt_trans2[where i="2"]
lt_def by auto
then have AG:"2\<lesssim>|B|" using lt_Card_imp_lesspoll Card_cardinal lesspoll_def
by auto
from B(2) have "|B|≈B" .
also with assms(2) have "…\<prec>Q" by auto
finally have TTT:"|B|\<prec>Q".
from B(1) have "Card(|B|)""A \<lesssim>|A|" using eqpoll_sym Card_cardinal eqpoll_imp_lepoll by auto
with AS have "A\<prec>|B|" using lt_Card_imp_lesspoll lesspoll_trans1 by auto
then have I1:"A\<lesssim>|B|" using lesspoll_def by auto
from B(2) have I2:"B\<lesssim>|B|" using eqpoll_sym eqpoll_imp_lepoll by auto
have "A ∪ B\<lesssim>A+B" using Un_lepoll_sum by auto
also with I1 I2 have "…\<lesssim> |B| + |B|" using sum_lepoll_mono by auto
also with AG have "…\<lesssim>|B| * |B|" using sum_lepoll_prod by auto
also from assms(3) INFB have "…≈|B|" using InfCard_square_eqpoll
by auto
finally have "A ∪ B\<lesssim>|B|".
also with TTT have "…\<prec>Q" by auto
finally have "A ∪ B\<prec>Q".
}
moreover
{
assume AS:"|B| < |A|"
{
assume "~InfCard(|B|)"
with D have "InfCard(|A|)" by auto}
moreover
{
assume "InfCard(|B|)"
then have "nat≤|B|" using InfCard_def by auto
with AS have "nat<|A|" using lt_trans1 by auto
then have "nat≤|A|" using leI by auto
then have "InfCard(|A|)" using InfCard_def Card_cardinal by auto
}
ultimately have INFB:"InfCard(|A|)" by auto
then have "2<|A|" unfolding InfCard_def using lt_trans2[where i= "2"]
using lt_def by auto
then have AG:"2\<lesssim>|A|" using lt_Card_imp_lesspoll[OF Card_cardinal] lesspoll_def
by auto
from B(1) have "|A|≈A" .
also with assms(1) have "…\<prec>Q" by auto
finally have TTT:"|A|\<prec>Q".
from B(2) have "Card(|A|)""B \<lesssim>|B|" using eqpoll_sym Card_cardinal eqpoll_imp_lepoll by auto
with AS have "B\<prec>|A|" using lt_Card_imp_lesspoll lesspoll_trans1 by auto
then have I1:"B\<lesssim>|A|" using lesspoll_def by auto
from B(1) have I2:"A\<lesssim>|A|" using eqpoll_sym eqpoll_imp_lepoll by auto
have "A ∪ B\<lesssim>A+B" using Un_lepoll_sum by auto
also with I1 I2 have "…\<lesssim> |A| + |A|" using sum_lepoll_mono by auto
also with AG have "…\<lesssim>|A| * |A|" using sum_lepoll_prod by auto
also from INFB assms(3) have "…≈|A|" using InfCard_square_eqpoll
by auto
finally have "A ∪ B\<lesssim>|A|".
also with TTT have "…\<prec>Q" by auto
finally have "A ∪ B\<prec>Q".
}
moreover
{
assume AS:"|A|=|B|"
with D have INFB:"InfCard(|A|)" by auto
then have "2<|A|" using InfCard_def lt_trans2[where i="2"]
using lt_def by auto
then have AG:"2\<lesssim>|A|" using lt_Card_imp_lesspoll Card_cardinal using lesspoll_def
by auto
from B(1) have "|A|≈A".
also with assms(1) have "…\<prec>Q" by auto
finally have TTT:"|A|\<prec>Q".
from AS B have I1:"A\<lesssim>|A|"and I2:"B\<lesssim>|A|" using eqpoll_refl eqpoll_imp_lepoll
eqpoll_sym by auto
have "A ∪ B\<lesssim>A+B" using Un_lepoll_sum by auto
also with I1 I2 have "…\<lesssim> |A| + |A|" using sum_lepoll_mono by auto
also with AG have "…\<lesssim>|A| * |A|" using sum_lepoll_prod by auto
also from assms(3) INFB have "…≈|A|" using InfCard_square_eqpoll
by auto
finally have "A ∪ B\<lesssim>|A|".
also with TTT have "…\<prec>Q" by auto
finally have "A ∪ B\<prec>Q".
}
ultimately have "A ∪ B\<prec>Q" using Ord_linear_lt[where thesis= "A ∪ B\<prec>Q"] Card_cardinal Card_is_Ord by auto
}
ultimately show "A ∪ B\<prec>Q" by auto
qed
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
@{term "CoCardinal X Q"} forms a topology. The proof is done
with an infinite cardinal, but it is obvious that the set @{term "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 @{term "CoCardinal X T"} is a topology,
@{prop "X≠0"}, @{prop "Card(T)"} and @{prop "T≠0"}; then @{term "T"} is an infinite cardinal, @{prop "X\<prec>T"}
or @{term "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
@{term "CoCardinal X T"} topology. In each case, we will not assume
sufficient conditions for @{term "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 @{term "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
@{term "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 @{term "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 @{term "0"} if $A$ and $X-A$ are closed,
@{term "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 @{term "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
@{term "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 @{term "(X ∩ T)"} and @{term "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 @{term "X"} or
the difference with the set @{term"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 @{term "0"} or
the union with @{term "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 @{term "0"} if $A$ is @{term "X"}
or @{term "0"}, and @{term "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 @{term "T"} and
@{term "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 @{term "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 @{term "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
@{term "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 @{term "T"}
and @{term "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
@{term"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
@{term "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 @{term "X-A"} if $A$ contains @{term "T"}
completely, is @{term "A"} if $X-A$ contains @{term "T"}
completely
and @{term "X"} if @{term "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 @{term "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 @{term "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 @{term "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