Theory Topology_ZF_examples_1

(* 
    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 More examples in topology

theory Topology_ZF_examples_1
imports Topology_ZF_1 Order_ZF
begin

textIn 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.

subsectionNew ideas using a base for a topology

subsectionThe topology of a base

textGiven a family of subsets satisfying the base condition,
  it is possible to construct a topology where that family is a base of. 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"

text If a collection $U$ of sets satisfies the base condition then the topology
  constructed from it is indeed a topology and $U$ is a base for this topology. 

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

textA 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""QPow(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""QPow(B-{0})" by auto
    hence "M=(Q)""QPow(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

textThe 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) = {TU. TA}"
proof
  have "{TU. TA}U" by auto
  with assms(1) have "{TU. TA}T"
    using IsAbaseFor_def by auto
  moreover have "{TU. TA}  A" by blast
  ultimately show  "{TU. TA}  Interior(A,T)"
    using assms(2) topology0.Top_2_L5 topology0_def by auto
  {
    fix x
    assume "x  Interior(A,T)"
    with assms obtain V where "VU" "V  Interior(A,T)" "xV"
      using point_open_base_neigh topology0.Top_2_L2 topology0_def 
      by blast
    with assms have "VU" "xV" "VA" using topology0.Top_2_L1 topology0_def
      by auto  
    hence "x  {TU. TA}" by auto
  }
  thus "Interior(A, T)  {T  U . T  A} " by auto
qed

textIn the following, we offer another lemma about the closure of a set 
  given a basis for a topology. This lemma is based on cl_inter_neigh› and 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}" "AQ"
  shows "Closure(A,Q) = {xQ. TU. xTAT0}"
proof
  {
    fix x
    assume A:"xClosure(A,Q)"
    with assms(2,3) have B:"xQ" using topology0_def topology0.Top_3_L11(1)
      by blast
    moreover
    {
      fix T
      assume "TU" "xT"
      with assms(1) have "TQ""xT" using base_sets_open by auto
      with assms(2,3) A have "AT  0" using topology0_def topology0.cl_inter_neigh
        by auto
    }
    hence "TU. xTAT0" by auto
    ultimately have "x{xQ. TU. xTAT0}" by auto
  }
  thus "Closure(A, Q) {xQ. TU. xTAT0}"
    by auto
  {                     
    fix x
    assume AS:"x{x  Q . TU. x  T  A  T  0}"
    hence "xQ" by blast
    moreover
    {
      fix R
      assume "RQ"                     
      with assms(1) obtain W where RR:"WU" "R=W" using
        IsAbaseFor_def by auto
      {
        assume "xR"
        with RR(2) obtain WW where TT:"WWW""xWW" by auto
        {
          assume "RA=0"
          with RR(2) TT(1) have "WWA=0"  by auto
           with TT(1) RR(1) have "WWU" "WWA=0" by auto
          with AS have "xQ-WW" by auto
          with TT(2) have "False" by auto
        }
        hence "RA0" by auto
      }
    }
    hence "UQ. xU  UA0" by auto
    ultimately have "xClosure(A,Q)" using assms(2,3) topology0_def topology0.inter_neigh_cl 
      by auto
  }
  then show "{x  Q . TU. x  T  A  T  0}  Closure(A,Q)"
    by auto
qed

textThe 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 -
  from assms have "(B {restricted to} Y)  (T {restricted to} Y)"
    unfolding IsAbaseFor_def RestrictedTo_def by auto 
  moreover have "(T {restricted to} Y) = {A. A  Pow(B {restricted to} Y)}"
  proof
    { fix U assume "U  (T {restricted to} Y)"
      then obtain W where "WT" and "U = WY" unfolding RestrictedTo_def by blast
      with assms obtain C where "CPow(B)" and "W=C" unfolding IsAbaseFor_def
        by blast
      let ?A="{VY. VC}"
      from CPow(B) U = WY W=C have 
        "?A  Pow(B {restricted to} Y)" and "U=(?A)" 
        unfolding RestrictedTo_def by auto 
      hence "U  {A. A  Pow(B {restricted to} Y)}" by blast 
    } thus "(T {restricted to} Y)  {A. A  Pow(B {restricted to} Y)}"
      by auto
    { fix U assume "U  {A. A  Pow(B {restricted to} Y)}"
      then obtain A where A: "A  (B {restricted to} Y)" and "U = (A)" by auto
      let ?A0="{CB. YCA}"
      from A have "?A0  B" and "A = ?A0 {restricted to} Y" unfolding RestrictedTo_def
        by auto 
      with U = (A) have "?A0  B" and "U = (?A0 {restricted to} Y)" 
        by auto
      with assms have "U  (T {restricted to} Y)" unfolding RestrictedTo_def IsAbaseFor_def
        by auto
    } thus "{A. A  Pow(B {restricted to} Y)}  (T {restricted to} Y)" by blast 
  qed
  ultimately show ?thesis unfolding IsAbaseFor_def by simp 
