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

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

subsection‹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 ‹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}""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)}, (∩)(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, (∩)(Y)))}" unfolding RestrictedTo_def
      by blast
  }
  hence "RepFun({⋃A . A ∈ Pow(B)}, (∩)(Y)) ⊆ {⋃A . A ∈ Pow(RepFun(B, (∩)(Y)))}" by(auto+)
  moreover
  {
    fix t
    assume "t∈{⋃A . A ∈ Pow(RepFun(B, (∩)(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)}, (∩)(Y))" by auto
  }
  hence "{⋃A . A ∈ Pow(RepFun(B, (∩)(Y)))} ⊆ RepFun({⋃A . A ∈ Pow(B)}, (∩)(Y)) " by (auto+)
  ultimately have "{⋃A . A ∈ Pow(RepFun(B, (∩)(Y)))} = RepFun({⋃A . A ∈ Pow(B)}, (∩)(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

subsection‹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 ‹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 ‹(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

subsection‹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 ‹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

subsection‹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