(* 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. *) section ‹Topology - examples› theory Topology_ZF_examples imports Topology_ZF Cardinal_ZF begin text‹ This theory deals with some concrete examples of topologies. › subsection‹CoCardinal Topology › text‹ In this section we define and prove the basic properties of the co-cardinal topology on a set $X$.› 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(X,T) ≡ {F∈Pow(X). X-F ≺ T}∪ {0}" text‹For any set and any infinite cardinal we prove that ‹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 "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 "⋃M∈Pow(X)" by auto moreover { assume B:"M=0" then have "⋃M∈?T" using CoCardinal_def by auto } moreover { assume B:"M={0}" then have "⋃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 ≺ (Q)" using CoCardinal_def by auto from C have "X-⋃M⊆X-T" by blast with D have "X-⋃M≺ (Q)" using subset_imp_lepoll lesspoll_trans1 by blast } ultimately have "⋃M∈?T" using CoCardinal_def by auto } moreover { fix U and V assume "U∈?T" and "V∈?T" then have A:"U=0 ∨ (U∈Pow(X) ∧ X-U≺ (Q))" and B:"V=0 ∨ (V∈Pow(X) ∧ X-V≺ (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)≺ (Q))" using less_less_imp_un_less assms by auto then have "U∩V∈?T" using CoCardinal_def by auto } ultimately show ?thesis using IsATopology_def by auto qed text‹ We can use theorems proven in ‹topology0› context for the co-cardinal topology. › 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 ‹CoCardinal(X,T)› is a topology, ‹ X≠0, Card(T)› and ‹T≠0›; then ‹T› is an infinite cardinal, ‹ X≺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 ("CoFinite _" 90) where "CoFinite X ≡ CoCardinal(X,nat)" text‹Cocountable topology in fact consists of the empty set and all cocountable subsets of $X$.› 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 ‹CoCardinal(X,T)› topology. In each case, we will not assume sufficient conditions for ‹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 "⋃ CoCardinal(X,T) = X" proof- have X:"X-X=0" by auto have "0 ≲ 0" by auto with assms have "0≺1""1 ≲T" using not_0_is_lepoll_1 lepoll_imp_lesspoll_succ by auto then have "0≺T" using lesspoll_trans2 by auto with X have "(X-X)≺T" by auto then have "X∈CoCardinal(X,T)" using CoCardinal_def by auto hence "X⊆⋃ CoCardinal(X,T)" by blast then show "⋃ 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≺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 auto with A(2) have "D≺T" using CoCardinal_def by simp } with assms have "D {is closed in} CoCardinal(X,T) ⟶ (D∈Pow(X) ∧ D≺T)∨ D=X" using IsClosed_def union_cocardinal by auto moreover { assume A:"D ≺ T""D ⊆ X" from A(2) have "X-(X-D)=D" by blast with A(1) have "X-(X-D)≺ T" by auto then have "X-D∈ CoCardinal(X,T)" using CoCardinal_def by auto } with assms have "(D∈Pow(X) ∧ D≺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 ‹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) ≺ T) then A else 0)" proof- from assms(2) have dif_dif:"X-(X-A)=A" by blast { assume "(X-A) ≺ T" then have "(X-A)∈Pow(X) ∧ (X-A) ≺ 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⊆⋃{U∈CoCardinal(X,T). U ⊆ A}" by auto have a2:"⋃{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) ≺ T)" { fix U assume "U ⊆A" hence "X-A ⊆ X-U" by blast then have Q:"X-A ≲ X-U" using subset_imp_lepoll by auto { assume "X-U≺ T" with Q have "X-A≺ T" using lesspoll_trans1 by auto with as have "False" by auto } hence "~((X-U) ≺ 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 ‹topology0› context since ‹ T≠0"} › is too weak for ‹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 ‹X› if it isn't closed.› lemma closure_set_cocardinal: assumes "T≠0""A⊆X" shows "Closure(A,CoCardinal(X,T))=(if (A ≺ T) then A else X)" proof- { assume "A ≺ 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:"⋂ClosedCovers(A,CoCardinal(X,T))⊆A" by blast from S have l2:"A ⊆ ⋂ClosedCovers(A,CoCardinal(X,T))" unfolding ClosedCovers_def by auto from l1 l2 have "Closure(A,CoCardinal(X,T))=A" using Closure_def by auto } moreover { assume as:"¬ A ≺ T" { fix U assume "A⊆U" then have Q:"A ≲ U" using subset_imp_lepoll by auto { assume "U≺ T" with Q have "A≺ T" using lesspoll_trans1 by auto with as have "False" by auto } hence "¬ U ≺ 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 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≠0""A⊆X" shows "Boundary(A,CoCardinal(X,T)) = (if A≺ T then (if (X-A)≺ T then 0 else A) else (if (X-A)≺ T then X-A else X))" proof- from assms(2) have "X-A ⊆ X" by auto { assume AS: "A≺T" "X-A ≺ T" with assms ‹X-A ⊆ X› have "Closure(X-A,CoCardinal(X,T)) = X-A" and "Closure(A,CoCardinal(X,T)) = A" using closure_set_cocardinal by auto with assms(1) have "Boundary(A,CoCardinal(X,T)) = 0" using Boundary_def union_cocardinal by auto } moreover { assume AS: "~(A≺T)" "X-A ≺ T" with assms ‹X-A ⊆ X› have "Closure(X-A,CoCardinal(X,T)) = X-A" and "Closure(A,CoCardinal(X,T)) = X" using closure_set_cocardinal by auto with assms(1) have "Boundary(A,CoCardinal(X,T))=X-A" using Boundary_def union_cocardinal by auto } moreover { assume AS:"~(A≺T)" "~(X-A ≺ T)" with assms ‹X-A ⊆ X› have "Closure(X-A,CoCardinal(X,T))=X" and "Closure(A,CoCardinal(X,T))=X" using closure_set_cocardinal by auto with assms(1) have "Boundary(A,CoCardinal(X,T))=X" using Boundary_def union_cocardinal by auto } moreover { assume AS:"A≺ T" "~(X-A≺T)" with assms ‹X-A ⊆ X› have "Closure(X-A,CoCardinal(X,T))=X" and "Closure(A,CoCardinal(X,T)) = A" using closure_set_cocardinal by auto with assms have "Boundary(A,CoCardinal(X,T))=A" using Boundary_def union_cocardinal by auto } ultimately show ?thesis by auto qed 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≺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 ≲X" using subset_imp_lepoll by auto then have "X-U≺ 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 ‹ 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)" and "Q=0 ∨ X-Q≺1" using CoCardinal_def by auto then have "Q ∈ Pow(X)" and "Q=0 ∨ X-Q=0" using lesspoll_succ_iff lepoll_0_iff by auto 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≺1" and "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 ‹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 with ‹(Y ∩ X)-M = (Y ∩ X)-A› have "(Y ∩ X)-M⊆ X-A" by auto then have "(Y ∩ X)-M ≲ X-A" using subset_imp_lepoll by auto with A1 have "(Y ∩ X)-M ≺ T ∨ M=0" using lesspoll_trans1 CoCardinal_def by auto 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≺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≺ 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 from A1 have "…=M" by auto finally have "Y ∩ ?A=M" by simp 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 subsection‹Excluded Set Topology› text‹In this section, we consider all the subsets of a set which have empty intersection with a fixed set.› text‹ The excluded set topology consists of subsets of $X$ that are disjoint with a fixed set $U$. › definition "ExcludedSet(X,U) ≡ {F∈Pow(X). U ∩ F=0}∪ {X}" text‹For any set; we prove that ‹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 "⋃M∈Pow(X)" by auto moreover { have B:"Q ∩⋃M=⋃{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 ∩ ⋃M=0" by auto } moreover { assume "X∈M" with A have "⋃M=X" by auto } ultimately have "Q ∩ ⋃M=0 ∨ ⋃M=X" by auto } ultimately have "⋃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 text‹We can use ‹topology0› when discussing excluded set topology. › 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 in excluded topology.› definition "ExcludedPoint(X,p) ≡ ExcludedSet(X,{p})" subsection‹Total set, closed sets, interior, closure and boundary› text‹Here we discuss what are closed sets, interior, closure and boundary in excluded set topology.› text‹The topology is defined in the set $X$› lemma union_excludedset: shows "⋃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 ‹(X ∩ T)› and ‹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 ‹X› or the difference with the set ‹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 auto 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 ‹0› or the union with ‹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" with assms have "(A∪(X∩T)) {is closed in}ExcludedSet(X,T)" using closed_sets_excludedset 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:"⋂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)" and "A⊆U" using ClosedCovers_def union_excludedset by auto then have "U=0∨(X∩T)⊆U" and "A⊆U" using closed_sets_excludedset by auto with A have "(X∩T)⊆U""A⊆U" by auto hence "(X∩T)∪A⊆U" by auto } with assms have "(A ∪(X∩ T)) ⊆ ⋂ClosedCovers(A,ExcludedSet(X,T))" using topology0.Top_3_L3 topology0_excludedset union_excludedset by auto with l1 have "⋂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 ‹0› if $A$ is ‹X› or ‹0›, and ‹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" and "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 "A≠0" and "A≠X" then have "X-A≠0" using assms by auto with assms ‹A≠0› ‹A⊆X› have "Closure(A,ExcludedSet(X,T)) = A ∪ (X∩T)" using closure_set_excludedset by simp moreover from ‹A⊆X› have "X-A ⊆ X" by blast with ‹X-A≠0› have "Closure(X-A,ExcludedSet(X,T)) = (X-A) ∪ (X∩T)" using closure_set_excludedset by simp ultimately have "Boundary(A,ExcludedSet(X,T)) = X∩T" using Boundary_def union_excludedset by auto } ultimately show ?thesis by auto qed subsection‹Special cases and subspaces› text‹This section provides some miscellaneous facts about excluded set topologies. › text‹The excluded set topology is equal in the sets ‹T› and ‹X∩T›.› lemma smaller_excludedset: shows "ExcludedSet(X,T) = ExcludedSet(X,(X∩T))" proof show "ExcludedSet(X,T) ⊆ ExcludedSet(X, X∩T)" and "ExcludedSet(X, X∩T) ⊆ExcludedSet(X,T)" unfolding ExcludedSet_def by auto qed text‹If the set which is excluded is disjoint with ‹X›, then the topology is discrete.› lemma empty_excludedset: assumes "T∩X=0" shows "ExcludedSet(X,T) = Pow(X)" proof from assms show "ExcludedSet(X,T) ⊆ Pow(X)" using smaller_excludedset ExcludedSet_def by auto from assms show "Pow(X) ⊆ExcludedSet(X,T)" unfolding ExcludedSet_def by blast qed text‹The topological subspaces of the ‹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" by simp with AT have "M ∈ExcludedSet(X,T) {restricted to} Y" 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 subsection‹Included Set Topology› text‹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.› text‹ We define the included set topology as the collection of supersets of some fixed subset of the space $X$. › definition "IncludedSet(X,U) ≡ {F∈Pow(X). U ⊆ F} ∪ {0}" text‹ In the next theorem we prove that ‹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 "⋃M∈Pow(X)" by auto moreover have"Q ⊆⋃M∨ ⋃M=0" using A by blast ultimately have "⋃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 text‹ We can reference the theorems proven in the ‹topology0› context when discussing the included set topology.› 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 ‹T≠0› and ‹T⊆X›. These cases will appear in the special cases section.› definition IncludedPoint ("IncludedPoint _ _" 90) where "IncludedPoint X p ≡ IncludedSet(X,{p})" subsection‹Basic topological notions in included set topology› text‹ This section discusses total set, closed sets, interior, closure and boundary for included set topology. › text‹The topology is defined in the set $X$.› lemma union_includedset: assumes "T⊆X " shows "⋃IncludedSet(X,T) = X" proof- from assms have "X ∈ IncludedSet(X,T)" using IncludedSet_def by auto then show "⋃IncludedSet(X,T) = X" using IncludedSet_def by auto qed text‹The closed sets are those which are disjoint with ‹T› and ‹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 the empty set 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 the whole space if it is not.› 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:"⋂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 ⊆ ⋂ClosedCovers(A,IncludedSet(X,T))" using topology0.Top_3_L3 topology0_includedset union_includedset assms by auto ultimately have "⋂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 ‹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⊆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 - from ‹A⊆X› have "X-A ⊆ X" by auto { assume "T⊆A" with assms(2,3) have "T∩A≠0" and "T∩(X-A)=0" by auto with assms(1,2) ‹X-A ⊆ X› have "Closure(A,IncludedSet(X,T)) = X" and "Closure(X-A,IncludedSet(X,T)) = (X-A)" using closure_set_includedset by auto with assms(2) have "Boundary(A,IncludedSet(X,T)) = X-A" using Boundary_def union_includedset by auto } moreover { assume "~(T⊆A)" and "T∩A=0" with assms(2) have "T∩(X-A)≠0" by auto with assms(1,2) ‹T∩A=0› ‹X-A ⊆ X› have "Closure(A,IncludedSet(X,T)) = A" and "Closure(X-A,IncludedSet(X,T)) = X" using closure_set_includedset by auto with assms(1,2) have "Boundary(A,IncludedSet(X,T))=A" using Boundary_def union_includedset by auto } moreover { assume "~(T⊆A)" and "T∩A ≠ 0" with assms(1,2) have "T∩(X-A) ≠ 0" by auto with assms(1,2) ‹T∩A≠0› ‹X-A ⊆ X› have "Closure(A,IncludedSet(X,T)) = X" and "Closure(X-A,IncludedSet(X,T)) = X" using closure_set_includedset by auto with assms(2) have "Boundary(A,IncludedSet(X,T)) = X" using Boundary_def union_includedset by auto } ultimately show ?thesis by auto qed subsection‹Special cases and subspaces› text‹ 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. › text‹The topology is discrete if ‹ T=0 ›› lemma smaller_includedset: shows "IncludedSet(X,0) = Pow(X)" proof show "IncludedSet(X,0) ⊆ Pow(X)" and "Pow(X) ⊆ IncludedSet(X,0)" unfolding IncludedSet_def by auto qed text‹If the set which is included is not a subset of ‹X›, then the topology is trivial.› lemma empty_includedset: assumes "~(T⊆X)" shows "IncludedSet(X,T) = {0}" proof from assms show "IncludedSet(X,T) ⊆ {0}" and "{0} ⊆ IncludedSet(X,T)" unfolding IncludedSet_def by auto qed text‹The topological subspaces of the ‹IncludedSet(X,T)› topology are also IncludedSet topologies. The trivial case does not fit the idea in the demonstration because if ‹Y⊆X› then ‹IncludedSet(Y∩X, Y∩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⊆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 from A1 have "…=M" by auto finally have "Y∩?A = M" by simp 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