qed

textIf 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""BB2"
  shows "TT2"
proof
  {
    fix x
    assume "xT"
    with assms(1) obtain M where "MB""x=M" using IsAbaseFor_def by auto
    with assms(3) have "MB2""x=M" by auto
    with assms(2) show "xT2" using IsAbaseFor_def by auto
  }
qed

subsectionDual Base for Closed Sets

textA 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. UB}{T}"


lemma closed_inter_dual_base:
  assumes "D{is closed in}T""B{is a base for}T"
  obtains M where "MDualBase B T""D=M"
proof-
  assume K:"M. M  DualBase B T  D = M  thesis"
  {
    assume AS:"DT"
    from assms(1) have D:"DPow(T)""T-DT" using IsClosed_def by auto
    hence A:"T-(T-D)=D""T-DT" by auto
    with assms(2) obtain Q where QQ:"QPow(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:"Q0" by auto
    from QQ(2) A(1) have "D=T-Q" by auto
    with QNN have "D={T-R. RQ}" by auto
    moreover
    with assms(2) QQ(1) have "{T-R. RQ}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

textWe 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}""AQ"
  shows "Closure(A,Q)={TDualBase U Q. AT}"
proof
  from assms(1) have T:"QDualBase U Q" using DualBase_def by auto
  moreover
  {
    fix T
    assume A:"TDualBase U Q" "AT"
    with assms(1) obtain R where "(T=Q-RRU)T=Q" using DualBase_def
      by auto
    with A(2) assms(1,2) have  "(T{is closed in}Q)""AT""TPow(Q)" using topology0.Top_3_L1 topology0_def
      topology0.Top_3_L9 base_sets_open by auto
  }
  then have SUB:"{TDualBase U Q. AT}{TPow(Q). (T{is closed in}Q)AT}"
    by blast
  with calculation assms(3) have "{TPow(Q). (T{is closed in}Q)AT}{TDualBase U Q. AT}"
    by auto
  then show "Closure(A,Q){TDualBase U Q. AT}" using Closure_def ClosedCovers_def
    by auto
  {
    fix x
    assume A:"x{TDualBase U Q. AT}"
    {
      fix T
      assume B:"xT""TU"
      {
        assume C:"AT=0"
        from B(2) assms(1) have "Q-TDualBase U Q" using DualBase_def
          by auto
        moreover
        from C assms(3) have "AQ-T" by auto
        moreover
        from B(1) have "xQ-T" by auto
        ultimately have "x{TDualBase U Q. AT}" by auto
        with A have "False" by auto
      }
      hence "AT0" by auto
    }
    hence "TU. xTAT0" by auto
    moreover
    from T A assms(3) have "xQ" by auto
    with calculation assms have "xClosure(A,Q)" using closure_set_base_topology
     by auto
  }
  thus "{T  DualBase U Q . A  T}  Closure(A, Q)" by auto
qed

subsectionPartition topology

textIn 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  (AU. BU. A=B AB=0) 0U)"

textA subcollection of a partition is a partition
of its union.

lemma subpartition:
  assumes "U {is a partition of} X" "VU"
  shows "V{is a partition of}V" 
  using assms unfolding IsAPartition_def by auto

textA 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} (XY)"
  using assms unfolding IsAPartition_def RestrictedTo_def
  by fast

textGiven a partition, 
the complement of a union of a subfamily
is a union of a subfamily.

lemma diff_union_is_union_diff:
  assumes "RP" "P {is a partition of} X"
  shows "X - R=(P-R)"
proof
  {
    fix x
    assume "xX - R"
    hence P:"xX""xR" by auto
    {
      fix T
      assume "TR"
      with P(2) have "xT" by auto
    }
    with P(1) assms(2) obtain Q where "Q(P-R)""xQ" 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 "QP-R""xQ" by auto
    hence C: "QP""QR""xQ" by auto
    then have "xP" by auto
    with assms(2) have "xX" using IsAPartition_def by auto
    moreover
    {
      assume "xR"
      then obtain t where G:"tR" "xt" by auto
      with C(3) assms(1) have "tQ0""tP" 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 "xR" by auto
    ultimately have "xX-R" by auto
  }
  thus "(P-R)X - R" by auto
qed

subsectionPartition topology is a topology.

textA 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:"UPVP"
    with assms have A:"U=V UV=0" using IsAPartition_def by auto
    {
      fix x
      assume ASS:"xUV"
      with A have "U=V" by auto
      with AS ASS have "UP""xU UUV" by auto
      hence "WP. xW WUV" by auto
    }
    hence "(x  UV. WP. xW  W  UV)" by auto
  }
  then show ?thesis using SatisfiesBaseCondition_def by auto
