(* 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\_1.thy}*} theory Topology_ZF_examples_1 imports Topology_ZF_1 Order_ZF begin text{*In this theory file we reformulate the concepts related to a topology in relation with a base of the topology and we give examples of topologies defined by bases or subbases.*} section{*New ideas using a base for a topology*} subsection{*The topology of a base*} text{*Given a family of subsets satisfiying the base condition, it is posible to construct a topology where that family is a base. Even more, it is the only topology with such characteristics.*} definition TopologyWithBase ("TopologyBase _ " 50) where "U {satisfies the base condition} ⟹ TopologyBase U ≡ THE T. U {is a base for} T" theorem Base_topology_is_a_topology: assumes "U {satisfies the base condition}" shows "(TopologyBase U) {is a topology}" and "U {is a base for} (TopologyBase U)" proof- from assms obtain T where "U {is a base for} T" using Top_1_2_T1(2) by blast then have "∃!T. U {is a base for} T" using same_base_same_top ex1I[where P= "λT. U {is a base for} T"] by blast with assms show "U {is a base for} (TopologyBase U) " using theI[where P= "λT. U {is a base for} T"] TopologyWithBase_def by auto with assms show "(TopologyBase U) {is a topology}" using Top_1_2_T1(1) IsAbaseFor_def by auto qed text{*A base doesn't need the empty set.*} lemma base_no_0: shows "B{is a base for}T ⟷ (B-{0}){is a base for}T" proof- { fix M assume "M∈{⋃A . A ∈ Pow(B)}" then obtain Q where "M=⋃Q""Q∈Pow(B)" by auto hence "M=⋃(Q-{0})""Q-{0}∈Pow(B-{0})" by auto hence "M∈{⋃A . A ∈ Pow(B - {0})}" by auto } hence "{⋃A . A ∈ Pow(B)} ⊆ {⋃A . A ∈ Pow(B - {0})}" by blast moreover { fix M assume "M∈{⋃A . A ∈ Pow(B-{0})}" then obtain Q where "M=⋃Q""Q∈Pow(B-{0})" by auto hence "M=⋃(Q)""Q∈Pow(B)" by auto hence "M∈{⋃A . A ∈ Pow(B)}" by auto } hence " {⋃A . A ∈ Pow(B - {0})} ⊆ {⋃A . A ∈ Pow(B)} " by auto ultimately have "{⋃A . A ∈ Pow(B - {0})} = {⋃A . A ∈ Pow(B)} " by auto then show "B{is a base for}T ⟷ (B-{0}){is a base for}T" using IsAbaseFor_def by auto qed text{*The interior of a set is the union of all the sets of the base which are fully contained by it.*} lemma interior_set_base_topology: assumes "U {is a base for} T""T{is a topology}" shows "Interior(A,T)=⋃{T∈U. T⊆A}" proof have "{T∈U. T⊆A}⊆U" by auto with assms(1) have "⋃{T∈U. T⊆A}∈T" using IsAbaseFor_def by auto moreover have "⋃{T∈U. T⊆A}⊆A" by blast with calculation assms(2) show "⋃{T∈U. T⊆A}⊆Interior(A,T)" using topology0.Top_2_L5 topology0_def by auto { fix x assume "x∈Interior(A,T)" with assms obtain V where "V∈U""V⊆Interior(A,T)""x∈V" using point_open_base_neigh topology0.Top_2_L2 topology0_def by blast with assms have "V∈U""x∈V""V⊆A" using topology0.Top_2_L1 topology0_def by(safe,blast) hence "x∈⋃{T∈U. T⊆A}" by auto } thus "Interior(A, T) ⊆ ⋃{T ∈ U . T ⊆ A} " by auto qed text{*In the following, we offer another lemma about the closure of a set given a basis for a topology. This lemma is based on @{text "cl_inter_neigh"} and @{text "inter_neigh_cl"}. It states that it is only necessary to check the sets of the base, not all the open sets.*} lemma closure_set_base_topology: assumes "U {is a base for} Q""Q{is a topology}""A⊆⋃Q" shows "Closure(A,Q)={x∈⋃Q. ∀T∈U. x∈T⟶A∩T≠0}" proof { fix x assume A:"x∈Closure(A,Q)" with assms(2,3) have B:"x∈⋃Q" using topology0_def topology0.Top_3_L11(1) by blast moreover { fix T assume "T∈U""x∈T" with assms(1) have "T∈Q""x∈T" using base_sets_open by auto with assms(2,3) A have "A∩T≠0" using topology0_def topology0.cl_inter_neigh[where U="T" and T="Q" and A="A"] by auto } hence "∀T∈U. x∈T⟶A∩T≠0" by auto ultimately have "x∈{x∈⋃Q. ∀T∈U. x∈T⟶A∩T≠0}" by auto } thus "Closure(A, Q) ⊆{x∈⋃Q. ∀T∈U. x∈T⟶A∩T≠0}" by auto { fix x assume AS:"x∈{x ∈ ⋃Q . ∀T∈U. x ∈ T ⟶ A ∩ T ≠ 0}" hence "x∈⋃Q" by blast moreover { fix R assume "R∈Q" with assms(1) obtain W where RR:"W⊆U""R=⋃W" using IsAbaseFor_def by auto { assume "x∈R" with RR(2) obtain WW where TT:"WW∈W""x∈WW" by auto { assume "R∩A=0" with RR(2) TT(1) have "WW∩A=0" by auto with TT(1) RR(1) have "WW∈U""WW∩A=0" by auto with AS have "x∈⋃Q-WW" by auto with TT(2) have "False" by auto } hence "R∩A≠0" by auto } } hence "∀U∈Q. x∈U ⟶ U∩A≠0" by auto with calculation assms(2,3) have "x∈Closure(A,Q)" using topology0_def topology0.inter_neigh_cl by auto } then show "{x ∈ ⋃Q . ∀T∈U. x ∈ T ⟶ A ∩ T ≠ 0}⊆Closure(A,Q)" by auto qed text{* The restriction of a base is a base for the restriction.*} lemma subspace_base_topology: assumes "B{is a base for}T" shows "(B{restricted to}Y){is a base for}(T{restricted to}Y)" proof- { fix t assume "t∈RepFun({⋃A . A ∈ Pow(B)}, op ∩(Y))" then obtain x where A:"t=Y∩x""x∈{⋃A . A ∈ Pow(B)}" by auto then obtain A where B:"x=⋃A""A∈Pow(B)" by auto from A(1) B(1) have "t=⋃(A {restricted to} Y)" using RestrictedTo_def by auto with B(2) have "t∈{⋃A . A ∈ Pow(RepFun(B, op ∩(Y)))}" unfolding RestrictedTo_def by blast } hence "RepFun({⋃A . A ∈ Pow(B)}, op ∩(Y)) ⊆ {⋃A . A ∈ Pow(RepFun(B, op ∩(Y)))}" by(auto+) moreover { fix t assume "t∈{⋃A . A ∈ Pow(RepFun(B, op ∩(Y)))}" then obtain A where A:"A⊆ B{restricted to}Y""t=⋃A" using RestrictedTo_def by auto let ?AA="{C∈B. Y∩C∈A}" from A(1) have "?AA⊆B""A=?AA {restricted to}Y" using RestrictedTo_def by auto with A(2) have "?AA⊆B""t=⋃(?AA {restricted to}Y)" by auto then have "?AA⊆B""t=Y∩(⋃?AA)" using RestrictedTo_def by auto hence "t∈RepFun({⋃A . A ∈ Pow(B)}, op ∩(Y))" by auto } hence "{⋃A . A ∈ Pow(RepFun(B, op ∩(Y)))} ⊆ RepFun({⋃A . A ∈ Pow(B)}, op ∩(Y)) " by (auto+) ultimately have "{⋃A . A ∈ Pow(RepFun(B, op ∩(Y)))} = RepFun({⋃A . A ∈ Pow(B)}, op ∩(Y))" by auto with assms show ?thesis using RestrictedTo_def IsAbaseFor_def by auto qed text{*If the base of a topology is contained in the base of another topology, then the topologies maintain the same relation.*} theorem base_subset: assumes "B{is a base for}T""B2{is a base for}T2""B⊆B2" shows "T⊆T2" proof { fix x assume "x∈T" with assms(1) obtain M where "M⊆B""x=⋃M" using IsAbaseFor_def by auto with assms(3) have "M⊆B2""x=⋃M" by auto with assms(2) show "x∈T2" using IsAbaseFor_def by auto } qed subsection{*Dual Base for Closed Sets*} text{*A dual base for closed sets is the collection of complements of sets of a base for the topology.*} definition DualBase ("DualBase _ _" 80) where "B{is a base for}T ⟹ DualBase B T≡{⋃T-U. U∈B}∪{⋃T}" lemma closed_inter_dual_base: assumes "D{is closed in}T""B{is a base for}T" obtains M where "M⊆DualBase B T""D=⋂M" proof- assume K:"⋀M. M ⊆ DualBase B T ⟹ D = ⋂M ⟹ thesis" { assume AS:"D≠⋃T" from assms(1) have D:"D∈Pow(⋃T)""⋃T-D∈T" using IsClosed_def by auto hence A:"⋃T-(⋃T-D)=D""⋃T-D∈T" by auto with assms(2) obtain Q where QQ:"Q∈Pow(B)""⋃T-D=⋃Q" using IsAbaseFor_def by auto { assume "Q=0" then have "⋃Q=0" by auto with QQ(2) have "⋃T-D=0" by auto with D(1) have "D=⋃T" by auto with AS have "False" by auto } hence QNN:"Q≠0" by auto from QQ(2) A(1) have "D=⋃T-⋃Q" by auto with QNN have "D=⋂{⋃T-R. R∈Q}" by auto moreover with assms(2) QQ(1) have "{⋃T-R. R∈Q}⊆DualBase B T" using DualBase_def by auto with calculation K have "thesis" by auto } moreover { assume AS:"D=⋃T" with assms(2) have "{⋃T}⊆DualBase B T" using DualBase_def by auto moreover have "⋃T = ⋂{⋃T}" by auto with calculation K AS have thesis by auto } ultimately show thesis by auto qed text{* We have already seen for a base that whenever there is a union of open sets, we can consider only basic open sets due to the fact that any open set is a union of basic open sets. What we should expect now is that when there is an intersection of closed sets, we can consider only dual basic closed sets.*} lemma closure_dual_base: assumes "U {is a base for} Q""Q{is a topology}""A⊆⋃Q" shows "Closure(A,Q)=⋂{T∈DualBase U Q. A⊆T}" proof from assms(1) have T:"⋃Q∈DualBase U Q" using DualBase_def by auto moreover { fix T assume A:"T∈DualBase U Q" "A⊆T" with assms(1) obtain R where "(T=⋃Q-R∧R∈U)∨T=⋃Q" using DualBase_def by auto with A(2) assms(1,2) have "(T{is closed in}Q)""A⊆T""T∈Pow(⋃Q)" using topology0.Top_3_L1 topology0_def topology0.Top_3_L9 base_sets_open by auto } then have SUB:"{T∈DualBase U Q. A⊆T}⊆{T∈Pow(⋃Q). (T{is closed in}Q)∧A⊆T}" by blast with calculation assms(3) have "⋂{T∈Pow(⋃Q). (T{is closed in}Q)∧A⊆T}⊆⋂{T∈DualBase U Q. A⊆T}" by auto then show "Closure(A,Q)⊆⋂{T∈DualBase U Q. A⊆T}" using Closure_def ClosedCovers_def by auto { fix x assume A:"x∈⋂{T∈DualBase U Q. A⊆T}" { fix T assume B:"x∈T""T∈U" { assume C:"A∩T=0" from B(2) assms(1) have "⋃Q-T∈DualBase U Q" using DualBase_def by auto moreover from C assms(3) have "A⊆⋃Q-T" by auto moreover from B(1) have "x∉⋃Q-T" by auto ultimately have "x∉⋂{T∈DualBase U Q. A⊆T}" by auto with A have "False" by auto } hence "A∩T≠0" by auto } hence "∀T∈U. x∈T⟶A∩T≠0" by auto moreover from T A assms(3) have "x∈⋃Q" by auto with calculation assms have "x∈Closure(A,Q)" using closure_set_base_topology by auto } thus "⋂{T ∈ DualBase U Q . A ⊆ T} ⊆ Closure(A, Q)" by auto qed section{*Partition topology*} text{*In the theory file Partitions\_ZF.thy; there is a definition to work with partitions. In this setting is much easier to work with a family of subsets.*} definition IsAPartition ("_{is a partition of}_" 90) where "(U {is a partition of} X) ≡ (⋃U=X ∧ (∀A∈U. ∀B∈U. A=B∨ A∩B=0)∧ 0∉U)" text{* A subcollection of a partition is a partition of its union.*} lemma subpartition: assumes "U {is a partition of} X" "V⊆U" shows "V{is a partition of}⋃V" using assms unfolding IsAPartition_def by auto text{* A restriction of a partition is a partition. If the empty set appears it has to be removed.*} lemma restriction_partition: assumes "U {is a partition of}X" shows "((U {restricted to} Y)-{0}) {is a partition of} (X∩Y)" using assms unfolding IsAPartition_def RestrictedTo_def by fast text{*Given a partition, the complement of a union of a subfamily is a union of a subfamily.*} lemma diff_union_is_union_diff: assumes "R⊆P" "P {is a partition of} X" shows "X - ⋃R=⋃(P-R)" proof { fix x assume "x∈X - ⋃R" hence P:"x∈X""x∉⋃R" by auto { fix T assume "T∈R" with P(2) have "x∉T" by auto } with P(1) assms(2) obtain Q where "Q∈(P-R)""x∈Q" using IsAPartition_def by auto hence "x∈⋃(P-R)" by auto } thus "X - ⋃R⊆⋃(P-R)" by auto { fix x assume "x∈⋃(P-R)" then obtain Q where "Q∈P-R""x∈Q" by auto hence C: "Q∈P""Q∉R""x∈Q" by auto then have "x∈⋃P" by auto with assms(2) have "x∈X" using IsAPartition_def by auto moreover { assume "x∈⋃R" then obtain t where G:"t∈R" "x∈t" by auto with C(3) assms(1) have "t∩Q≠0""t∈P" by auto with assms(2) C(1,3) have "t=Q" using IsAPartition_def by blast with C(2) G(1) have "False" by auto } hence "x∉⋃R" by auto ultimately have "x∈X-⋃R" by auto } thus "⋃(P-R)⊆X - ⋃R" by auto qed subsection{*Partition topology is a topology.*} text{* A partition satisfies the base condition.*} lemma partition_base_condition: assumes "P {is a partition of} X" shows "P {satisfies the base condition}" proof- { fix U V assume AS:"U∈P∧V∈P" with assms have A:"U=V∨ U∩V=0" using IsAPartition_def by auto { fix x assume ASS:"x∈U∩V" with A have "U=V" by auto with AS ASS have "U∈P""x∈U∧ U⊆U∩V" by auto hence "∃W∈P. x∈W∧ W⊆U∩V" by auto } hence "(∀x ∈ U∩V. ∃W∈P. x∈W ∧ W ⊆ U∩V)" by auto } then show ?thesis using SatisfiesBaseCondition_def by auto qed text{*Since a partition is a base of a topology, and this topology is uniquely determined; we can built it. In the definition we have to make sure that we have a partition.*} definition PartitionTopology ("PTopology _ _" 50) where "(U {is a partition of} X) ⟹ PTopology X U ≡ TopologyBase U" theorem Ptopology_is_a_topology: assumes "U {is a partition of} X" shows "(PTopology X U) {is a topology}" and "U {is a base for} (PTopology X U)" using assms Base_topology_is_a_topology partition_base_condition PartitionTopology_def by auto lemma topology0_ptopology: assumes "U {is a partition of} X" shows "topology0(PTopology X U)" using Ptopology_is_a_topology topology0_def assms by auto subsection{*Total set, Closed sets, Interior, Closure and Boundary*} text{*The topology is defined in the set $X$*} lemma union_ptopology: assumes "U {is a partition of} X" shows "⋃(PTopology X U)=X" using assms Ptopology_is_a_topology(2) Top_1_2_L5 IsAPartition_def by auto text{*The closed sets are the open sets.*} lemma closed_sets_ptopology: assumes "T {is a partition of} X" shows"D {is closed in} (PTopology X T) ⟷ D∈(PTopology X T)" proof from assms have B:"T{is a base for}(PTopology X T)" using Ptopology_is_a_topology(2) by auto { fix D assume "D {is closed in} (PTopology X T)" with assms have A:"D∈Pow(X)""X-D∈(PTopology X T)" using IsClosed_def union_ptopology by auto from A(2) B obtain R where Q:"R⊆T" "X-D=⋃R" using Top_1_2_L1[where B="T" and U="X-D"] by auto from A(1) have "X-(X-D)=D" by blast with Q(2) have "D=X-⋃R" by auto with Q(1) assms have "D=⋃(T-R)" using diff_union_is_union_diff by auto with B show "D∈(PTopology X T)" using IsAbaseFor_def by auto } { fix D assume "D∈(PTopology X T)" with B obtain R where Q:"R⊆T""D=⋃R" using IsAbaseFor_def by auto hence "X-D=X-⋃R" by auto with Q(1) assms have "X-D=⋃(T-R)" using diff_union_is_union_diff by auto with B have "X-D∈(PTopology X T)" using IsAbaseFor_def by auto moreover from Q have "D⊆⋃T" by auto with assms have "D⊆X" using IsAPartition_def by auto with calculation assms show "D{is closed in} (PTopology X T)" using IsClosed_def union_ptopology by auto } qed text{*There is a formula for the interior given by an intersection of sets of the dual base. Is the intersection of all the closed sets of the dual basis such that they do not complement $A$ to $X$. Since the interior of $X$ must be inside $X$, we have to enter $X$ as one of the sets to be intersected.*} lemma interior_set_ptopology: assumes "U {is a partition of} X""A⊆X" shows "Interior(A,(PTopology X U))=⋂{T∈DualBase U (PTopology X U). T=X∨T∪A≠X}" proof { fix x assume "x∈Interior(A,(PTopology X U))" with assms obtain R where A:"x∈R""R∈(PTopology X U)""R⊆A" using topology0.open_open_neigh topology0_ptopology topology0.Top_2_L2 topology0.Top_2_L1 by auto with assms obtain B where B:"B⊆U""R=⋃B" using Ptopology_is_a_topology(2) IsAbaseFor_def by auto from A(1,3) assms have XX:"x∈X""X∈{T∈DualBase U (PTopology X U). T=X∨T∪A≠X}" using union_ptopology[of "U""X"] DualBase_def[of"U"] Ptopology_is_a_topology(2)[of "U""X"] by (safe,blast,auto) moreover from B(2) A(1) obtain S where C:"S∈B""x∈S" by auto { fix T assume AS:"T∈DualBase U (PTopology X U)""T ∪A≠X" from AS(1) assms obtain w where "(T=X-w∧w∈U)∨(T=X)" using DualBase_def union_ptopology Ptopology_is_a_topology(2) by auto with assms(2) AS(2) have D:"T=X-w""w∈U" by auto from D(2) have "w⊆⋃U" by auto with assms(1) have "w⊆⋃(PTopology X U)" using Ptopology_is_a_topology(2) Top_1_2_L5[of "U""PTopology X U"] by auto with assms(1) have "w⊆X" using union_ptopology by auto with D(1) have "X-T=w" by auto with D(2) have "X-T∈U" by auto { assume "x∈X-T" with C B(1) have "S∈U""S∩(X-T)≠0" by auto with `X-T∈U` assms(1) have "X-T=S" using IsAPartition_def by auto with `X-T=w``T=X-w` have "X-S=T" by auto with AS(2) have "X-S∪A≠X" by auto from A(3) B(2) C(1) have "S⊆A" by auto hence "X-A⊆X-S" by auto with assms(2) have "X-S∪A=X" by auto with `X-S∪A≠X` have "False" by auto } then have "x∈T" using XX by auto } ultimately have "x∈⋂{T∈DualBase U (PTopology X U). T=X∨T∪A≠X}" by auto } thus "Interior(A,(PTopology X U))⊆⋂{T∈DualBase U (PTopology X U). T=X∨T∪A≠X}" by auto { fix x assume p:"x∈⋂{T∈DualBase U (PTopology X U). T=X∨T∪A≠X}" hence noE:"⋂{T∈DualBase U (PTopology X U). T=X∨T∪A≠X}≠0" by auto { fix T assume "T∈DualBase U (PTopology X U)" with assms(1) obtain w where "T=X∨(w∈U∧T=X-w)" using DualBase_def Ptopology_is_a_topology(2) union_ptopology by auto with assms(1) have "T=X∨(w∈(PTopology X U)∧T=X-w)" using base_sets_open Ptopology_is_a_topology(2) by blast with assms(1) have "T{is closed in}(PTopology X U)" using topology0.Top_3_L1[where T="PTopology X U"] topology0_ptopology topology0.Top_3_L9[where T="PTopology X U"] union_ptopology by auto } moreover from assms(1) p have "X∈{T∈DualBase U (PTopology X U). T=X∨T∪A≠X}"and X:"x∈X" using Ptopology_is_a_topology(2) DualBase_def union_ptopology by auto with calculation assms(1) have "(⋂{T∈DualBase U (PTopology X U). T=X∨T∪A≠X}) {is closed in}(PTopology X U)" using topology0.Top_3_L4[where K="{T∈DualBase U (PTopology X U). T=X∨T∪A≠X}"] topology0_ptopology[where U="U" and X="X"] by auto with assms(1) have ab:"(⋂{T∈DualBase U (PTopology X U). T=X∨T∪A≠X})∈(PTopology X U)" using closed_sets_ptopology by auto with assms(1) obtain B where "B∈Pow(U)""(⋂{T∈DualBase U (PTopology X U). T=X∨T∪A≠X})=⋃B" using Ptopology_is_a_topology(2) IsAbaseFor_def by auto with p obtain R where "x∈R""R∈U""R⊆(⋂{T∈DualBase U (PTopology X U). T=X∨T∪A≠X})" by auto with assms(1) have R:"x∈R""R∈(PTopology X U)""R⊆(⋂{T∈DualBase U (PTopology X U). T=X∨T∪A≠X})""X-R∈DualBase U (PTopology X U)" using base_sets_open Ptopology_is_a_topology(2) DualBase_def union_ptopology by (safe,blast,simp,blast) { assume "(X-R) ∪A≠X" with R(4) have "X-R∈{T∈DualBase U (PTopology X U). T=X∨T∪A≠X}" by auto hence "⋂{T∈DualBase U (PTopology X U). T=X∨T∪A≠X}⊆X-R" by auto with R(3) have "R⊆X-R" using subset_trans[where A="R" and C="X-R"] by auto hence "R=0" by blast with R(1) have "False" by auto } hence I:"(X-R) ∪A=X" by auto { fix y assume ASR:"y∈R" with R(2) have "y∈⋃(PTopology X U)" by auto with assms(1) have XX:"y∈X" using union_ptopology by auto with I have "y∈(X-R) ∪A" by auto with XX have "y∉R∨y∈A" by auto with ASR have "y∈A" by auto } hence "R⊆A" by auto with R(1,2) have "∃R∈(PTopology X U). (x∈R∧R⊆A)" by auto with assms(1) have "x∈Interior(A,(PTopology X U))" using topology0.Top_2_L6 topology0_ptopology by auto } thus "⋂{T ∈ DualBase U PTopology X U . T = X ∨ T ∪ A ≠ X} ⊆ Interior(A, PTopology X U)" by auto qed text{*The closure of a set is the union of all the sets of the partition which intersect with @{text "A"}.*} lemma closure_set_ptopology: assumes "U {is a partition of} X""A⊆X" shows "Closure(A,(PTopology X U))=⋃{T∈U. T∩A≠0}" proof { fix x assume A:"x∈Closure(A,(PTopology X U))" with assms have "x∈⋃(PTopology X U)" using topology0.Top_3_L11(1)[where T="PTopology X U" and A="A"] topology0_ptopology union_ptopology by auto with assms(1) have "x∈⋃U" using Top_1_2_L5[where B="U" and T="PTopology X U"] Ptopology_is_a_topology(2) by auto then obtain W where B:"x∈W""W∈U" by auto with A have "x∈Closure(A,(PTopology X U))∩W" by auto moreover from assms B(2) have "W∈(PTopology X U)""A⊆X" using base_sets_open Ptopology_is_a_topology(2) by (safe,blast) with calculation assms(1) have "A∩W≠0" using topology0_ptopology[where U="U" and X="X"] topology0.cl_inter_neigh union_ptopology by auto with B have "x∈⋃{T∈U. T∩A≠0}" by blast } thus "Closure(A, PTopology X U) ⊆ ⋃{T ∈ U . T ∩ A ≠ 0}" by auto { fix x assume "x∈⋃{T ∈ U . T ∩ A ≠ 0}" then obtain T where A:"x∈T""T∈U""T∩A≠0" by auto from assms have "A⊆⋃(PTopology X U)" using union_ptopology by auto moreover from A(1,2) assms(1) have "x∈⋃(PTopology X U)" using Top_1_2_L5[where B="U" and T="PTopology X U"] Ptopology_is_a_topology(2) by auto moreover { fix Q assume B:"Q∈(PTopology X U)""x∈Q" with assms(1) obtain M where C:"Q=⋃M""M⊆U" using Ptopology_is_a_topology(2) IsAbaseFor_def by auto from B(2) C(1) obtain R where D:"R∈M""x∈R" by auto with C(2) A(1,2) have "R∩T≠0""R∈U""T∈U" by auto with assms(1) have "R=T" using IsAPartition_def by auto with C(1) D(1) have "T⊆Q" by auto with A(3) have "Q∩A≠0" by auto } then have "∀Q∈(PTopology X U). x∈Q ⟶ Q∩A≠0" by auto with calculation assms(1) have "x∈Closure(A,(PTopology X U))" using topology0.inter_neigh_cl topology0_ptopology by auto } then show "⋃{T ∈ U . T ∩ A ≠ 0} ⊆ Closure(A, PTopology X U) " by auto qed text{*The boundary of a set is given by the union of the sets of the partition which have non empty intersection with the set but that are not fully contained in it. Another equivalent statement would be: the union of the sets of the partition which have non empty intersection with the set and its complement.*} lemma boundary_set_ptopology: assumes "U {is a partition of} X""A⊆X" shows "Boundary(A,(PTopology X U))=⋃{T∈U. T∩A≠0 ∧ ~(T⊆A)}" proof- from assms have "Closure(A,(PTopology X U))=⋃{T ∈ U . T ∩ A ≠ 0}" using closure_set_ptopology by auto moreover from assms(1) have "Interior(A,(PTopology X U))=⋃{T ∈ U . T ⊆ A}" using interior_set_base_topology Ptopology_is_a_topology[where U="U" and X="X"] by auto with calculation assms have A:"Boundary(A,(PTopology X U))=⋃{T ∈ U . T ∩ A ≠ 0} - ⋃{T ∈ U . T ⊆ A}" using topology0.Top_3_L12 topology0_ptopology union_ptopology by auto from assms(1) have "({T ∈ U . T ∩ A ≠ 0}) {is a partition of} ⋃({T ∈ U . T ∩ A ≠ 0})" using subpartition by blast moreover { fix T assume "T∈U""T⊆A" with assms(1) have "T∩A=T""T≠0" using IsAPartition_def by auto with `T∈U` have "T∩A≠0""T∈U" by auto } then have "{T ∈ U . T ⊆ A}⊆{T ∈ U . T ∩ A ≠ 0}" by auto ultimately have "⋃{T ∈ U . T ∩ A ≠ 0} - ⋃{T ∈ U . T ⊆ A}=⋃(({T ∈ U . T ∩ A ≠ 0})-({T ∈ U . T ⊆ A}))" using diff_union_is_union_diff by auto also have "…=⋃({T ∈ U . T ∩ A ≠ 0 ∧ ~(T⊆A)})" by blast with calculation A show ?thesis by auto qed subsection{*Special cases and subspaces*} text{*The discrete and the indiscrete topologies appear as special cases of this partition topologies.*} lemma discrete_partition: shows "{{x}.x∈X} {is a partition of}X" using IsAPartition_def by auto lemma indiscrete_partition: assumes "X≠0" shows "{X} {is a partition of} X" using assms IsAPartition_def by auto theorem discrete_ptopology: shows "(PTopology X {{x}.x∈X})=Pow(X)" proof { fix t assume "t∈(PTopology X {{x}.x∈X})" hence "t⊆⋃(PTopology X {{x}.x∈X})" by auto then have "t∈Pow(X)" using union_ptopology discrete_partition by auto } thus "(PTopology X {{x}.x∈X})⊆Pow(X)" by auto { fix t assume A:"t∈Pow(X)" have "⋃({{x}. x∈t})=t" by auto moreover from A have "{{x}. x∈t}∈Pow({{x}.x∈X})" by auto hence "⋃({{x}. x∈t})∈{⋃A . A ∈ Pow({{x} . x ∈ X})}" by auto ultimately have "t∈(PTopology X {{x} . x ∈ X})" using Ptopology_is_a_topology(2) discrete_partition IsAbaseFor_def by auto } thus "Pow(X) ⊆ (PTopology X {{x} . x ∈ X}) " by auto qed theorem indiscrete_ptopology: assumes "X≠0" shows "(PTopology X {X})={0,X}" proof { fix T assume "T∈(PTopology X {X})" with assms obtain M where "M⊆{X}""⋃M=T" using Ptopology_is_a_topology(2) indiscrete_partition IsAbaseFor_def by auto then have "T=0∨T=X" by auto } then show "(PTopology X {X})⊆{0,X}" by auto from assms have "0∈(PTopology X {X})" using Ptopology_is_a_topology(1) empty_open indiscrete_partition by auto moreover from assms have "⋃(PTopology X {X})∈(PTopology X {X})" using union_open Ptopology_is_a_topology(1) indiscrete_partition by auto with assms have "X∈(PTopology X {X})" using union_ptopology indiscrete_partition by auto ultimately show "{0,X}⊆(PTopology X {X})" by auto qed text{*The topological subspaces of the @{text "(PTopology X U)"} are partition topologies.*} lemma subspace_ptopology: assumes "U{is a partition of}X" shows "(PTopology X U) {restricted to} Y=(PTopology (X∩Y) ((U {restricted to} Y)-{0}))" proof- from assms have "U{is a base for}(PTopology X U)" using Ptopology_is_a_topology(2) by auto then have "(U{restricted to} Y){is a base for}(PTopology X U){restricted to} Y" using subspace_base_topology by auto then have "((U{restricted to} Y)-{0}){is a base for}(PTopology X U){restricted to} Y" using base_no_0 by auto moreover from assms have "((U{restricted to} Y)-{0}) {is a partition of} (X∩Y)" using restriction_partition by auto then have "((U{restricted to} Y)-{0}){is a base for}(PTopology (X∩Y) ((U {restricted to} Y)-{0}))" using Ptopology_is_a_topology(2) by auto ultimately show ?thesis using same_base_same_top by auto qed section{*Order topologies*} subsection{*Order topology is a topology*} text{*Given a totally ordered set, several topologies can be defined using the order relation. First we define an open interval, notice that the set defined as @{text "Interval"} is a closed interval; and open rays.*} definition IntervalX where "IntervalX(X,r,b,c)≡(Interval(r,b,c)∩X)-{b,c}" definition LeftRayX where "LeftRayX(X,r,b)≡{c∈X. ⟨c,b⟩∈r}-{b}" definition RightRayX where "RightRayX(X,r,b)≡{c∈X. ⟨b,c⟩∈r}-{b}" text{*Intersections of intervals and rays.*} lemma inter_two_intervals: assumes "bu∈X""bv∈X""cu∈X""cv∈X""IsLinOrder(X,r)" shows "IntervalX(X,r,bu,cu)∩IntervalX(X,r,bv,cv)=IntervalX(X,r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv))" proof have T:"GreaterOf(r,bu,bv)∈X""SmallerOf(r,cu,cv)∈X" using assms GreaterOf_def SmallerOf_def by (cases "⟨bu,bv⟩∈r",simp,simp,cases "⟨cu,cv⟩∈r",simp,simp) { fix x assume ASS:"x∈IntervalX(X,r,bu,cu)∩IntervalX(X,r,bv,cv)" then have "x∈IntervalX(X,r,bu,cu)""x∈IntervalX(X,r,bv,cv)" by auto then have BB:"x∈X""x∈Interval(r,bu,cu)""x≠bu""x≠cu""x∈Interval(r,bv,cv)""x≠bv""x≠cv" using IntervalX_def assms by auto then have "x∈X" by auto moreover have "x≠GreaterOf(r,bu,bv)""x≠SmallerOf(r,cu,cv)" proof- show "x≠GreaterOf(r,bu,bv)" using GreaterOf_def BB(6,3) by (cases "⟨bu,bv⟩∈r",simp+) show "x≠SmallerOf(r,cu,cv)" using SmallerOf_def BB(7,4) by (cases "⟨cu,cv⟩∈r",simp+) qed moreover have "⟨bu,x⟩∈r""⟨x,cu⟩∈r""⟨bv,x⟩∈r""⟨x,cv⟩∈r" using BB(2,5) Order_ZF_2_L1A by auto then have "⟨GreaterOf(r,bu,bv),x⟩∈r""⟨x,SmallerOf(r,cu,cv)⟩∈r" using GreaterOf_def SmallerOf_def by (cases "⟨bu,bv⟩∈r",simp,simp,cases "⟨cu,cv⟩∈r",simp,simp) then have "x∈Interval(r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv))" using Order_ZF_2_L1 by auto ultimately have "x∈IntervalX(X,r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv))" using IntervalX_def T by auto } then show "IntervalX(X, r, bu, cu) ∩ IntervalX(X, r, bv, cv) ⊆ IntervalX(X, r, GreaterOf(r, bu, bv), SmallerOf(r, cu, cv))" by auto { fix x assume "x∈IntervalX(X,r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv))" then have BB:"x∈X""x∈Interval(r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv))""x≠GreaterOf(r,bu,bv)""x≠SmallerOf(r,cu,cv)" using IntervalX_def T by auto then have "x∈X" by auto moreover from BB(2) have CC:"⟨GreaterOf(r,bu,bv),x⟩∈r""⟨x,SmallerOf(r,cu,cv)⟩∈r" using Order_ZF_2_L1A by auto { { assume AS:"⟨bu,bv⟩∈r" then have "GreaterOf(r,bu,bv)=bv" using GreaterOf_def by auto then have "⟨bv,x⟩∈r" using CC(1) by auto with AS have "⟨bu,x⟩∈r" "⟨bv,x⟩∈r" using assms IsLinOrder_def trans_def by (safe, blast) } moreover { assume AS:"⟨bu,bv⟩∉r" then have "GreaterOf(r,bu,bv)=bu" using GreaterOf_def by auto then have "⟨bu,x⟩∈r" using CC(1) by auto from AS have "⟨bv,bu⟩∈r" using assms IsLinOrder_def IsTotal_def assms by auto with `⟨bu,x⟩∈r` have "⟨bu,x⟩∈r" "⟨bv,x⟩∈r" using assms IsLinOrder_def trans_def by (safe, blast) } ultimately have R:"⟨bu,x⟩∈r" "⟨bv,x⟩∈r" by auto moreover { assume AS:"x=bu" then have "⟨bv,bu⟩∈r" using R(2) by auto then have "GreaterOf(r,bu,bv)=bu" using GreaterOf_def assms IsLinOrder_def antisym_def by auto then have "False" using AS BB(3) by auto } moreover { assume AS:"x=bv" then have "⟨bu,bv⟩∈r" using R(1) by auto then have "GreaterOf(r,bu,bv)=bv" using GreaterOf_def by auto then have "False" using AS BB(3) by auto } ultimately have "⟨bu,x⟩∈r" "⟨bv,x⟩∈r""x≠bu""x≠bv" by auto } moreover { { assume AS:"⟨cu,cv⟩∈r" then have "SmallerOf(r,cu,cv)=cu" using SmallerOf_def by auto then have "⟨x,cu⟩∈r" using CC(2) by auto with AS have "⟨x,cu⟩∈r" "⟨x,cv⟩∈r" using assms IsLinOrder_def trans_def by(safe ,blast) } moreover { assume AS:"⟨cu,cv⟩∉r" then have "SmallerOf(r,cu,cv)=cv" using SmallerOf_def by auto then have "⟨x,cv⟩∈r" using CC(2) by auto from AS have "⟨cv,cu⟩∈r" using assms IsLinOrder_def IsTotal_def by auto with `⟨x,cv⟩∈r` have "⟨x,cv⟩∈r" "⟨x,cu⟩∈r" using assms IsLinOrder_def trans_def by(safe ,blast) } ultimately have R:"⟨x,cv⟩∈r" "⟨x,cu⟩∈r" by auto moreover { assume AS:"x=cv" then have "⟨cv,cu⟩∈r" using R(2) by auto then have "SmallerOf(r,cu,cv)=cv" using SmallerOf_def assms IsLinOrder_def antisym_def by auto then have "False" using AS BB(4) by auto } moreover { assume AS:"x=cu" then have "⟨cu,cv⟩∈r" using R(1) by auto then have "SmallerOf(r,cu,cv)=cu" using SmallerOf_def by auto then have "False" using AS BB(4) by auto } ultimately have "⟨x,cu⟩∈r" "⟨x,cv⟩∈r""x≠cu""x≠cv" by auto } ultimately have "x∈IntervalX(X,r,bu,cu)" "x∈IntervalX(X,r,bv,cv)" using Order_ZF_2_L1 IntervalX_def assms by auto then have "x∈IntervalX(X, r, bu, cu) ∩ IntervalX(X, r, bv, cv) " by auto } then show "IntervalX(X,r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv)) ⊆ IntervalX(X, r, bu, cu) ∩ IntervalX(X, r, bv, cv)" by auto qed lemma inter_rray_interval: assumes "bv∈X""bu∈X""cv∈X""IsLinOrder(X,r)" shows "RightRayX(X,r,bu)∩IntervalX(X,r,bv,cv)=IntervalX(X,r,GreaterOf(r,bu,bv),cv)" proof { fix x assume "x∈RightRayX(X,r,bu)∩IntervalX(X,r,bv,cv)" then have "x∈RightRayX(X,r,bu)""x∈IntervalX(X,r,bv,cv)" by auto then have BB:"x∈X""x≠bu""x≠bv""x≠cv""⟨bu,x⟩∈r""x∈Interval(r,bv,cv)" using RightRayX_def IntervalX_def by auto then have "⟨bv,x⟩∈r""⟨x,cv⟩∈r" using Order_ZF_2_L1A by auto with `⟨bu,x⟩∈r` have "⟨GreaterOf(r,bu,bv),x⟩∈r" using GreaterOf_def by (cases "⟨bu,bv⟩∈r",simp+) with `⟨x,cv⟩∈r` have "x∈Interval(r,GreaterOf(r,bu,bv),cv)" using Order_ZF_2_L1 by auto then have "x∈IntervalX(X,r,GreaterOf(r,bu,bv),cv)" using BB(1-4) IntervalX_def GreaterOf_def by (simp) } then show "RightRayX(X, r, bu) ∩ IntervalX(X, r, bv, cv) ⊆ IntervalX(X, r, GreaterOf(r, bu, bv), cv)" by auto { fix x assume "x∈IntervalX(X, r, GreaterOf(r, bu, bv), cv)" then have "x∈X""x∈Interval(r,GreaterOf(r, bu, bv), cv)""x≠cv""x≠GreaterOf(r, bu, bv)" using IntervalX_def by auto then have R:"⟨GreaterOf(r, bu, bv),x⟩∈r""⟨x,cv⟩∈r" using Order_ZF_2_L1A by auto with `x≠cv` have "⟨x,cv⟩∈r""x≠cv" by auto moreover { { assume AS:"⟨bu,bv⟩∈r" then have "GreaterOf(r,bu,bv)=bv" using GreaterOf_def by auto then have "⟨bv,x⟩∈r" using R(1) by auto with AS have "⟨bu,x⟩∈r" "⟨bv,x⟩∈r" using assms unfolding IsLinOrder_def trans_def by (safe,blast) } moreover { assume AS:"⟨bu,bv⟩∉r" then have "GreaterOf(r,bu,bv)=bu" using GreaterOf_def by auto then have "⟨bu,x⟩∈r" using R(1) by auto from AS have "⟨bv,bu⟩∈r" using assms unfolding IsLinOrder_def IsTotal_def using assms by auto with `⟨bu,x⟩∈r` have "⟨bu,x⟩∈r" "⟨bv,x⟩∈r" using assms unfolding IsLinOrder_def trans_def by (safe,blast) } ultimately have T:"⟨bu,x⟩∈r" "⟨bv,x⟩∈r" by auto moreover { assume AS:"x=bu" then have "⟨bv,bu⟩∈r" using T(2) by auto then have "GreaterOf(r,bu,bv)=bu" unfolding GreaterOf_def using assms unfolding IsLinOrder_def antisym_def by auto with `x≠GreaterOf(r,bu,bv)` have "False" using AS by auto } moreover { assume AS:"x=bv" then have "⟨bu,bv⟩∈r" using T(1) by auto then have "GreaterOf(r,bu,bv)=bv" unfolding GreaterOf_def by auto with `x≠GreaterOf(r,bu,bv)` have "False" using AS by auto } ultimately have "⟨bu,x⟩∈r" "⟨bv,x⟩∈r""x≠bu""x≠bv" by auto } with calculation `x∈X` have "x∈RightRayX(X, r, bu)""x∈IntervalX(X, r, bv, cv)" unfolding RightRayX_def IntervalX_def using Order_ZF_2_L1 by auto then have "x∈RightRayX(X, r, bu) ∩ IntervalX(X, r, bv, cv) " by auto } then show "IntervalX(X, r, GreaterOf(r, bu, bv), cv) ⊆ RightRayX(X, r, bu) ∩ IntervalX(X, r, bv, cv) " by auto qed lemma inter_lray_interval: assumes "bv∈X""cu∈X""cv∈X""IsLinOrder(X,r)" shows "LeftRayX(X,r,cu)∩IntervalX(X,r,bv,cv)=IntervalX(X,r,bv,SmallerOf(r,cu,cv))" proof { fix x assume "x∈LeftRayX(X,r,cu)∩IntervalX(X,r,bv,cv)" then have B:"x≠cu""x∈X""⟨x,cu⟩∈r""⟨bv,x⟩∈r""⟨x,cv⟩∈r""x≠bv""x≠cv" unfolding LeftRayX_def IntervalX_def Interval_def by auto from `⟨x,cu⟩∈r` `⟨x,cv⟩∈r` have C:"⟨x,SmallerOf(r, cu, cv)⟩∈r" using SmallerOf_def by (cases "⟨cu,cv⟩∈r",simp+) from B(7,1) have "x≠SmallerOf(r,cu,cv)" using SmallerOf_def by (cases "⟨cu,cv⟩∈r",simp+) then have "x∈IntervalX(X,r,bv,SmallerOf(r,cu,cv))" using B C IntervalX_def Order_ZF_2_L1 by auto } then show "LeftRayX(X, r, cu) ∩ IntervalX(X, r, bv, cv) ⊆ IntervalX(X, r, bv, SmallerOf(r, cu, cv))" by auto { fix x assume "x∈IntervalX(X,r,bv,SmallerOf(r,cu,cv))" then have R:"x∈X""⟨bv,x⟩∈r""⟨x,SmallerOf(r,cu,cv)⟩∈r""x≠bv""x≠SmallerOf(r,cu,cv)" using IntervalX_def Interval_def by auto then have "⟨bv,x⟩∈r""x≠bv" by auto moreover { { assume AS:"⟨cu,cv⟩∈r" then have "SmallerOf(r,cu,cv)=cu" using SmallerOf_def by auto then have "⟨x,cu⟩∈r" using R(3) by auto with AS have "⟨x,cu⟩∈r" "⟨x,cv⟩∈r" using assms unfolding IsLinOrder_def trans_def by (safe, blast) } moreover { assume AS:"⟨cu,cv⟩∉r" then have "SmallerOf(r,cu,cv)=cv" using SmallerOf_def by auto then have "⟨x,cv⟩∈r" using R(3) by auto from AS have "⟨cv,cu⟩∈r" using assms IsLinOrder_def IsTotal_def assms by auto with `⟨x,cv⟩∈r` have "⟨x,cv⟩∈r" "⟨x,cu⟩∈r" using assms IsLinOrder_def trans_def by (safe, blast) } ultimately have T:"⟨x,cv⟩∈r" "⟨x,cu⟩∈r" by auto moreover { assume AS:"x=cu" then have "⟨cu,cv⟩∈r" using T(1) by auto then have "SmallerOf(r,cu,cv)=cu" using SmallerOf_def assms IsLinOrder_def antisym_def by auto with `x≠SmallerOf(r,cu,cv)` have "False" using AS by auto } moreover { assume AS:"x=cv" then have "⟨cv,cu⟩∈r" using T(2) by auto then have "SmallerOf(r,cu,cv)=cv" using SmallerOf_def assms IsLinOrder_def antisym_def by auto with `x≠SmallerOf(r,cu,cv)` have "False" using AS by auto } ultimately have "⟨x,cu⟩∈r" "⟨x,cv⟩∈r""x≠cu""x≠cv" by auto } with calculation `x∈X` have "x∈LeftRayX(X,r,cu)""x∈IntervalX(X, r, bv, cv)" using LeftRayX_def IntervalX_def Interval_def by auto then have "x∈LeftRayX(X, r, cu) ∩ IntervalX(X, r, bv, cv)" by auto } then show "IntervalX(X, r, bv, SmallerOf(r, cu, cv)) ⊆ LeftRayX(X, r, cu) ∩ IntervalX(X, r, bv, cv) " by auto qed lemma inter_lray_rray: assumes "bu∈X""cv∈X""IsLinOrder(X,r)" shows "LeftRayX(X,r,bu)∩RightRayX(X,r,cv)=IntervalX(X,r,cv,bu)" unfolding LeftRayX_def RightRayX_def IntervalX_def Interval_def by auto lemma inter_lray_lray: assumes "bu∈X""cv∈X""IsLinOrder(X,r)" shows "LeftRayX(X,r,bu)∩LeftRayX(X,r,cv)=LeftRayX(X,r,SmallerOf(r,bu,cv))" proof { fix x assume "x∈LeftRayX(X,r,bu)∩LeftRayX(X,r,cv)" then have B:"x∈X""⟨x,bu⟩∈r""⟨x,cv⟩∈r""x≠bu""x≠cv" using LeftRayX_def by auto then have C:"⟨x,SmallerOf(r,bu,cv)⟩∈r" using SmallerOf_def by (cases "⟨bu,cv⟩∈r", auto) from B have D:"x≠SmallerOf(r,bu,cv)" using SmallerOf_def by (cases "⟨bu,cv⟩∈r", auto) from B C D have "x∈LeftRayX(X,r,SmallerOf(r,bu,cv))" using LeftRayX_def by auto } then show "LeftRayX(X, r, bu) ∩ LeftRayX(X, r, cv) ⊆ LeftRayX(X, r, SmallerOf(r, bu, cv))" by auto { fix x assume "x∈LeftRayX(X, r, SmallerOf(r, bu, cv))" then have R:"x∈X""⟨x,SmallerOf(r,bu,cv)⟩∈r""x≠SmallerOf(r,bu,cv)" using LeftRayX_def by auto { { assume AS:"⟨bu,cv⟩∈r" then have "SmallerOf(r,bu,cv)=bu" using SmallerOf_def by auto then have "⟨x,bu⟩∈r" using R(2) by auto with AS have "⟨x,bu⟩∈r" "⟨x,cv⟩∈r" using assms IsLinOrder_def trans_def by(safe, blast) } moreover { assume AS:"⟨bu,cv⟩∉r" then have "SmallerOf(r,bu,cv)=cv" using SmallerOf_def by auto then have "⟨x,cv⟩∈r" using R(2) by auto from AS have "⟨cv,bu⟩∈r" using assms IsLinOrder_def IsTotal_def assms by auto with `⟨x,cv⟩∈r` have "⟨x,cv⟩∈r" "⟨x,bu⟩∈r" using assms IsLinOrder_def trans_def by(safe, blast) } ultimately have T:"⟨x,cv⟩∈r" "⟨x,bu⟩∈r" by auto moreover { assume AS:"x=bu" then have "⟨bu,cv⟩∈r" using T(1) by auto then have "SmallerOf(r,bu,cv)=bu" using SmallerOf_def assms IsLinOrder_def antisym_def by auto with `x≠SmallerOf(r,bu,cv)` have "False" using AS by auto } moreover { assume AS:"x=cv" then have "⟨cv,bu⟩∈r" using T(2) by auto then have "SmallerOf(r,bu,cv)=cv" using SmallerOf_def assms IsLinOrder_def antisym_def by auto with `x≠SmallerOf(r,bu,cv)` have "False" using AS by auto } ultimately have "⟨x,bu⟩∈r" "⟨x,cv⟩∈r""x≠bu""x≠cv" by auto } with `x∈X` have "x∈ LeftRayX(X, r, bu) ∩ LeftRayX(X, r, cv)" using LeftRayX_def by auto } then show "LeftRayX(X, r, SmallerOf(r, bu, cv)) ⊆ LeftRayX(X, r, bu) ∩ LeftRayX(X, r, cv) " by auto qed lemma inter_rray_rray: assumes "bu∈X""cv∈X""IsLinOrder(X,r)" shows "RightRayX(X,r,bu)∩RightRayX(X,r,cv)=RightRayX(X,r,GreaterOf(r,bu,cv))" proof { fix x assume "x∈RightRayX(X,r,bu)∩RightRayX(X,r,cv)" then have B:"x∈X""⟨bu,x⟩∈r""⟨cv,x⟩∈r""x≠bu""x≠cv" using RightRayX_def by auto then have C:"⟨GreaterOf(r,bu,cv),x⟩∈r" using GreaterOf_def by (cases "⟨bu,cv⟩∈r",auto) from B have D:"x≠GreaterOf(r,bu,cv)" using GreaterOf_def by (cases "⟨bu,cv⟩∈r",auto) from B C D have "x∈RightRayX(X,r,GreaterOf(r,bu,cv))" using RightRayX_def by auto } then show " RightRayX(X, r, bu) ∩ RightRayX(X, r, cv) ⊆ RightRayX(X, r, GreaterOf(r, bu, cv))" by auto { fix x assume "x∈RightRayX(X, r, GreaterOf(r, bu, cv))" then have R:"x∈X""⟨GreaterOf(r,bu,cv),x⟩∈r""x≠GreaterOf(r,bu,cv)" using RightRayX_def by auto { { assume AS:"⟨bu,cv⟩∈r" then have "GreaterOf(r,bu,cv)=cv" using GreaterOf_def by auto then have "⟨cv,x⟩∈r" using R(2) by auto with AS have "⟨bu,x⟩∈r" "⟨cv,x⟩∈r" using assms IsLinOrder_def trans_def by(safe, blast) } moreover { assume AS:"⟨bu,cv⟩∉r" then have "GreaterOf(r,bu,cv)=bu" using GreaterOf_def by auto then have "⟨bu,x⟩∈r" using R(2) by auto from AS have "⟨cv,bu⟩∈r" using assms IsLinOrder_def IsTotal_def assms by auto with `⟨bu,x⟩∈r` have "⟨cv,x⟩∈r" "⟨bu,x⟩∈r" using assms IsLinOrder_def trans_def by(safe, blast) } ultimately have T:"⟨cv,x⟩∈r" "⟨bu,x⟩∈r" by auto moreover { assume AS:"x=bu" then have "⟨cv,bu⟩∈r" using T(1) by auto then have "GreaterOf(r,bu,cv)=bu" using GreaterOf_def assms IsLinOrder_def antisym_def by auto with `x≠GreaterOf(r,bu,cv)` have "False" using AS by auto } moreover { assume AS:"x=cv" then have "⟨bu,cv⟩∈r" using T(2) by auto then have "GreaterOf(r,bu,cv)=cv" using GreaterOf_def assms IsLinOrder_def antisym_def by auto with `x≠GreaterOf(r,bu,cv)` have "False" using AS by auto } ultimately have "⟨bu,x⟩∈r" "⟨cv,x⟩∈r""x≠bu""x≠cv" by auto } with `x∈X` have "x∈ RightRayX(X, r, bu) ∩ RightRayX(X, r, cv) " using RightRayX_def by auto } then show "RightRayX(X, r, GreaterOf(r, bu, cv)) ⊆ RightRayX(X, r, bu) ∩ RightRayX(X, r, cv)" by auto qed text{*The open intervals and rays satisfy the base condition.*} lemma intervals_rays_base_condition: assumes "IsLinOrder(X,r)" shows "{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X} {satisfies the base condition}" proof- let ?I="{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}" let ?R="{RightRayX(X,r,b). b∈X}" let ?L="{LeftRayX(X,r,b). b∈X}" let ?B="{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X}" { fix U V assume A:"U∈?B""V∈?B" then have dU:"U∈?I∨U∈?L∨U∈?R"and dV:"V∈?I∨V∈?L∨V∈?R" by auto { assume S:"V∈?I" { assume "U∈?I" with S obtain bu cu bv cv where A:"U=IntervalX(X,r,bu,cu)""V=IntervalX(X,r,bv,cv)""bu∈X""cu∈X""bv∈X""cv∈X" by auto then have "SmallerOf(r,cu,cv)∈X""GreaterOf(r,bu,bv)∈X" by (cases "⟨cu,cv⟩∈r",simp add:SmallerOf_def A,simp add:SmallerOf_def A, cases "⟨bu,bv⟩∈r",simp add:GreaterOf_def A,simp add:GreaterOf_def A) with A have "U∩V∈?B" using inter_two_intervals assms by auto } moreover { assume "U∈?L" with S obtain bu bv cv where A:"U=LeftRayX(X, r,bu)""V=IntervalX(X,r,bv,cv)""bu∈X""bv∈X""cv∈X" by auto then have "SmallerOf(r,bu,cv)∈X" using SmallerOf_def by (cases "⟨bu,cv⟩∈r",auto) with A have "U∩V∈?B" using inter_lray_interval assms by auto } moreover { assume "U∈?R" with S obtain cu bv cv where A:"U=RightRayX(X,r,cu)""V=IntervalX(X,r,bv,cv)""cu∈X""bv∈X""cv∈X" by auto then have "GreaterOf(r,cu,bv)∈X" using GreaterOf_def by (cases "⟨cu,bv⟩∈r",auto) with A have "U∩V∈?B" using inter_rray_interval assms by auto } ultimately have "U∩V∈?B" using dU by auto } moreover { assume S:"V∈?L" { assume "U∈?I" with S obtain bu bv cv where A:"V=LeftRayX(X, r,bu)""U=IntervalX(X,r,bv,cv)""bu∈X""bv∈X""cv∈X" by auto then have "SmallerOf(r,bu,cv)∈X" using SmallerOf_def by (cases "⟨bu,cv⟩∈r", auto) have "U∩V=V∩U" by auto with A `SmallerOf(r,bu,cv)∈X` have "U∩V∈?B" using inter_lray_interval assms by auto } moreover { assume "U∈?R" with S obtain bu cv where A:"V=LeftRayX(X,r,bu)""U=RightRayX(X,r,cv)""bu∈X""cv∈X" by auto have "U∩V=V∩U" by auto with A have "U∩V∈?B" using inter_lray_rray assms by auto } moreover { assume "U∈?L" with S obtain bu bv where A:"U=LeftRayX(X,r,bu)""V=LeftRayX(X,r,bv)""bu∈X""bv∈X" by auto then have "SmallerOf(r,bu,bv)∈X" using SmallerOf_def by (cases "⟨bu,bv⟩∈r", auto) with A have "U∩V∈?B" using inter_lray_lray assms by auto } ultimately have "U∩V∈?B" using dU by auto } moreover { assume S:"V∈?R" { assume "U∈?I" with S obtain cu bv cv where A:"V=RightRayX(X,r,cu)""U=IntervalX(X,r,bv,cv)""cu∈X""bv∈X""cv∈X" by auto then have "GreaterOf(r,cu,bv)∈X" using GreaterOf_def by (cases "⟨cu,bv⟩∈r",auto) have "U∩V=V∩U" by auto with A `GreaterOf(r,cu,bv)∈X` have "U∩V∈?B" using inter_rray_interval assms by auto } moreover { assume "U∈?L" with S obtain bu cv where A:"U=LeftRayX(X,r,bu)""V=RightRayX(X,r,cv)""bu∈X""cv∈X" by auto then have "U∩V∈?B" using inter_lray_rray assms by auto } moreover { assume "U∈?R" with S obtain cu cv where A:"U=RightRayX(X,r,cu)""V=RightRayX(X,r,cv)""cu∈X""cv∈X" by auto then have "GreaterOf(r,cu,cv)∈X" using GreaterOf_def by (cases "⟨cu,cv⟩∈r",auto) with A have "U∩V∈?B" using inter_rray_rray assms by auto } ultimately have "U∩V∈?B" using dU by auto } ultimately have S:"U∩V∈?B" using dV by auto { fix x assume "x∈U∩V" then have "x∈U∩V∧U∩V⊆U∩V" by auto then have "∃W. W∈(?B)∧ x∈W ∧ W ⊆ U∩V" using S by blast then have "∃W∈(?B). x∈W ∧ W ⊆ U∩V" by blast } hence "(∀x ∈ U∩V. ∃W∈(?B). x∈W ∧ W ⊆ U∩V)" by auto } then show ?thesis using SatisfiesBaseCondition_def by auto qed text{*Since the intervals and rays form a base of a topology, and this topology is uniquely determined; we can built it. In the definition we have to make sure that we have a totally ordered set.*} definition OrderTopology ("OrdTopology _ _" 50) where "IsLinOrder(X,r) ⟹ OrdTopology X r ≡ TopologyBase {IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X}" theorem Ordtopology_is_a_topology: assumes "IsLinOrder(X,r)" shows "(OrdTopology X r) {is a topology}" and "{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X} {is a base for} (OrdTopology X r)" using assms Base_topology_is_a_topology intervals_rays_base_condition OrderTopology_def by auto lemma topology0_ordtopology: assumes "IsLinOrder(X,r)" shows "topology0(OrdTopology X r)" using Ordtopology_is_a_topology topology0_def assms by auto subsection{*Total set*} text{*The topology is defined in the set $X$, when $X$ has more than one point*} lemma union_ordtopology: assumes "IsLinOrder(X,r)""∃x y. x≠y ∧ x∈X∧ y∈X" shows "⋃(OrdTopology X r)=X" proof let ?B="{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X}" have base:"?B {is a base for} (OrdTopology X r)" using Ordtopology_is_a_topology(2) assms(1) by auto from assms(2) obtain x y where T:"x≠y ∧ x∈X∧ y∈X" by auto then have B:"x∈LeftRayX(X,r,y)∨x∈RightRayX(X,r,y)" using LeftRayX_def RightRayX_def assms(1) IsLinOrder_def IsTotal_def by auto then have "x∈⋃?B" using T by auto then have x:"x∈⋃(OrdTopology X r)" using Top_1_2_L5 base by auto { fix z assume z:"z∈X" { assume "x=z" then have "z∈⋃(OrdTopology X r)" using x by auto } moreover { assume "x≠z" with z T have "z∈LeftRayX(X,r,x)∨z∈RightRayX(X,r,x)""x∈X" using LeftRayX_def RightRayX_def assms(1) IsLinOrder_def IsTotal_def by auto then have "z∈⋃?B" by auto then have "z∈⋃(OrdTopology X r)" using Top_1_2_L5 base by auto } ultimately have "z∈⋃(OrdTopology X r)" by auto } then show "X⊆⋃(OrdTopology X r)" by auto have "⋃?B⊆X" using IntervalX_def LeftRayX_def RightRayX_def by auto then show "⋃(OrdTopology X r)⊆X" using Top_1_2_L5 base by auto qed text{*The interior, closure and boundary can be calculated using the formulas proved in the section that deals with the base.*} text{*The subspace of an order topology doesn't have to be an order topology.*} (*Note: Build a counter-example using the real numbers.*) subsection{*Right order and Left order topologies.*} text{*Notice that the left and right rays are closed under intersection, hence they form a base of a topology. They are called right order topology and left order topology respectively.*} text{*If the order in $X$ has a minimal or a maximal element, is necessary to consider $X$ as an element of the base or that limit point wouldn't be in any basic open set.*} subsubsection{*Right and Left Order topologies are topologies*} lemma leftrays_base_condition: assumes "IsLinOrder(X,r)" shows "{LeftRayX(X,r,b). b∈X}∪{X} {satisfies the base condition}" proof- { fix U V assume "U∈{LeftRayX(X,r,b). b∈X}∪{X}""V∈{LeftRayX(X,r,b). b∈X}∪{X}" then obtain b c where A:"(b∈X∧U=LeftRayX(X,r,b))∨U=X""(c∈X∧V=LeftRayX(X,r,c))∨V=X""U⊆X""V⊆X" unfolding LeftRayX_def by auto then have "(U∩V=LeftRayX(X,r,SmallerOf(r,b,c))∧b∈X∧c∈X)∨U∩V=X∨(U∩V=LeftRayX(X,r,c)∧c∈X)∨(U∩V=LeftRayX(X,r,b)∧b∈X)" using inter_lray_lray assms by auto moreover have "b∈X∧c∈X ⟶ SmallerOf(r,b,c)∈X" unfolding SmallerOf_def by (cases "⟨b,c⟩∈r",auto) ultimately have "U∩V∈{LeftRayX(X,r,b). b∈X}∪{X}" by auto hence "∀x∈U∩V. ∃W∈{LeftRayX(X,r,b). b∈X}∪{X}. x∈W∧W⊆U∩V" by blast } moreover then show ?thesis using SatisfiesBaseCondition_def by auto qed lemma rightrays_base_condition: assumes "IsLinOrder(X,r)" shows "{RightRayX(X,r,b). b∈X}∪{X} {satisfies the base condition}" proof- { fix U V assume "U∈{RightRayX(X,r,b). b∈X}∪{X}""V∈{RightRayX(X,r,b). b∈X}∪{X}" then obtain b c where A:"(b∈X∧U=RightRayX(X,r,b))∨U=X""(c∈X∧V=RightRayX(X,r,c))∨V=X""U⊆X""V⊆X" unfolding RightRayX_def by auto then have "(U∩V=RightRayX(X,r,GreaterOf(r,b,c))∧b∈X∧c∈X)∨U∩V=X∨(U∩V=RightRayX(X,r,c)∧c∈X)∨(U∩V=RightRayX(X,r,b)∧b∈X)" using inter_rray_rray assms by auto moreover have "b∈X∧c∈X ⟶ GreaterOf(r,b,c)∈X" using GreaterOf_def by (cases "⟨b,c⟩∈r",auto) ultimately have "U∩V∈{RightRayX(X,r,b). b∈X}∪{X}" by auto hence "∀x∈U∩V. ∃W∈{RightRayX(X,r,b). b∈X}∪{X}. x∈W∧W⊆U∩V" by blast } then show ?thesis using SatisfiesBaseCondition_def by auto qed definition LeftOrderTopology ("LOrdTopology _ _" 50) where "IsLinOrder(X,r) ⟹ LOrdTopology X r ≡ TopologyBase {LeftRayX(X,r,b). b∈X}∪{X}" definition RightOrderTopology ("ROrdTopology _ _" 50) where "IsLinOrder(X,r) ⟹ ROrdTopology X r ≡ TopologyBase {RightRayX(X,r,b). b∈X}∪{X}" theorem LOrdtopology_ROrdtopology_are_topologies: assumes "IsLinOrder(X,r)" shows "(LOrdTopology X r) {is a topology}" and "{LeftRayX(X,r,b). b∈X}∪{X} {is a base for} (LOrdTopology X r)" and "(ROrdTopology X r) {is a topology}" and "{RightRayX(X,r,b). b∈X}∪{X} {is a base for} (ROrdTopology X r)" using Base_topology_is_a_topology leftrays_base_condition assms rightrays_base_condition LeftOrderTopology_def RightOrderTopology_def by auto lemma topology0_lordtopology_rordtopology: assumes "IsLinOrder(X,r)" shows "topology0(LOrdTopology X r)" and "topology0(ROrdTopology X r)" using LOrdtopology_ROrdtopology_are_topologies topology0_def assms by auto subsubsection{*Total set*} text{*The topology is defined on the set $X$*} lemma union_lordtopology_rordtopology: assumes "IsLinOrder(X,r)" shows "⋃(LOrdTopology X r)=X" and "⋃(ROrdTopology X r)=X" using Top_1_2_L5[OF LOrdtopology_ROrdtopology_are_topologies(2)[OF assms]] Top_1_2_L5[OF LOrdtopology_ROrdtopology_are_topologies(4)[OF assms]] unfolding LeftRayX_def RightRayX_def by auto section{*Union of Topologies*} text{*The union of two topologies is not a topology. A way to overcome this fact is to define the following topology: *} definition joinT ("joinT _" 90) where "(∀T∈M. T{is a topology} ∧ (∀Q∈M. ⋃Q=⋃T)) ⟹ (joinT M ≡ THE T. (⋃M){is a subbase for} T)" text{*First let's proof that given a family of sets, then it is a subbase for a topology.*} text{* The first result states that from any family of sets we get a base using finite intersections of them. The second one states that any family of sets is a subbase of some topology.*} theorem subset_as_subbase: shows "{⋂A. A ∈ FinPow(B)} {satisfies the base condition}" proof- { fix U V assume A:"U∈{⋂A. A ∈ FinPow(B)} ∧ V∈{⋂A. A ∈ FinPow(B)}" then obtain M R where MR:"Finite(M)""Finite(R)""M⊆B""R⊆B" "U=⋂M""V=⋂R" using FinPow_def by auto { fix x assume AS:"x∈U∩V" then have N:"M≠0""R≠0" using MR(5,6) by auto have "Finite(M ∪R)" using MR(1,2) by auto moreover have "M ∪ R∈Pow(B)" using MR(3,4) by auto ultimately have "M∪R∈FinPow(B)" using FinPow_def by auto then have "⋂(M∪R)∈{⋂A. A ∈ FinPow(B)}" by auto moreover from N have "⋂(M∪R)⊆⋂M""⋂(M∪R)⊆⋂R" by auto then have "⋂(M∪R)⊆U∩V" using MR(5,6) by auto moreover { fix S assume "S∈M ∪ R" then have "S∈M∨S∈R" by auto then have "x∈S" using AS MR(5,6) by auto } then have "x∈⋂(M ∪ R)" using N by auto ultimately have "∃W∈{⋂A. A ∈ FinPow(B)}. x∈W∧W⊆U∩V" by blast } then have "(∀x ∈ U∩V. ∃W∈{⋂A. A ∈ FinPow(B)}. x∈W ∧ W ⊆ U∩V)" by auto } then have "∀U V. ((U∈{⋂A. A ∈ FinPow(B)} ∧ V∈{⋂A. A ∈ FinPow(B)}) ⟶ (∀x ∈ U∩V. ∃W∈{⋂A. A ∈ FinPow(B)}. x∈W ∧ W ⊆ U∩V))" by auto then show "{⋂A. A ∈ FinPow(B)} {satisfies the base condition}" using SatisfiesBaseCondition_def by auto qed theorem Top_subbase: assumes "T = {⋃A. A∈Pow({⋂A. A ∈ FinPow(B)})}" shows "T {is a topology}" and "B {is a subbase for} T" proof- { fix S assume "S∈B" then have "{S}∈FinPow(B)""⋂{S}=S" using FinPow_def by auto then have "{S}∈Pow({⋂A. A ∈ FinPow(B)})" by (blast+) then have "⋃{S}∈{⋃A. A∈Pow({⋂A. A ∈ FinPow(B)})}" by blast then have "S∈{⋃A. A∈Pow({⋂A. A ∈ FinPow(B)})}" by auto then have "S∈T" using assms by auto } then have "B⊆T" by auto moreover have "{⋂A. A ∈ FinPow(B)} {satisfies the base condition}" using subset_as_subbase by auto then have "T {is a topology}" and "{⋂A. A ∈ FinPow(B)} {is a base for} T" using Top_1_2_T1 assms by auto ultimately show "T {is a topology}" and "B{is a subbase for}T" using IsAsubBaseFor_def by auto qed text{*A subbase defines a unique topology.*} theorem same_subbase_same_top: assumes "B {is a subbase for} T" and "B {is a subbase for} S" shows "T = S" using IsAsubBaseFor_def assms same_base_same_top by auto end