(*

This file is a part of IsarMathLib -

a library of formalized mathematics written for Isabelle/Isar.

Copyright (C) 2012 Daniel de la Concepcion

This program is free software; Redistribution and use in source and binary forms,

with or without modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice,

this list of conditions and the following disclaimer.

2. Redistributions in binary form must reproduce the above copyright notice,

this list of conditions and the following disclaimer in the documentation and/or

other materials provided with the distribution.

3. The name of the author may not be used to endorse or promote products

derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED

WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF

MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.

IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,

SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,

PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;

OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,

WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR

OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,

EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)

header{*\isaheader{Topology\_ZF\_examples\_1.thy}*}

theory Topology_ZF_examples_1

imports Topology_ZF_1 Order_ZF

begin

text{*In this theory file we reformulate the concepts related to a topology

in relation with a base of the topology and we give examples of topologies defined by

bases or subbases.*}

section{*New ideas using a base for a topology*}

subsection{*The topology of a base*}

text{*Given a family of subsets satisfiying the base condition,

it is posible to construct

a topology where that family is a base. Even more,

it is the only topology with such characteristics.*}

definition

TopologyWithBase ("TopologyBase _ " 50) where

"U {satisfies the base condition} ==> TopologyBase U ≡ THE T. U {is a base for} T"

theorem Base_topology_is_a_topology:

assumes "U {satisfies the base condition}"

shows "(TopologyBase U) {is a topology}" and "U {is a base for} (TopologyBase U)"

proof-

from assms obtain T where "U {is a base for} T" using

Top_1_2_T1(2) by blast

then have "∃!T. U {is a base for} T" using same_base_same_top ex1I[where P=

"λT. U {is a base for} T"] by blast

with assms show "U {is a base for} (TopologyBase U) " using theI[where P=

"λT. U {is a base for} T"] TopologyWithBase_def by auto

with assms show "(TopologyBase U) {is a topology}" using Top_1_2_T1(1)

IsAbaseFor_def by auto

qed

text{*A base doesn't need the empty set.*}

lemma base_no_0:

shows "B{is a base for}T <-> (B-{0}){is a base for}T"

proof-

{

fix M

assume "M∈{\<Union>A . A ∈ Pow(B)}"

then obtain Q where "M=\<Union>Q""Q∈Pow(B)" by auto

hence "M=\<Union>(Q-{0})""Q-{0}∈Pow(B-{0})" by auto

hence "M∈{\<Union>A . A ∈ Pow(B - {0})}" by auto

}

hence "{\<Union>A . A ∈ Pow(B)} ⊆ {\<Union>A . A ∈ Pow(B - {0})}" by blast

moreover

{

fix M

assume "M∈{\<Union>A . A ∈ Pow(B-{0})}"

then obtain Q where "M=\<Union>Q""Q∈Pow(B-{0})" by auto

hence "M=\<Union>(Q)""Q∈Pow(B)" by auto

hence "M∈{\<Union>A . A ∈ Pow(B)}" by auto

}

hence " {\<Union>A . A ∈ Pow(B - {0})} ⊆ {\<Union>A . A ∈ Pow(B)} "

by auto

ultimately have "{\<Union>A . A ∈ Pow(B - {0})} = {\<Union>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)=\<Union>{T∈U. T⊆A}"

proof

have "{T∈U. T⊆A}⊆U" by auto

with assms(1) have "\<Union>{T∈U. T⊆A}∈T"

using IsAbaseFor_def by auto

moreover

have "\<Union>{T∈U. T⊆A}⊆A" by blast

with calculation assms(2) show "\<Union>{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∈\<Union>{T∈U. T⊆A}" by auto

}

thus "Interior(A, T) ⊆ \<Union>{T ∈ U . T ⊆ A} " by auto

qed

text{*In the following, we offer another lemma

about the closure of a set given a basis for a topology.

This lemma is based on @{text "cl_inter_neigh"} and @{text

"inter_neigh_cl"}. It states that it is only necessary to

check the sets of the base, not all the open sets.*}

lemma closure_set_base_topology:

assumes "U {is a base for} Q""Q{is a topology}""A⊆\<Union>Q"

shows "Closure(A,Q)={x∈\<Union>Q. ∀T∈U. x∈T-->A∩T≠0}"

proof

{

fix x

assume A:"x∈Closure(A,Q)"

with assms(2,3) have B:"x∈\<Union>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∈\<Union>Q. ∀T∈U. x∈T-->A∩T≠0}" by auto

}

thus "Closure(A, Q) ⊆{x∈\<Union>Q. ∀T∈U. x∈T-->A∩T≠0}"

by auto