qed

textSince 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

subsectionTotal set, Closed sets, Interior, Closure and Boundary

textThe 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

textThe 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:"DPow(X)""X-D(PTopology X T)"
      using IsClosed_def union_ptopology by auto
    from A(2) B obtain R where Q:"RT" "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:"RT""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 "DT" by auto
    with assms have "DX" using IsAPartition_def by auto
    with calculation assms show "D{is closed in} (PTopology X T)"
      using IsClosed_def union_ptopology by auto
  }
qed

textThere 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""AX"
  shows "Interior(A,(PTopology X U))={TDualBase U (PTopology X U). T=XTAX}"
proof
  {
    fix x
    assume "xInterior(A,(PTopology X U))"
    with assms obtain R where A:"xR""R(PTopology X U)""RA"
      using topology0.open_open_neigh topology0_ptopology
      topology0.Top_2_L2 topology0.Top_2_L1
      by auto
    with assms obtain B where B:"BU""R=B" using Ptopology_is_a_topology(2)
      IsAbaseFor_def by auto
    from A(1,3) assms have XX:"xX""X{TDualBase U (PTopology X U). T=XTAX}"
      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:"SB""xS" by auto
    {
      fix T
      assume AS:"TDualBase U (PTopology X U)""T AX"
      from AS(1) assms obtain w where "(T=X-wwU)(T=X)"
        using DualBase_def union_ptopology Ptopology_is_a_topology(2)
        by auto
      with assms(2) AS(2) have D:"T=X-w""wU" by auto
      from D(2) have "wU" 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 "wX" using union_ptopology by auto
      with D(1) have "X-T=w" by auto
      with D(2) have "X-TU" by auto
      { 
        assume "xX-T"
        with C B(1) have "SU""S(X-T)0" by auto
        with X-TU assms(1) have "X-T=S" using IsAPartition_def by auto
        with X-T=wT=X-w have "X-S=T" by auto
        with AS(2) have "X-SAX" by auto
        from A(3) B(2) C(1) have "SA" by auto
        hence "X-AX-S" by auto
        with assms(2) have "X-SA=X"  by auto
        with X-SAX have "False" by auto
        }
      then have "xT" using XX by auto
      }
    ultimately have "x{TDualBase U (PTopology X U). T=XTAX}"
      by auto
  }
  thus "Interior(A,(PTopology X U)){TDualBase U (PTopology X U). T=XTAX}" by auto
  {
    fix x
    assume p:"x{TDualBase U (PTopology X U). T=XTAX}"
    hence noE:"{TDualBase U (PTopology X U). T=XTAX}0" by auto
    {
      fix T
      assume "TDualBase U (PTopology X U)"
      with assms(1) obtain w where "T=X(wUT=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{TDualBase U (PTopology X U). T=XTAX}"and X:"xX" using Ptopology_is_a_topology(2) 
      DualBase_def union_ptopology by auto
    with calculation assms(1) have "({TDualBase U (PTopology X U). T=XTAX}) {is closed in}(PTopology X U)"
      using topology0.Top_3_L4[where K="{TDualBase U (PTopology X U). T=XTAX}"] topology0_ptopology[where U="U" and X="X"]
      by auto
    with assms(1) have ab:"({TDualBase U (PTopology X U). T=XTAX})(PTopology X U)"
      using closed_sets_ptopology by auto
    with assms(1) obtain B where "BPow(U)""({TDualBase U (PTopology X U). T=XTAX})=B"
      using Ptopology_is_a_topology(2) IsAbaseFor_def by auto
    with p obtain R where "xR""RU""R({TDualBase U (PTopology X U). T=XTAX})"
      by auto
    with assms(1) have R:"xR""R(PTopology X U)""R({TDualBase U (PTopology X U). T=XTAX})""X-RDualBase 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) AX"
      with R(4) have "X-R{TDualBase U (PTopology X U). T=XTAX}" by auto
      hence "{TDualBase U (PTopology X U). T=XTAX}X-R" by auto
      with R(3) have "RX-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:"yR"
      with R(2) have "y(PTopology X U)" by auto
      with assms(1) have XX:"yX" using union_ptopology by auto
      with I have "y(X-R) A" by auto
      with XX have "yRyA" by auto
      with ASR have "yA" by auto
    }
    hence "RA" by auto
    with R(1,2) have "R(PTopology X U). (xRRA)" by auto
    with assms(1) have "xInterior(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


textThe closure of a set is the union of
all the sets of the partition which intersect
with A›.

lemma closure_set_ptopology:
  assumes "U {is a partition of} X""AX"
  shows "Closure(A,(PTopology X U))={TU. TA0}"
proof
  {
    fix x
    assume A:"xClosure(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 "xU" 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:"xW""WU" by auto
    with A have "xClosure(A,(PTopology X U))W" by auto
    moreover
    from assms B(2) have "W(PTopology X U)""AX" using base_sets_open Ptopology_is_a_topology(2)
      by (safe,blast)
    with calculation assms(1) have "AW0" using topology0_ptopology[where U="U" and X="X"]
      topology0.cl_inter_neigh union_ptopology by auto
    with B have "x{TU. TA0}" 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:"xT""TU""TA0" 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)""xQ"
      with assms(1) obtain M where C:"Q=M""MU" using 
        Ptopology_is_a_topology(2)
        IsAbaseFor_def by auto
      from B(2) C(1) obtain R where D:"RM""xR" by auto
      with C(2) A(1,2) have "RT0""RU""TU" by auto
      with assms(1) have "R=T" using IsAPartition_def by auto
      with C(1) D(1) have "TQ" by auto
      with A(3) have "QA0" by auto
    }
    then have "Q(PTopology X U). xQ  QA0" by auto
    with calculation assms(1) have "xClosure(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

