Theory Topology_ZF_examples_1
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 satisfying the base condition,
it is possible to construct a topology where that family is a base of. Even more,
it is the only topology with such characteristics.›
definition
TopologyWithBase ("TopologyBase _ " 50) where
"U {satisfies the base condition} ⟹ TopologyBase U ≡ THE T. U {is a base for} T"
text‹ If a collection $U$ of sets satisfies the base condition then the topology
constructed from it is indeed a topology and $U$ is a base for this topology. ›
theorem Base_topology_is_a_topology:
assumes "U {satisfies the base condition}"
shows "(TopologyBase U) {is a topology}" and "U {is a base for} (TopologyBase U)"
proof-
from assms obtain T where "U {is a base for} T" using
Top_1_2_T1(2) by blast
then have "∃!T. U {is a base for} T" using same_base_same_top ex1I[where P=
"λT. U {is a base for} T"] by blast
with assms show "U {is a base for} (TopologyBase U) " using theI[where P=
"λT. U {is a base for} T"] TopologyWithBase_def by auto
with assms show "(TopologyBase U) {is a topology}" using Top_1_2_T1(1)
IsAbaseFor_def by auto
qed
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
ultimately show "⋃{T∈U. T⊆A} ⊆ Interior(A,T)"
using assms(2) topology0.Top_2_L5 topology0_def by auto
{
fix x
assume "x ∈ Interior(A,T)"
with assms obtain V where "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 auto
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
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
ultimately have "x∈Closure(A,Q)" using assms(2,3) 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 -
from assms have "(B {restricted to} Y) ⊆ (T {restricted to} Y)"
unfolding IsAbaseFor_def RestrictedTo_def by auto
moreover have "(T {restricted to} Y) = {⋃A. A ∈ Pow(B {restricted to} Y)}"
proof
{ fix U assume "U ∈ (T {restricted to} Y)"
then obtain W where "W∈T" and "U = W∩Y" unfolding RestrictedTo_def by blast
with assms obtain C where "C∈Pow(B)" and "W=⋃C" unfolding IsAbaseFor_def
by blast
let ?A="{V∩Y. V∈C}"
from ‹C∈Pow(B)› ‹U = W∩Y› ‹W=⋃C› have
"?A ∈ Pow(B {restricted to} Y)" and "U=(⋃?A)"
unfolding RestrictedTo_def by auto
hence "U ∈ {⋃A. A ∈ Pow(B {restricted to} Y)}" by blast
} thus "(T {restricted to} Y) ⊆ {⋃A. A ∈ Pow(B {restricted to} Y)}"
by auto
{ fix U assume "U ∈ {⋃A. A ∈ Pow(B {restricted to} Y)}"
then obtain A where A: "A ⊆ (B {restricted to} Y)" and "U = (⋃A)" by auto
let ?A⇩0="{C∈B. Y∩C∈A}"
from A have "?A⇩0 ⊆ B" and "A = ?A⇩0 {restricted to} Y" unfolding RestrictedTo_def
by auto
with ‹U = (⋃A)› have "?A⇩0 ⊆ B" and "U = ⋃(?A⇩0 {restricted to} Y)"
by auto
with assms have "U ∈ (T {restricted to} Y)" unfolding RestrictedTo_def IsAbaseFor_def
by auto
} thus "{⋃A. A ∈ Pow(B {restricted to} Y)} ⊆ (T {restricted to} Y)" by blast
qed
ultimately show ?thesis unfolding IsAbaseFor_def by simp
qed
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.›
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