{

fix x

assume AS:"x∈{x ∈ \<Union>Q . ∀T∈U. x ∈ T --> A ∩ T ≠ 0}"

hence "x∈\<Union>Q" by blast

moreover

{

fix R

assume "R∈Q"

with assms(1) obtain W where RR:"W⊆U""R=\<Union>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∈\<Union>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 ∈ \<Union>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({\<Union>A . A ∈ Pow(B)}, op ∩(Y))"

then obtain x where A:"t=Y∩x""x∈{\<Union>A . A ∈ Pow(B)}" by auto

then obtain A where B:"x=\<Union>A""A∈Pow(B)" by auto

from A(1) B(1) have "t=\<Union>(A {restricted to} Y)" using RestrictedTo_def

by auto

with B(2) have "t∈{\<Union>A . A ∈ Pow(RepFun(B, op ∩(Y)))}" unfolding RestrictedTo_def

by blast

}

hence "RepFun({\<Union>A . A ∈ Pow(B)}, op ∩(Y)) ⊆ {\<Union>A . A ∈ Pow(RepFun(B, op ∩(Y)))}" by(auto+)

moreover

{

fix t

assume "t∈{\<Union>A . A ∈ Pow(RepFun(B, op ∩(Y)))}"

then obtain A where A:"A⊆ B{restricted to}Y""t=\<Union>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=\<Union>(?AA {restricted to}Y)" by auto

then have "?AA⊆B""t=Y∩(\<Union>?AA)" using RestrictedTo_def by auto

hence "t∈RepFun({\<Union>A . A ∈ Pow(B)}, op ∩(Y))" by auto

}

hence "{\<Union>A . A ∈ Pow(RepFun(B, op ∩(Y)))} ⊆ RepFun({\<Union>A . A ∈ Pow(B)}, op ∩(Y)) " by (auto+)

ultimately have "{\<Union>A . A ∈ Pow(RepFun(B, op ∩(Y)))} = RepFun({\<Union>A . A ∈ Pow(B)}, op ∩(Y))" by auto

with assms show ?thesis using RestrictedTo_def IsAbaseFor_def by auto

qed

text{*If the base of a topology is contained in the base of another

topology, then the topologies maintain the same relation.*}

theorem base_subset:

assumes "B{is a base for}T""B2{is a base for}T2""B⊆B2"

shows "T⊆T2"

proof

{

fix x

assume "x∈T"

with assms(1) obtain M where "M⊆B""x=\<Union>M" using IsAbaseFor_def by auto

with assms(3) have "M⊆B2""x=\<Union>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≡{\<Union>T-U. U∈B}∪{\<Union>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=\<Inter>M"

proof-

assume K:"!!M. M ⊆ DualBase B T ==> D = \<Inter>M ==> thesis"

{

assume AS:"D≠\<Union>T"

from assms(1) have D:"D∈Pow(\<Union>T)""\<Union>T-D∈T" using IsClosed_def by auto

hence A:"\<Union>T-(\<Union>T-D)=D""\<Union>T-D∈T" by auto

with assms(2) obtain Q where QQ:"Q∈Pow(B)""\<Union>T-D=\<Union>Q" using IsAbaseFor_def by auto

{

assume "Q=0"

then have "\<Union>Q=0" by auto

with QQ(2) have "\<Union>T-D=0" by auto

with D(1) have "D=\<Union>T" by auto

with AS have "False" by auto

}

hence QNN:"Q≠0" by auto

from QQ(2) A(1) have "D=\<Union>T-\<Union>Q" by auto

with QNN have "D=\<Inter>{\<Union>T-R. R∈Q}" by auto

moreover

with assms(2) QQ(1) have "{\<Union>T-R. R∈Q}⊆DualBase B T" using DualBase_def

by auto

with calculation K have "thesis" by auto

}

moreover

{

assume AS:"D=\<Union>T"

with assms(2) have "{\<Union>T}⊆DualBase B T" using DualBase_def by auto

moreover

have "\<Union>T = \<Inter>{\<Union>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⊆\<Union>Q"

shows "Closure(A,Q)=\<Inter>{T∈DualBase U Q. A⊆T}"

proof

from assms(1) have T:"\<Union>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=\<Union>Q-R∧R∈U)∨T=\<Union>Q" using DualBase_def

by auto

with A(2) assms(1,2) have "(T{is closed in}Q)""A⊆T""T∈Pow(\<Union>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(\<Union>Q). (T{is closed in}Q)∧A⊆T}"

by blast

with calculation assms(3) have "\<Inter>{T∈Pow(\<Union>Q). (T{is closed in}Q)∧A⊆T}⊆\<Inter>{T∈DualBase U Q. A⊆T}"

by auto

then show "Closure(A,Q)⊆\<Inter>{T∈DualBase U Q. A⊆T}" using Closure_def ClosedCovers_def

by auto

{

fix x

assume A:"x∈\<Inter>{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 "\<Union>Q-T∈DualBase U Q" using DualBase_def

by auto

moreover

from C assms(3) have "A⊆\<Union>Q-T" by auto

moreover

from B(1) have "x∉\<Union>Q-T" by auto

ultimately have "x∉\<Inter>{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∈\<Union>Q" by auto

with calculation assms have "x∈Closure(A,Q)" using closure_set_base_topology

by auto

}

thus "\<Inter>{T ∈ DualBase U Q . A ⊆ T} ⊆ Closure(A, Q)" by auto

qed

section{*Partition topology*}

text{*In the theory file Partitions\_ZF.thy; there is

a definition to work with partitions. In this setting

is much easier to work with a family of subsets.*}

definition

IsAPartition ("_{is a partition of}_" 90) where

"(U {is a partition of} X) ≡ (\<Union>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}\<Union>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 - \<Union>R=\<Union>(P-R)"

proof

{

fix x

assume "x∈X - \<Union>R"

hence P:"x∈X""x∉\<Union>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∈\<Union>(P-R)" by auto

}

thus "X - \<Union>R⊆\<Union>(P-R)" by auto

{

fix x

assume "x∈\<Union>(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∈\<Union>P" by auto

with assms(2) have "x∈X" using IsAPartition_def by auto

moreover

{

assume "x∈\<Union>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∉\<Union>R" by auto

ultimately have "x∈X-\<Union>R" by auto

}

thus "\<Union>(P-R)⊆X - \<Union>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 "\<Union>(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=\<Union>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-\<Union>R" by auto

with Q(1) assms have "D=\<Union>(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=\<Union>R" using IsAbaseFor_def by auto

hence "X-D=X-\<Union>R" by auto

with Q(1) assms have "X-D=\<Union>(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⊆\<Union>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))=\<Inter>{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=\<Union>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⊆\<Union>U" by auto

with assms(1) have "w⊆\<Union>(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∈\<Inter>{T∈DualBase U (PTopology X U). T=X∨T∪A≠X}"

by auto

}

thus "Interior(A,(PTopology X U))⊆\<Inter>{T∈DualBase U (PTopology X U). T=X∨T∪A≠X}" by auto

{

fix x

assume p:"x∈\<Inter>{T∈DualBase U (PTopology X U). T=X∨T∪A≠X}"

hence noE:"\<Inter>{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 "(\<Inter>{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:"(\<Inter>{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)""(\<Inter>{T∈DualBase U (PTopology X U). T=X∨T∪A≠X})=\<Union>B"

using Ptopology_is_a_topology(2) IsAbaseFor_def by auto

with p obtain R where "x∈R""R∈U""R⊆(\<Inter>{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⊆(\<Inter>{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 "\<Inter>{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∈\<Union>(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 "\<Inter>{T ∈ DualBase U PTopology X U . T = X ∨ T ∪ A ≠ X} ⊆ Interior(A, PTopology X U)"

by auto

qed

text{*The closure of a set is the union of

all the sets of the partition which intersect

with @{text "A"}.*}

lemma closure_set_ptopology:

assumes "U {is a partition of} X""A⊆X"

shows "Closure(A,(PTopology X U))=\<Union>{T∈U. T∩A≠0}"

proof

{

fix x

assume A:"x∈Closure(A,(PTopology X U))"

with assms have "x∈\<Union>(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∈\<Union>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∈\<Union>{T∈U. T∩A≠0}" by blast

}

thus "Closure(A, PTopology X U) ⊆ \<Union>{T ∈ U . T ∩ A ≠ 0}" by auto

{

fix x

assume "x∈\<Union>{T ∈ U . T ∩ A ≠ 0}"

then obtain T where A:"x∈T""T∈U""T∩A≠0" by auto

from assms have "A⊆\<Union>(PTopology X U)" using union_ptopology by auto

moreover

from A(1,2) assms(1) have "x∈\<Union>(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=\<Union>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 "\<Union>{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))=\<Union>{T∈U. T∩A≠0 ∧ ~(T⊆A)}"

proof-

from assms have "Closure(A,(PTopology X U))=\<Union>{T ∈ U . T ∩ A ≠ 0}" using

closure_set_ptopology by auto

moreover

from assms(1) have "Interior(A,(PTopology X U))=\<Union>{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))=\<Union>{T ∈ U . T ∩ A ≠ 0} - \<Union>{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} \<Union>({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 "\<Union>{T ∈ U . T ∩ A ≠ 0} - \<Union>{T ∈ U . T ⊆ A}=\<Union>(({T ∈ U . T ∩ A ≠ 0})-({T ∈ U . T ⊆ A}))"

using diff_union_is_union_diff by auto

also have "…=\<Union>({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⊆\<Union>(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 "\<Union>({{x}. x∈t})=t" by auto

moreover

from A have "{{x}. x∈t}∈Pow({{x}.x∈X})" by auto

hence "\<Union>({{x}. x∈t})∈{\<Union>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}""\<Union>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 "\<Union>(PTopology X {X})∈(PTopology X {X})" using union_open Ptopology_is_a_topology(1)

indiscrete_partition by auto

with assms have "X∈(PTopology X {X})" using union_ptopology indiscrete_partition

by auto

ultimately show "{0,X}⊆(PTopology X {X})" by auto

qed

text{*The topological subspaces of the @{text "(PTopology X U)"}

are partition topologies.*}

lemma subspace_ptopology:

assumes "U{is a partition of}X"

shows "(PTopology X U) {restricted to} Y=(PTopology (X∩Y) ((U {restricted to} Y)-{0}))"

proof-

from assms have "U{is a base for}(PTopology X U)" using Ptopology_is_a_topology(2)

by auto

then have "(U{restricted to} Y){is a base for}(PTopology X U){restricted to} Y"

using subspace_base_topology by auto

then have "((U{restricted to} Y)-{0}){is a base for}(PTopology X U){restricted to} Y" using base_no_0

by auto

moreover

from assms have "((U{restricted to} Y)-{0}) {is a partition of} (X∩Y)"

using restriction_partition by auto

then have "((U{restricted to} Y)-{0}){is a base for}(PTopology (X∩Y) ((U {restricted to} Y)-{0}))"

using Ptopology_is_a_topology(2) by auto

ultimately show ?thesis using same_base_same_top by auto

qed

section{*Order topologies*}

subsection{*Order topology is a topology*}

text{*Given a totally ordered set, several topologies can be defined

using the order relation. First we define an open interval, notice that

the set defined as @{text "Interval"} is a closed interval; and open rays.*}

definition

IntervalX where

"IntervalX(X,r,b,c)≡(Interval(r,b,c)∩X)-{b,c}"

definition

LeftRayX where

"LeftRayX(X,r,b)≡{c∈X. ⟨c,b⟩∈r}-{b}"

definition

RightRayX where

"RightRayX(X,r,b)≡{c∈X. ⟨b,c⟩∈r}-{b}"

text{*Intersections of intervals and rays.*}

lemma inter_two_intervals:

assumes "bu∈X""bv∈X""cu∈X""cv∈X""IsLinOrder(X,r)"

shows "IntervalX(X,r,bu,cu)∩IntervalX(X,r,bv,cv)=IntervalX(X,r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv))"

proof

have T:"GreaterOf(r,bu,bv)∈X""SmallerOf(r,cu,cv)∈X" using assms

GreaterOf_def SmallerOf_def by (cases "⟨bu,bv⟩∈r",simp,simp,cases "⟨cu,cv⟩∈r",simp,simp)

{

fix x

assume ASS:"x∈IntervalX(X,r,bu,cu)∩IntervalX(X,r,bv,cv)"

then have "x∈IntervalX(X,r,bu,cu)""x∈IntervalX(X,r,bv,cv)" by auto

then have BB:"x∈X""x∈Interval(r,bu,cu)""x≠bu""x≠cu""x∈Interval(r,bv,cv)""x≠bv""x≠cv"

using IntervalX_def assms by auto

then have "x∈X" by auto

moreover

have "x≠GreaterOf(r,bu,bv)""x≠SmallerOf(r,cu,cv)"

proof-

show "x≠GreaterOf(r,bu,bv)" using GreaterOf_def BB(6,3) by (cases "⟨bu,bv⟩∈r",simp+)

show "x≠SmallerOf(r,cu,cv)" using SmallerOf_def BB(7,4) by (cases "⟨cu,cv⟩∈r",simp+)

qed

moreover

have "⟨bu,x⟩∈r""⟨x,cu⟩∈r""⟨bv,x⟩∈r""⟨x,cv⟩∈r" using BB(2,5) Order_ZF_2_L1A by auto

then have "⟨GreaterOf(r,bu,bv),x⟩∈r""⟨x,SmallerOf(r,cu,cv)⟩∈r" using GreaterOf_def SmallerOf_def

by (cases "⟨bu,bv⟩∈r",simp,simp,cases "⟨cu,cv⟩∈r",simp,simp)

then have "x∈Interval(r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv))" using Order_ZF_2_L1 by auto

ultimately

have "x∈IntervalX(X,r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv))" using IntervalX_def T by auto

}

then show "IntervalX(X, r, bu, cu) ∩ IntervalX(X, r, bv, cv) ⊆ IntervalX(X, r, GreaterOf(r, bu, bv), SmallerOf(r, cu, cv))"

by auto

{

fix x

assume "x∈IntervalX(X,r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv))"

then have BB:"x∈X""x∈Interval(r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv))""x≠GreaterOf(r,bu,bv)""x≠SmallerOf(r,cu,cv)"

using IntervalX_def T by auto

then have "x∈X" by auto

moreover

from BB(2) have CC:"⟨GreaterOf(r,bu,bv),x⟩∈r""⟨x,SmallerOf(r,cu,cv)⟩∈r" using Order_ZF_2_L1A by auto

{

{

assume AS:"⟨bu,bv⟩∈r"

then have "GreaterOf(r,bu,bv)=bv" using GreaterOf_def by auto

then have "⟨bv,x⟩∈r" using CC(1) by auto

with AS have "⟨bu,x⟩∈r" "⟨bv,x⟩∈r" using assms IsLinOrder_def trans_def by (safe, blast)

}

moreover

{

assume AS:"⟨bu,bv⟩∉r"

then have "GreaterOf(r,bu,bv)=bu" using GreaterOf_def by auto

then have "⟨bu,x⟩∈r" using CC(1) by auto

from AS have "⟨bv,bu⟩∈r" using assms IsLinOrder_def IsTotal_def assms by auto

with `⟨bu,x⟩∈r` have "⟨bu,x⟩∈r" "⟨bv,x⟩∈r" using assms IsLinOrder_def trans_def by (safe, blast)

}

ultimately have R:"⟨bu,x⟩∈r" "⟨bv,x⟩∈r" by auto

moreover

{

assume AS:"x=bu"

then have "⟨bv,bu⟩∈r" using R(2) by auto

then have "GreaterOf(r,bu,bv)=bu" using GreaterOf_def assms IsLinOrder_def

antisym_def by auto

then have "False" using AS BB(3) by auto

}

moreover

{

assume AS:"x=bv"

then have "⟨bu,bv⟩∈r" using R(1) by auto

then have "GreaterOf(r,bu,bv)=bv" using GreaterOf_def by auto

then have "False" using AS BB(3) by auto

}

ultimately have "⟨bu,x⟩∈r" "⟨bv,x⟩∈r""x≠bu""x≠bv" by auto

}

moreover

{

{

assume AS:"⟨cu,cv⟩∈r"

then have "SmallerOf(r,cu,cv)=cu" using SmallerOf_def by auto

then have "⟨x,cu⟩∈r" using CC(2) by auto

with AS have "⟨x,cu⟩∈r" "⟨x,cv⟩∈r" using assms IsLinOrder_def trans_def by(safe ,blast)

}

moreover

{

assume AS:"⟨cu,cv⟩∉r"

then have "SmallerOf(r,cu,cv)=cv" using SmallerOf_def by auto

then have "⟨x,cv⟩∈r" using CC(2) by auto

from AS have "⟨cv,cu⟩∈r" using assms IsLinOrder_def IsTotal_def by auto

with `⟨x,cv⟩∈r` have "⟨x,cv⟩∈r" "⟨x,cu⟩∈r" using assms IsLinOrder_def trans_def by(safe ,blast)

}

ultimately have R:"⟨x,cv⟩∈r" "⟨x,cu⟩∈r" by auto

moreover

{

assume AS:"x=cv"

then have "⟨cv,cu⟩∈r" using R(2) by auto

then have "SmallerOf(r,cu,cv)=cv" using SmallerOf_def assms IsLinOrder_def

antisym_def by auto

then have "False" using AS BB(4) by auto

}

moreover

{

assume AS:"x=cu"

then have "⟨cu,cv⟩∈r" using R(1) by auto

then have "SmallerOf(r,cu,cv)=cu" using SmallerOf_def by auto

then have "False" using AS BB(4) by auto

}

ultimately have "⟨x,cu⟩∈r" "⟨x,cv⟩∈r""x≠cu""x≠cv" by auto

}

ultimately

have "x∈IntervalX(X,r,bu,cu)" "x∈IntervalX(X,r,bv,cv)" using Order_ZF_2_L1 IntervalX_def

assms by auto

then have "x∈IntervalX(X, r, bu, cu) ∩ IntervalX(X, r, bv, cv) " by auto

}

then show "IntervalX(X,r,GreaterOf(r,bu,bv),SmallerOf(r,cu,cv)) ⊆ IntervalX(X, r, bu, cu) ∩ IntervalX(X, r, bv, cv)"

by auto

qed

lemma inter_rray_interval:

assumes "bv∈X""bu∈X""cv∈X""IsLinOrder(X,r)"

shows "RightRayX(X,r,bu)∩IntervalX(X,r,bv,cv)=IntervalX(X,r,GreaterOf(r,bu,bv),cv)"

proof

{

fix x

assume "x∈RightRayX(X,r,bu)∩IntervalX(X,r,bv,cv)"

then have "x∈RightRayX(X,r,bu)""x∈IntervalX(X,r,bv,cv)" by auto

then have BB:"x∈X""x≠bu""x≠bv""x≠cv""⟨bu,x⟩∈r""x∈Interval(r,bv,cv)" using RightRayX_def IntervalX_def

by auto

then have "⟨bv,x⟩∈r""⟨x,cv⟩∈r" using Order_ZF_2_L1A by auto

with `⟨bu,x⟩∈r` have "⟨GreaterOf(r,bu,bv),x⟩∈r" using GreaterOf_def by (cases "⟨bu,bv⟩∈r",simp+)

with `⟨x,cv⟩∈r` have "x∈Interval(r,GreaterOf(r,bu,bv),cv)" using Order_ZF_2_L1 by auto

then have "x∈IntervalX(X,r,GreaterOf(r,bu,bv),cv)" using BB(1-4) IntervalX_def GreaterOf_def

by (simp)

}

then show "RightRayX(X, r, bu) ∩ IntervalX(X, r, bv, cv) ⊆ IntervalX(X, r, GreaterOf(r, bu, bv), cv)" by auto

{

fix x

assume "x∈IntervalX(X, r, GreaterOf(r, bu, bv), cv)"

then have "x∈X""x∈Interval(r,GreaterOf(r, bu, bv), cv)""x≠cv""x≠GreaterOf(r, bu, bv)" using IntervalX_def by auto

then have R:"⟨GreaterOf(r, bu, bv),x⟩∈r""⟨x,cv⟩∈r" using Order_ZF_2_L1A by auto

with `x≠cv` have "⟨x,cv⟩∈r""x≠cv" by auto

moreover

{

{

assume AS:"⟨bu,bv⟩∈r"

then have "GreaterOf(r,bu,bv)=bv" using GreaterOf_def by auto

then have "⟨bv,x⟩∈r" using R(1) by auto

with AS have "⟨bu,x⟩∈r" "⟨bv,x⟩∈r" using assms unfolding IsLinOrder_def trans_def by (safe,blast)

}

moreover

{

assume AS:"⟨bu,bv⟩∉r"

then have "GreaterOf(r,bu,bv)=bu" using GreaterOf_def by auto

then have "⟨bu,x⟩∈r" using R(1) by auto

from AS have "⟨bv,bu⟩∈r" using assms unfolding IsLinOrder_def IsTotal_def using assms by auto

with `⟨bu,x⟩∈r` have "⟨bu,x⟩∈r" "⟨bv,x⟩∈r" using assms unfolding IsLinOrder_def trans_def by (safe,blast)

}

ultimately have T:"⟨bu,x⟩∈r" "⟨bv,x⟩∈r" by auto

moreover

{

assume AS:"x=bu"

then have "⟨bv,bu⟩∈r" using T(2) by auto

then have "GreaterOf(r,bu,bv)=bu" unfolding GreaterOf_def using assms unfolding IsLinOrder_def

antisym_def by auto

with `x≠GreaterOf(r,bu,bv)` have "False" using AS by auto

}

moreover

{

assume AS:"x=bv"

then have "⟨bu,bv⟩∈r" using T(1) by auto

then have "GreaterOf(r,bu,bv)=bv" unfolding GreaterOf_def by auto

with `x≠GreaterOf(r,bu,bv)` have "False" using AS by auto

}

ultimately have "⟨bu,x⟩∈r" "⟨bv,x⟩∈r""x≠bu""x≠bv" by auto

}

with calculation `x∈X` have "x∈RightRayX(X, r, bu)""x∈IntervalX(X, r, bv, cv)" unfolding RightRayX_def IntervalX_def

using Order_ZF_2_L1 by auto

then have "x∈RightRayX(X, r, bu) ∩ IntervalX(X, r, bv, cv) " by auto

}

then show "IntervalX(X, r, GreaterOf(r, bu, bv), cv) ⊆ RightRayX(X, r, bu) ∩ IntervalX(X, r, bv, cv) " by auto

qed

lemma inter_lray_interval:

assumes "bv∈X""cu∈X""cv∈X""IsLinOrder(X,r)"

shows "LeftRayX(X,r,cu)∩IntervalX(X,r,bv,cv)=IntervalX(X,r,bv,SmallerOf(r,cu,cv))"

proof

{

fix x assume "x∈LeftRayX(X,r,cu)∩IntervalX(X,r,bv,cv)"

then have B:"x≠cu""x∈X""⟨x,cu⟩∈r""⟨bv,x⟩∈r""⟨x,cv⟩∈r""x≠bv""x≠cv" unfolding LeftRayX_def IntervalX_def Interval_def

by auto

from `⟨x,cu⟩∈r` `⟨x,cv⟩∈r` have C:"⟨x,SmallerOf(r, cu, cv)⟩∈r" using SmallerOf_def by (cases "⟨cu,cv⟩∈r",simp+)

from B(7,1) have "x≠SmallerOf(r,cu,cv)" using SmallerOf_def by (cases "⟨cu,cv⟩∈r",simp+)

then have "x∈IntervalX(X,r,bv,SmallerOf(r,cu,cv))" using B C IntervalX_def Order_ZF_2_L1 by auto

}

then show "LeftRayX(X, r, cu) ∩ IntervalX(X, r, bv, cv) ⊆ IntervalX(X, r, bv, SmallerOf(r, cu, cv))" by auto

{

fix x assume "x∈IntervalX(X,r,bv,SmallerOf(r,cu,cv))"

then have R:"x∈X""⟨bv,x⟩∈r""⟨x,SmallerOf(r,cu,cv)⟩∈r""x≠bv""x≠SmallerOf(r,cu,cv)" using IntervalX_def Interval_def

by auto

then have "⟨bv,x⟩∈r""x≠bv" by auto

moreover

{

{

assume AS:"⟨cu,cv⟩∈r"

then have "SmallerOf(r,cu,cv)=cu" using SmallerOf_def by auto

then have "⟨x,cu⟩∈r" using R(3) by auto

with AS have "⟨x,cu⟩∈r" "⟨x,cv⟩∈r" using assms unfolding IsLinOrder_def trans_def by (safe, blast)

}

moreover

{

assume AS:"⟨cu,cv⟩∉r"

then have "SmallerOf(r,cu,cv)=cv" using SmallerOf_def by auto

then have "⟨x,cv⟩∈r" using R(3) by auto

from AS have "⟨cv,cu⟩∈r" using assms IsLinOrder_def IsTotal_def assms by auto

with `⟨x,cv⟩∈r` have "⟨x,cv⟩∈r" "⟨x,cu⟩∈r" using assms IsLinOrder_def trans_def by (safe, blast)

}

ultimately have T:"⟨x,cv⟩∈r" "⟨x,cu⟩∈r" by auto

moreover

{

assume AS:"x=cu"

then have "⟨cu,cv⟩∈r" using T(1) by auto

then have "SmallerOf(r,cu,cv)=cu" using SmallerOf_def assms IsLinOrder_def

antisym_def by auto

with `x≠SmallerOf(r,cu,cv)` have "False" using AS by auto

}

moreover

{

assume AS:"x=cv"

then have "⟨cv,cu⟩∈r" using T(2) by auto

then have "SmallerOf(r,cu,cv)=cv" using SmallerOf_def assms IsLinOrder_def

antisym_def by auto

with `x≠SmallerOf(r,cu,cv)` have "False" using AS by auto

}

ultimately have "⟨x,cu⟩∈r" "⟨x,cv⟩∈r""x≠cu""x≠cv" by auto

}

with calculation `x∈X` have "x∈LeftRayX(X,r,cu)""x∈IntervalX(X, r, bv, cv)" using LeftRayX_def IntervalX_def Interval_def

by auto

then have "x∈LeftRayX(X, r, cu) ∩ IntervalX(X, r, bv, cv)" by auto

}

then show "IntervalX(X, r, bv, SmallerOf(r, cu, cv)) ⊆ LeftRayX(X, r, cu) ∩ IntervalX(X, r, bv, cv) " by auto

qed

lemma inter_lray_rray:

assumes "bu∈X""cv∈X""IsLinOrder(X,r)"

shows "LeftRayX(X,r,bu)∩RightRayX(X,r,cv)=IntervalX(X,r,cv,bu)"

unfolding LeftRayX_def RightRayX_def IntervalX_def Interval_def by auto

lemma inter_lray_lray:

assumes "bu∈X""cv∈X""IsLinOrder(X,r)"

shows "LeftRayX(X,r,bu)∩LeftRayX(X,r,cv)=LeftRayX(X,r,SmallerOf(r,bu,cv))"

proof

{

fix x

assume "x∈LeftRayX(X,r,bu)∩LeftRayX(X,r,cv)"

then have B:"x∈X""⟨x,bu⟩∈r""⟨x,cv⟩∈r""x≠bu""x≠cv" using LeftRayX_def by auto

then have C:"⟨x,SmallerOf(r,bu,cv)⟩∈r" using SmallerOf_def by (cases "⟨bu,cv⟩∈r", auto)

from B have D:"x≠SmallerOf(r,bu,cv)" using SmallerOf_def by (cases "⟨bu,cv⟩∈r", auto)

from B C D have "x∈LeftRayX(X,r,SmallerOf(r,bu,cv))" using LeftRayX_def by auto

}

then show "LeftRayX(X, r, bu) ∩ LeftRayX(X, r, cv) ⊆ LeftRayX(X, r, SmallerOf(r, bu, cv))" by auto

{

fix x

assume "x∈LeftRayX(X, r, SmallerOf(r, bu, cv))"

then have R:"x∈X""⟨x,SmallerOf(r,bu,cv)⟩∈r""x≠SmallerOf(r,bu,cv)" using LeftRayX_def by auto

{

{

assume AS:"⟨bu,cv⟩∈r"

then have "SmallerOf(r,bu,cv)=bu" using SmallerOf_def by auto

then have "⟨x,bu⟩∈r" using R(2) by auto

with AS have "⟨x,bu⟩∈r" "⟨x,cv⟩∈r" using assms IsLinOrder_def trans_def by(safe, blast)

}

moreover

{

assume AS:"⟨bu,cv⟩∉r"

then have "SmallerOf(r,bu,cv)=cv" using SmallerOf_def by auto

then have "⟨x,cv⟩∈r" using R(2) by auto

from AS have "⟨cv,bu⟩∈r" using assms IsLinOrder_def IsTotal_def assms by auto

with `⟨x,cv⟩∈r` have "⟨x,cv⟩∈r" "⟨x,bu⟩∈r" using assms IsLinOrder_def trans_def by(safe, blast)

}

ultimately have T:"⟨x,cv⟩∈r" "⟨x,bu⟩∈r" by auto

moreover

{

assume AS:"x=bu"

then have "⟨bu,cv⟩∈r" using T(1) by auto

then have "SmallerOf(r,bu,cv)=bu" using SmallerOf_def assms IsLinOrder_def

antisym_def by auto

with `x≠SmallerOf(r,bu,cv)` have "False" using AS by auto

}

moreover

{

assume AS:"x=cv"

then have "⟨cv,bu⟩∈r" using T(2) by auto

then have "SmallerOf(r,bu,cv)=cv" using SmallerOf_def assms IsLinOrder_def

antisym_def by auto

with `x≠SmallerOf(r,bu,cv)` have "False" using AS by auto

}

ultimately have "⟨x,bu⟩∈r" "⟨x,cv⟩∈r""x≠bu""x≠cv" by auto

}

with `x∈X` have "x∈ LeftRayX(X, r, bu) ∩ LeftRayX(X, r, cv)" using LeftRayX_def by auto

}

then show "LeftRayX(X, r, SmallerOf(r, bu, cv)) ⊆ LeftRayX(X, r, bu) ∩ LeftRayX(X, r, cv) " by auto

qed

lemma inter_rray_rray:

assumes "bu∈X""cv∈X""IsLinOrder(X,r)"

shows "RightRayX(X,r,bu)∩RightRayX(X,r,cv)=RightRayX(X,r,GreaterOf(r,bu,cv))"

proof

{

fix x

assume "x∈RightRayX(X,r,bu)∩RightRayX(X,r,cv)"

then have B:"x∈X""⟨bu,x⟩∈r""⟨cv,x⟩∈r""x≠bu""x≠cv" using RightRayX_def by auto

then have C:"⟨GreaterOf(r,bu,cv),x⟩∈r" using GreaterOf_def by (cases "⟨bu,cv⟩∈r",auto)

from B have D:"x≠GreaterOf(r,bu,cv)" using GreaterOf_def by (cases "⟨bu,cv⟩∈r",auto)

from B C D have "x∈RightRayX(X,r,GreaterOf(r,bu,cv))" using RightRayX_def by auto

}

then show " RightRayX(X, r, bu) ∩ RightRayX(X, r, cv) ⊆ RightRayX(X, r, GreaterOf(r, bu, cv))" by auto

{

fix x

assume "x∈RightRayX(X, r, GreaterOf(r, bu, cv))"

then have R:"x∈X""⟨GreaterOf(r,bu,cv),x⟩∈r""x≠GreaterOf(r,bu,cv)" using RightRayX_def by auto

{

{

assume AS:"⟨bu,cv⟩∈r"

then have "GreaterOf(r,bu,cv)=cv" using GreaterOf_def by auto

then have "⟨cv,x⟩∈r" using R(2) by auto

with AS have "⟨bu,x⟩∈r" "⟨cv,x⟩∈r" using assms IsLinOrder_def trans_def by(safe, blast)

}

moreover

{

assume AS:"⟨bu,cv⟩∉r"

then have "GreaterOf(r,bu,cv)=bu" using GreaterOf_def by auto

then have "⟨bu,x⟩∈r" using R(2) by auto

from AS have "⟨cv,bu⟩∈r" using assms IsLinOrder_def IsTotal_def assms by auto

with `⟨bu,x⟩∈r` have "⟨cv,x⟩∈r" "⟨bu,x⟩∈r" using assms IsLinOrder_def trans_def by(safe, blast)

}

ultimately have T:"⟨cv,x⟩∈r" "⟨bu,x⟩∈r" by auto

moreover

{

assume AS:"x=bu"

then have "⟨cv,bu⟩∈r" using T(1) by auto

then have "GreaterOf(r,bu,cv)=bu" using GreaterOf_def assms IsLinOrder_def

antisym_def by auto

with `x≠GreaterOf(r,bu,cv)` have "False" using AS by auto

}

moreover

{

assume AS:"x=cv"

then have "⟨bu,cv⟩∈r" using T(2) by auto

then have "GreaterOf(r,bu,cv)=cv" using GreaterOf_def assms IsLinOrder_def

antisym_def by auto

with `x≠GreaterOf(r,bu,cv)` have "False" using AS by auto

}

ultimately have "⟨bu,x⟩∈r" "⟨cv,x⟩∈r""x≠bu""x≠cv" by auto

}

with `x∈X` have "x∈ RightRayX(X, r, bu) ∩ RightRayX(X, r, cv) " using RightRayX_def by auto

}

then show "RightRayX(X, r, GreaterOf(r, bu, cv)) ⊆ RightRayX(X, r, bu) ∩ RightRayX(X, r, cv)" by auto

qed

text{*The open intervals and rays satisfy the base condition.*}

lemma intervals_rays_base_condition:

assumes "IsLinOrder(X,r)"

shows "{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X} {satisfies the base condition}"

proof-

let ?I="{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}"

let ?R="{RightRayX(X,r,b). b∈X}"

let ?L="{LeftRayX(X,r,b). b∈X}"

let ?B="{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X}"

{

fix U V

assume A:"U∈?B""V∈?B"

then have dU:"U∈?I∨U∈?L∨U∈?R"and dV:"V∈?I∨V∈?L∨V∈?R" by auto

{

assume S:"V∈?I"

{

assume "U∈?I"

with S obtain bu cu bv cv where A:"U=IntervalX(X,r,bu,cu)""V=IntervalX(X,r,bv,cv)""bu∈X""cu∈X""bv∈X""cv∈X"

by auto

then have "SmallerOf(r,cu,cv)∈X""GreaterOf(r,bu,bv)∈X" by (cases "⟨cu,cv⟩∈r",simp add:SmallerOf_def A,simp add:SmallerOf_def A,

cases "⟨bu,bv⟩∈r",simp add:GreaterOf_def A,simp add:GreaterOf_def A)

with A have "U∩V∈?B" using inter_two_intervals assms by auto

}

moreover

{

assume "U∈?L"

with S obtain bu bv cv where A:"U=LeftRayX(X, r,bu)""V=IntervalX(X,r,bv,cv)""bu∈X""bv∈X""cv∈X"

by auto

then have "SmallerOf(r,bu,cv)∈X" using SmallerOf_def by (cases "⟨bu,cv⟩∈r",auto)

with A have "U∩V∈?B" using inter_lray_interval assms by auto

}

moreover

{

assume "U∈?R"

with S obtain cu bv cv where A:"U=RightRayX(X,r,cu)""V=IntervalX(X,r,bv,cv)""cu∈X""bv∈X""cv∈X"

by auto

then have "GreaterOf(r,cu,bv)∈X" using GreaterOf_def by (cases "⟨cu,bv⟩∈r",auto)

with A have "U∩V∈?B" using inter_rray_interval assms by auto

}

ultimately have "U∩V∈?B" using dU by auto

}

moreover

{

assume S:"V∈?L"

{

assume "U∈?I"

with S obtain bu bv cv where A:"V=LeftRayX(X, r,bu)""U=IntervalX(X,r,bv,cv)""bu∈X""bv∈X""cv∈X"

by auto

then have "SmallerOf(r,bu,cv)∈X" using SmallerOf_def by (cases "⟨bu,cv⟩∈r", auto)

have "U∩V=V∩U" by auto

with A `SmallerOf(r,bu,cv)∈X` have "U∩V∈?B" using inter_lray_interval assms by auto

}

moreover

{

assume "U∈?R"

with S obtain bu cv where A:"V=LeftRayX(X,r,bu)""U=RightRayX(X,r,cv)""bu∈X""cv∈X"

by auto

have "U∩V=V∩U" by auto

with A have "U∩V∈?B" using inter_lray_rray assms by auto

}

moreover

{

assume "U∈?L"

with S obtain bu bv where A:"U=LeftRayX(X,r,bu)""V=LeftRayX(X,r,bv)""bu∈X""bv∈X"

by auto

then have "SmallerOf(r,bu,bv)∈X" using SmallerOf_def by (cases "⟨bu,bv⟩∈r", auto)

with A have "U∩V∈?B" using inter_lray_lray assms by auto

}

ultimately have "U∩V∈?B" using dU by auto

}

moreover

{

assume S:"V∈?R"

{

assume "U∈?I"

with S obtain cu bv cv where A:"V=RightRayX(X,r,cu)""U=IntervalX(X,r,bv,cv)""cu∈X""bv∈X""cv∈X"

by auto

then have "GreaterOf(r,cu,bv)∈X" using GreaterOf_def by (cases "⟨cu,bv⟩∈r",auto)

have "U∩V=V∩U" by auto

with A `GreaterOf(r,cu,bv)∈X` have "U∩V∈?B" using inter_rray_interval assms by auto

}

moreover

{

assume "U∈?L"

with S obtain bu cv where A:"U=LeftRayX(X,r,bu)""V=RightRayX(X,r,cv)""bu∈X""cv∈X"

by auto

then have "U∩V∈?B" using inter_lray_rray assms by auto

}

moreover

{

assume "U∈?R"

with S obtain cu cv where A:"U=RightRayX(X,r,cu)""V=RightRayX(X,r,cv)""cu∈X""cv∈X"

by auto

then have "GreaterOf(r,cu,cv)∈X" using GreaterOf_def by (cases "⟨cu,cv⟩∈r",auto)

with A have "U∩V∈?B" using inter_rray_rray assms by auto

}

ultimately have "U∩V∈?B" using dU by auto

}

ultimately have S:"U∩V∈?B" using dV by auto

{

fix x

assume "x∈U∩V"

then have "x∈U∩V∧U∩V⊆U∩V" by auto

then have "∃W. W∈(?B)∧ x∈W ∧ W ⊆ U∩V" using S by blast

then have "∃W∈(?B). x∈W ∧ W ⊆ U∩V" by blast

}

hence "(∀x ∈ U∩V. ∃W∈(?B). x∈W ∧ W ⊆ U∩V)" by auto

}

then show ?thesis using SatisfiesBaseCondition_def by auto

qed

text{*Since the intervals and rays form a base of a topology, and this topology

is uniquely determined; we can built it. In the definition

we have to make sure that we have a totally ordered set.*}

definition

OrderTopology ("OrdTopology _ _" 50) where

"IsLinOrder(X,r) ==> OrdTopology X r ≡ TopologyBase {IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X}"

theorem Ordtopology_is_a_topology:

assumes "IsLinOrder(X,r)"

shows "(OrdTopology X r) {is a topology}" and "{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X} {is a base for} (OrdTopology X r)"

using assms Base_topology_is_a_topology intervals_rays_base_condition

OrderTopology_def by auto

lemma topology0_ordtopology:

assumes "IsLinOrder(X,r)"

shows "topology0(OrdTopology X r)"

using Ordtopology_is_a_topology topology0_def assms by auto

subsection{*Total set*}

text{*The topology is defined in the set $X$, when $X$ has more than

one point*}

lemma union_ordtopology:

assumes "IsLinOrder(X,r)""∃x y. x≠y ∧ x∈X∧ y∈X"

shows "\<Union>(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∈\<Union>?B" using T by auto

then have x:"x∈\<Union>(OrdTopology X r)" using Top_1_2_L5 base by auto

{

fix z

assume z:"z∈X"

{

assume "x=z"

then have "z∈\<Union>(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∈\<Union>?B" by auto

then have "z∈\<Union>(OrdTopology X r)" using Top_1_2_L5 base by auto

}

ultimately have "z∈\<Union>(OrdTopology X r)" by auto

}

then show "X⊆\<Union>(OrdTopology X r)" by auto

have "\<Union>?B⊆X" using IntervalX_def LeftRayX_def RightRayX_def by auto

then show "\<Union>(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 "\<Union>(LOrdTopology X r)=X" and "\<Union>(ROrdTopology X r)=X"

using Top_1_2_L5[OF LOrdtopology_ROrdtopology_are_topologies(2)[OF assms]]

Top_1_2_L5[OF LOrdtopology_ROrdtopology_are_topologies(4)[OF assms]]

unfolding LeftRayX_def RightRayX_def by auto

section{*Union of Topologies*}

text{*The union of two topologies is not a topology. A way to

overcome this fact is to define the following topology: *}

definition

joinT ("joinT _" 90) where

"(∀T∈M. T{is a topology} ∧ (∀Q∈M. \<Union>Q=\<Union>T)) ==> (joinT M ≡ THE T. (\<Union>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 "{\<Inter>A. A ∈ FinPow(B)} {satisfies the base condition}"

proof-

{

fix U V

assume A:"U∈{\<Inter>A. A ∈ FinPow(B)} ∧ V∈{\<Inter>A. A ∈ FinPow(B)}"

then obtain M R where MR:"Finite(M)""Finite(R)""M⊆B""R⊆B"

"U=\<Inter>M""V=\<Inter>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 "\<Inter>(M∪R)∈{\<Inter>A. A ∈ FinPow(B)}" by auto

moreover

from N have "\<Inter>(M∪R)⊆\<Inter>M""\<Inter>(M∪R)⊆\<Inter>R" by auto

then have "\<Inter>(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∈\<Inter>(M ∪ R)" using N by auto

ultimately have "∃W∈{\<Inter>A. A ∈ FinPow(B)}. x∈W∧W⊆U∩V" by blast

}

then have "(∀x ∈ U∩V. ∃W∈{\<Inter>A. A ∈ FinPow(B)}. x∈W ∧ W ⊆ U∩V)" by auto

}

then have "∀U V. ((U∈{\<Inter>A. A ∈ FinPow(B)} ∧ V∈{\<Inter>A. A ∈ FinPow(B)}) -->

(∀x ∈ U∩V. ∃W∈{\<Inter>A. A ∈ FinPow(B)}. x∈W ∧ W ⊆ U∩V))" by auto

then show "{\<Inter>A. A ∈ FinPow(B)} {satisfies the base condition}"

using SatisfiesBaseCondition_def by auto

qed

theorem Top_subbase:

assumes "T = {\<Union>A. A∈Pow({\<Inter>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)""\<Inter>{S}=S" using FinPow_def by auto

then have "{S}∈Pow({\<Inter>A. A ∈ FinPow(B)})" by (blast+)

then have "\<Union>{S}∈{\<Union>A. A∈Pow({\<Inter>A. A ∈ FinPow(B)})}" by blast

then have "S∈{\<Union>A. A∈Pow({\<Inter>A. A ∈ FinPow(B)})}" by auto

then have "S∈T" using assms by auto

}

then have "B⊆T" by auto

moreover

have "{\<Inter>A. A ∈ FinPow(B)} {satisfies the base condition}"

using subset_as_subbase by auto

then have "T {is a topology}" and "{\<Inter>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