textThe 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""AX"
  shows "Boundary(A,(PTopology X U))={TU. TA0  ~(TA)}"
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 "TU""TA"
    with assms(1) have "TA=T""T0" using IsAPartition_def by auto
    with TU have "TA0""TU" 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  ~(TA)})" by blast
  with calculation A show ?thesis by auto
qed

subsectionSpecial cases and subspaces

textThe discrete and the indiscrete topologies appear as special
cases of this partition topologies.

lemma discrete_partition:
  shows "{{x}.xX} {is a partition of}X"
  using IsAPartition_def by auto

lemma indiscrete_partition:
  assumes "X0"
  shows "{X} {is a partition of} X"
  using assms IsAPartition_def by auto

theorem discrete_ptopology:
  shows "(PTopology X {{x}.xX})=Pow(X)"
proof
  {
    fix t
    assume "t(PTopology X {{x}.xX})"
    hence "t(PTopology X {{x}.xX})" by auto
    then have "tPow(X)" using union_ptopology 
      discrete_partition by auto
  }
  thus "(PTopology X {{x}.xX})Pow(X)" by auto
  {
    fix t
    assume A:"tPow(X)"
    have "({{x}. xt})=t" by auto
    moreover
    from A have "{{x}. xt}Pow({{x}.xX})" by auto
    hence "({{x}. xt}){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 "X0"
  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=0T=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

textThe topological subspaces of the (PTopology X U)›
are partition topologies.

lemma subspace_ptopology:
  assumes "U{is a partition of}X"
  shows "(PTopology X U) {restricted to} Y=(PTopology (XY) ((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} (XY)"
    using restriction_partition by auto
  then have "((U{restricted to} Y)-{0}){is a base for}(PTopology (XY) ((U {restricted to} Y)-{0}))"
    using Ptopology_is_a_topology(2) by auto
  ultimately show ?thesis using same_base_same_top by auto
qed

subsectionOrder topologies

subsectionOrder topology is a topology

textGiven 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 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){cX. c,br}-{b}"
definition
  RightRayX where
  "RightRayX(X,r,b){cX. b,cr}-{b}"

textIntersections of intervals and rays.

lemma inter_two_intervals:
  assumes "buX""bvX""cuX""cvX""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,bvr",simp,simp,cases "cu,cvr",simp,simp)
  {
    fix x
    assume ASS:"xIntervalX(X,r,bu,cu)IntervalX(X,r,bv,cv)"
    then have "xIntervalX(X,r,bu,cu)""xIntervalX(X,r,bv,cv)" by auto
    then have BB:"xX""xInterval(r,bu,cu)""xbu""xcu""xInterval(r,bv,cv)""xbv""xcv"
    using IntervalX_def assms by auto
    then have "xX" by auto
    moreover
    have "xGreaterOf(r,bu,bv)""xSmallerOf(r,cu,cv)"
    proof-
      show "xGreaterOf(r,bu,bv)" using GreaterOf_def BB(6,3) by (cases "bu,bvr",simp+)
      show "xSmallerOf(r,cu,cv)" using SmallerOf_def BB(7,4) by (cases "cu,cvr",simp+)
    qed
    moreover
    have "bu,xr""x,cur""bv,xr""x,cvr" using BB(2,5) Order_ZF_2_L1A by auto
    then have "GreaterOf(r,bu,bv),xr""x,SmallerOf(r,cu,cv)r" using GreaterOf_def SmallerOf_def 
      by (cases "bu,bvr",simp,simp,cases "cu,cvr",simp,simp)
    then have "xInterval(r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv))" using Order_ZF_2_L1 by auto
    ultimately
    have "xIntervalX(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 "xIntervalX(X,r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv))"
    then have BB:"xX""xInterval(r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv))""xGreaterOf(r,bu,bv)""xSmallerOf(r,cu,cv)"
    using IntervalX_def T by auto
    then have "xX" by auto
    moreover
    from BB(2) have CC:"GreaterOf(r,bu,bv),xr""x,SmallerOf(r,cu,cv)r" using Order_ZF_2_L1A by auto
    {
      {
        assume AS:"bu,bvr"
        then have "GreaterOf(r,bu,bv)=bv" using GreaterOf_def by auto
        then have "bv,xr" using CC(1) by auto
        with AS have "bu,xr" "bv,xr" using assms IsLinOrder_def trans_def by (safe, blast)
      }
      moreover
      {
        assume AS:"bu,bvr"
        then have "GreaterOf(r,bu,bv)=bu" using GreaterOf_def by auto
        then have "bu,xr" using CC(1) by auto
        from AS have "bv,bur" using assms IsLinOrder_def IsTotal_def assms by auto
        with bu,xr have "bu,xr" "bv,xr" using assms IsLinOrder_def trans_def by (safe, blast)
      }
      ultimately have R:"bu,xr" "bv,xr" by auto
      moreover
      {
        assume AS:"x=bu"
        then have "bv,bur" 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,bvr" 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,xr" "bv,xr""xbu""xbv" by auto
    }
    moreover
    {
      {
        assume AS:"cu,cvr"
        then have "SmallerOf(r,cu,cv)=cu" using SmallerOf_def by auto
        then have "x,cur" using CC(2) by auto
        with AS have "x,cur" "x,cvr" using assms IsLinOrder_def trans_def by(safe ,blast)
      }
      moreover
      {
        assume AS:"cu,cvr"
        then have "SmallerOf(r,cu,cv)=cv" using SmallerOf_def by auto
        then have "x,cvr" using CC(2) by auto
        from AS have "cv,cur" using assms IsLinOrder_def IsTotal_def by auto
        with x,cvr have "x,cvr" "x,cur" using assms IsLinOrder_def trans_def by(safe ,blast)
      }
      ultimately have R:"x,cvr" "x,cur" by auto
      moreover
      {
        assume AS:"x=cv"
        then have "cv,cur" 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,cvr" 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,cur" "x,cvr""xcu""xcv" by auto
    }
    ultimately
    have "xIntervalX(X,r,bu,cu)" "xIntervalX(X,r,bv,cv)" using Order_ZF_2_L1 IntervalX_def
      assms by auto
    then have "xIntervalX(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 "bvX""buX""cvX""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 "xRightRayX(X,r,bu)IntervalX(X,r,bv,cv)"
    then have "xRightRayX(X,r,bu)""xIntervalX(X,r,bv,cv)" by auto
    then have BB:"xX""xbu""xbv""xcv""bu,xr""xInterval(r,bv,cv)" using RightRayX_def IntervalX_def
      by auto
    then have "bv,xr""x,cvr" using Order_ZF_2_L1A by auto
    with bu,xr have "GreaterOf(r,bu,bv),xr" using GreaterOf_def by (cases "bu,bvr",simp+)
    with x,cvr have "xInterval(r,GreaterOf(r,bu,bv),cv)" using Order_ZF_2_L1 by auto
    then have "xIntervalX(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 "xIntervalX(X, r, GreaterOf(r, bu, bv), cv)"
    then have "xX""xInterval(r,GreaterOf(r, bu, bv), cv)""xcv""xGreaterOf(r, bu, bv)" using IntervalX_def by auto
    then have R:"GreaterOf(r, bu, bv),xr""x,cvr" using Order_ZF_2_L1A by auto
    with xcv have "x,cvr""xcv" by auto
    moreover
    {
      {
        assume AS:"bu,bvr"
        then have "GreaterOf(r,bu,bv)=bv" using GreaterOf_def by auto
        then have "bv,xr" using R(1) by auto
        with AS have "bu,xr" "bv,xr" using assms unfolding IsLinOrder_def trans_def by (safe,blast)
      }
      moreover
      {
        assume AS:"bu,bvr"
        then have "GreaterOf(r,bu,bv)=bu" using GreaterOf_def by auto
        then have "bu,xr" using R(1) by auto
        from AS have "bv,bur" using assms unfolding IsLinOrder_def IsTotal_def using assms by auto
        with bu,xr have "bu,xr" "bv,xr" using assms unfolding IsLinOrder_def trans_def  by (safe,blast)
      }
      ultimately have T:"bu,xr" "bv,xr" by auto
      moreover
      {
        assume AS:"x=bu"
        then have "bv,bur" 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 xGreaterOf(r,bu,bv) have "False" using AS by auto
      }
      moreover
      {
        assume AS:"x=bv"
        then have "bu,bvr" using T(1) by auto
        then have "GreaterOf(r,bu,bv)=bv" unfolding GreaterOf_def by auto
        with xGreaterOf(r,bu,bv) have "False" using AS by auto
      }
      ultimately have "bu,xr" "bv,xr""xbu""xbv" by auto
    }
    with calculation xX have "xRightRayX(X, r, bu)""xIntervalX(X, r, bv, cv)" unfolding RightRayX_def IntervalX_def
      using Order_ZF_2_L1 by auto
    then have "xRightRayX(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 "bvX""cuX""cvX""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 "xLeftRayX(X,r,cu)IntervalX(X,r,bv,cv)"
    then have B:"xcu""xX""x,cur""bv,xr""x,cvr""xbv""xcv" unfolding LeftRayX_def IntervalX_def Interval_def
      by auto
    from x,cur x,cvr have C:"x,SmallerOf(r, cu, cv)r" using SmallerOf_def by (cases "cu,cvr",simp+)
    from B(7,1) have "xSmallerOf(r,cu,cv)" using SmallerOf_def by (cases "cu,cvr",simp+)
    then have "xIntervalX(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 "xIntervalX(X,r,bv,SmallerOf(r,cu,cv))"
    then have R:"xX""bv,xr""x,SmallerOf(r,cu,cv)r""xbv""xSmallerOf(r,cu,cv)" using IntervalX_def Interval_def
      by auto
    then have "bv,xr""xbv" by auto
    moreover
    {
      {
        assume AS:"cu,cvr"
        then have "SmallerOf(r,cu,cv)=cu" using SmallerOf_def by auto
        then have "x,cur" using R(3) by auto
        with AS have "x,cur" "x,cvr" using assms unfolding IsLinOrder_def trans_def by (safe, blast)
      }
      moreover
      {
        assume AS:"cu,cvr"
        then have "SmallerOf(r,cu,cv)=cv" using SmallerOf_def by auto
        then have "x,cvr" using R(3) by auto
        from AS have "cv,cur" using assms IsLinOrder_def IsTotal_def assms by auto
        with x,cvr have "x,cvr" "x,cur" using assms IsLinOrder_def trans_def by (safe, blast)
      }
      ultimately have T:"x,cvr" "x,cur" by auto
      moreover
      {
        assume AS:"x=cu"
        then have "cu,cvr" using T(1) by auto
        then have "SmallerOf(r,cu,cv)=cu" using SmallerOf_def assms IsLinOrder_def
          antisym_def by auto
        with xSmallerOf(r,cu,cv) have "False" using AS by auto
      }
      moreover
      {
        assume AS:"x=cv"
        then have "cv,cur" using T(2) by auto
        then have "SmallerOf(r,cu,cv)=cv" using SmallerOf_def assms IsLinOrder_def
        antisym_def by auto
        with xSmallerOf(r,cu,cv) have "False" using AS by auto
      }
      ultimately have "x,cur" "x,cvr""xcu""xcv" by auto
    }
    with calculation xX have "xLeftRayX(X,r,cu)""xIntervalX(X, r, bv, cv)" using LeftRayX_def IntervalX_def Interval_def
      by auto
    then have "xLeftRayX(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 "buX""cvX""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 "buX""cvX""IsLinOrder(X,r)"
  shows "LeftRayX(X,r,bu)LeftRayX(X,r,cv)=LeftRayX(X,r,SmallerOf(r,bu,cv))"
proof
  {
    fix x
    assume "xLeftRayX(X,r,bu)LeftRayX(X,r,cv)"
    then have B:"xX""x,bur""x,cvr""xbu""xcv" using LeftRayX_def by auto
    then have C:"x,SmallerOf(r,bu,cv)r" using SmallerOf_def by (cases "bu,cvr", auto)
    from B have D:"xSmallerOf(r,bu,cv)" using SmallerOf_def by (cases "bu,cvr", auto)
    from B C D have "xLeftRayX(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 "xLeftRayX(X, r, SmallerOf(r, bu, cv))"
    then have R:"xX""x,SmallerOf(r,bu,cv)r""xSmallerOf(r,bu,cv)" using LeftRayX_def by auto
    {
      {
        assume AS:"bu,cvr"
        then have "SmallerOf(r,bu,cv)=bu" using SmallerOf_def by auto
        then have "x,bur" using R(2) by auto
        with AS have "x,bur" "x,cvr" using assms IsLinOrder_def trans_def by(safe, blast)
      }
      moreover
      {
        assume AS:"bu,cvr"
        then have "SmallerOf(r,bu,cv)=cv" using SmallerOf_def by auto
        then have "x,cvr" using R(2) by auto
        from AS have "cv,bur" using assms IsLinOrder_def IsTotal_def assms by auto
        with x,cvr have "x,cvr" "x,bur" using assms IsLinOrder_def trans_def by(safe, blast)
      }
      ultimately have T:"x,cvr" "x,bur" by auto
      moreover
      {
        assume AS:"x=bu"
        then have "bu,cvr" using T(1) by auto
        then have "SmallerOf(r,bu,cv)=bu" using SmallerOf_def assms IsLinOrder_def
          antisym_def by auto
        with xSmallerOf(r,bu,cv) have "False" using AS by auto
      }
      moreover
      {
        assume AS:"x=cv"
        then have "cv,bur" using T(2) by auto
        then have "SmallerOf(r,bu,cv)=cv" using SmallerOf_def assms IsLinOrder_def
          antisym_def by auto
        with xSmallerOf(r,bu,cv) have "False" using AS by auto
      }
      ultimately have "x,bur" "x,cvr""xbu""xcv" by auto
    }
    with xX 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 "buX""cvX""IsLinOrder(X,r)"
  shows "RightRayX(X,r,bu)RightRayX(X,r,cv)=RightRayX(X,r,GreaterOf(r,bu,cv))"
proof
  {
    fix x
    assume "xRightRayX(X,r,bu)RightRayX(X,r,cv)"
    then have B:"xX""bu,xr""cv,xr""xbu""xcv" using RightRayX_def by auto
    then have C:"GreaterOf(r,bu,cv),xr" using GreaterOf_def by (cases "bu,cvr",auto)
    from B have D:"xGreaterOf(r,bu,cv)" using GreaterOf_def by (cases "bu,cvr",auto)
    from B C D have "xRightRayX(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 "xRightRayX(X, r, GreaterOf(r, bu, cv))"
    then have R:"xX""GreaterOf(r,bu,cv),xr""xGreaterOf(r,bu,cv)" using RightRayX_def by auto
    {
      {
        assume AS:"bu,cvr"
        then have "GreaterOf(r,bu,cv)=cv" using GreaterOf_def by auto
        then have "cv,xr" using R(2) by auto
        with AS have "bu,xr" "cv,xr" using assms IsLinOrder_def trans_def by(safe, blast)
      }
      moreover
      {
        assume AS:"bu,cvr"
        then have "GreaterOf(r,bu,cv)=bu" using GreaterOf_def by auto
        then have "bu,xr" using R(2) by auto
        from AS have "cv,bur" using assms IsLinOrder_def IsTotal_def assms by auto
        with bu,xr have "cv,xr" "bu,xr" using assms IsLinOrder_def trans_def by(safe, blast)
      }
      ultimately have T:"cv,xr" "bu,xr" by auto
      moreover
      {
        assume AS:"x=bu"
        then have "cv,bur" using T(1) by auto
        then have "GreaterOf(r,bu,cv)=bu" using GreaterOf_def assms IsLinOrder_def
          antisym_def by auto
        with xGreaterOf(r,bu,cv) have "False" using AS by auto
      }
      moreover
      {
        assume AS:"x=cv"
        then have "bu,cvr" using T(2) by auto
        then have "GreaterOf(r,bu,cv)=cv" using GreaterOf_def assms IsLinOrder_def
          antisym_def by auto
        with xGreaterOf(r,bu,cv) have "False" using AS by auto
      }
      ultimately have "bu,xr" "cv,xr""xbu""xcv" by auto
    }
    with xX 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

textThe open intervals and rays satisfy the base condition.

lemma intervals_rays_base_condition:
  assumes "IsLinOrder(X,r)"
  shows "{IntervalX(X,r,b,c). b,cX×X}{LeftRayX(X,r,b). bX}{RightRayX(X,r,b). bX} {satisfies the base condition}"
proof-
  let ?I="{IntervalX(X,r,b,c). b,cX×X}"
  let ?R="{RightRayX(X,r,b). bX}"
  let ?L="{LeftRayX(X,r,b). bX}"
  let ?B="{IntervalX(X,r,b,c). b,cX×X}{LeftRayX(X,r,b). bX}{RightRayX(X,r,b). bX}"
  {
    fix U V
    assume A:"U?B""V?B"
    then have dU:"U?IU?LU?R"and dV:"V?IV?LV?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)""buX""cuX""bvX""cvX"
          by auto
        then have "SmallerOf(r,cu,cv)X""GreaterOf(r,bu,bv)X" by (cases "cu,cvr",simp add:SmallerOf_def A,simp add:SmallerOf_def A,
          cases "bu,bvr",simp add:GreaterOf_def A,simp add:GreaterOf_def A)
        with A have "UV?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)""buX""bvX""cvX"
        by auto
        then have "SmallerOf(r,bu,cv)X" using SmallerOf_def by (cases "bu,cvr",auto)
        with A have "UV?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)""cuX""bvX""cvX"
        by auto
        then have "GreaterOf(r,cu,bv)X" using GreaterOf_def by (cases "cu,bvr",auto)
        with A have "UV?B" using inter_rray_interval assms by auto
      }
      ultimately have "UV?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)""buX""bvX""cvX"
          by auto
        then have "SmallerOf(r,bu,cv)X" using SmallerOf_def by (cases "bu,cvr", auto)
        have "UV=VU" by auto
        with A SmallerOf(r,bu,cv)X have "UV?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)""buX""cvX"
        by auto
        have "UV=VU" by auto
        with A have "UV?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)""buX""bvX"
        by auto
        then have "SmallerOf(r,bu,bv)X" using SmallerOf_def by (cases "bu,bvr", auto)
        with A have "UV?B" using inter_lray_lray assms by auto
      }
      ultimately have "UV?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)""cuX""bvX""cvX"
        by auto
        then have "GreaterOf(r,cu,bv)X" using GreaterOf_def by (cases "cu,bvr",auto)
        have "UV=VU" by auto
        with A GreaterOf(r,cu,bv)X have "UV?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)""buX""cvX"
        by auto
        then have "UV?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)""cuX""cvX"
        by auto
        then have "GreaterOf(r,cu,cv)X" using GreaterOf_def by (cases "cu,cvr",auto)
        with A have "UV?B" using inter_rray_rray assms by auto
      }
      ultimately have "UV?B" using dU by auto
    }
    ultimately have  S:"UV?B" using dV by auto
    {
      fix x
      assume "xUV"
      then have "xUVUVUV" by auto
      then have "W. W(?B) xW  W  UV" using S by blast
      then have "W(?B). xW  W  UV" by blast
    }
    hence "(x  UV. W(?B). xW  W  UV)" by auto
  }
  then show ?thesis using SatisfiesBaseCondition_def by auto
qed

textSince 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,cX×X}{LeftRayX(X,r,b). bX}{RightRayX(X,r,b). bX}"

theorem Ordtopology_is_a_topology:
  assumes "IsLinOrder(X,r)"
  shows "(OrdTopology X r) {is a topology}" and "{IntervalX(X,r,b,c). b,cX×X}{LeftRayX(X,r,b). bX}{RightRayX(X,r,b). bX} {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

subsectionTotal set

textThe topology is defined in the set $X$, when $X$ has more than 
one point

lemma union_ordtopology:
  assumes "IsLinOrder(X,r)""x y. xy  xX yX"
  shows "(OrdTopology X r)=X"
proof
  let ?B="{IntervalX(X,r,b,c). b,cX×X}{LeftRayX(X,r,b). bX}{RightRayX(X,r,b). bX}"
  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:"xy  xX yX" by auto
  then have B:"xLeftRayX(X,r,y)xRightRayX(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:"zX"
    {
      assume "x=z"
      then have "z(OrdTopology X r)" using x by auto
    }
    moreover
    {
      assume "xz"
      with z T have "zLeftRayX(X,r,x)zRightRayX(X,r,x)""xX" 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 "?BX" using IntervalX_def LeftRayX_def RightRayX_def by auto
  then show "(OrdTopology X r)X" using Top_1_2_L5 base by auto
qed

textThe interior, closure and boundary can be calculated using the formulas
proved in the section that deals with the base.

textThe subspace of an order topology doesn't have to be an
order topology.

(*Note: Build a counter-example using the real numbers.*)

subsectionRight order and Left order topologies.

textNotice 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.

textIf 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.

subsubsectionRight and Left Order topologies are topologies

lemma leftrays_base_condition:
assumes "