Theory Topology_ZF_11
section ‹Topology 11›
theory Topology_ZF_11 imports Topology_ZF_7 Finite_ZF_1
begin
text‹This file deals with order topologies. The order topology
is already defined in @{file "Topology_ZF_examples_1.thy"}.›
subsection‹Order topologies›
text‹We will assume
most of the time that the ordered set has more than one point.
It is natural to think that the topological properties
can be translated to properties of the order; since every
order rises one and only one topology in a set.›
subsection‹Separation properties›
text‹Order topologies have a lot of separation properties.›
text‹Every order topology is Hausdorff.›
theorem order_top_T2:
assumes "IsLinOrder(X,r)" "∃x y. x≠y∧x∈X∧y∈X"
shows "(OrdTopology X r){is T⇩2}"
proof-
{
fix x y assume A1:"x∈⋃(OrdTopology X r)""y∈⋃(OrdTopology X r)""x≠y"
then have AS:"x∈X""y∈X""x≠y" using union_ordtopology[OF assms(1) assms(2)] by auto
{
assume A2:"∃z∈X-{x,y}. (⟨x,y⟩∈r⟶⟨x,z⟩∈r∧⟨z,y⟩∈r)∧(⟨y,x⟩∈r⟶⟨y,z⟩∈r∧⟨z,x⟩∈r)"
from AS(1,2) assms(1) have "⟨x,y⟩∈r∨⟨y,x⟩∈r" unfolding IsLinOrder_def IsTotal_def by auto moreover
{
assume "⟨x,y⟩∈r"
with AS A2 obtain z where z:"⟨x,z⟩∈r""⟨z,y⟩∈r""z∈X""z≠x""z≠y" by auto
with AS(1,2) have "x∈LeftRayX(X,r,z)""y∈RightRayX(X,r,z)" unfolding LeftRayX_def RightRayX_def
by auto moreover
have "LeftRayX(X,r,z)∩RightRayX(X,r,z)=0" using inter_lray_rray[OF z(3) z(3) assms(1)]
unfolding IntervalX_def using Order_ZF_2_L4[OF total_is_refl _ z(3)] assms(1) unfolding IsLinOrder_def
by auto moreover
have "LeftRayX(X,r,z)∈(OrdTopology X r)""RightRayX(X,r,z)∈(OrdTopology X r)"
using z(3) base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] by auto
ultimately have "∃U∈(OrdTopology X r). ∃V∈(OrdTopology X r). x∈U ∧ y∈V ∧ U∩V=0" by auto
}
moreover
{
assume "⟨y,x⟩∈r"
with AS A2 obtain z where z:"⟨y,z⟩∈r""⟨z,x⟩∈r""z∈X""z≠x""z≠y" by auto
with AS(1,2) have "y∈LeftRayX(X,r,z)""x∈RightRayX(X,r,z)" unfolding LeftRayX_def RightRayX_def
by auto moreover
have "LeftRayX(X,r,z)∩RightRayX(X,r,z)=0" using inter_lray_rray[OF z(3) z(3) assms(1)]
unfolding IntervalX_def using Order_ZF_2_L4[OF total_is_refl _ z(3)] assms(1) unfolding IsLinOrder_def
by auto moreover
have "LeftRayX(X,r,z)∈(OrdTopology X r)""RightRayX(X,r,z)∈(OrdTopology X r)"
using z(3) base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] by auto
ultimately have "∃U∈(OrdTopology X r). ∃V∈(OrdTopology X r). x∈U ∧ y∈V ∧ U∩V=0" by auto
}
ultimately have "∃U∈(OrdTopology X r). ∃V∈(OrdTopology X r). x∈U ∧ y∈V ∧ U∩V=0" by auto
}
moreover
{
assume A2:"∀z∈X - {x, y}. (⟨x, y⟩ ∈ r ∧ (⟨x, z⟩ ∉ r ∨ ⟨z, y⟩ ∉ r)) ∨ (⟨y, x⟩ ∈ r ∧ (⟨y, z⟩ ∉ r ∨ ⟨z, x⟩ ∉ r))"
from AS(1,2) assms(1) have disj:"⟨x,y⟩∈r∨⟨y,x⟩∈r" unfolding IsLinOrder_def IsTotal_def by auto moreover
{
assume TT:"⟨x,y⟩∈r"
with AS assms(1) have T:"⟨y,x⟩∉r" unfolding IsLinOrder_def antisym_def by auto
from TT AS(1-3) have "x∈LeftRayX(X,r,y)""y∈RightRayX(X,r,x)" unfolding LeftRayX_def RightRayX_def
by auto moreover
{
fix z assume "z∈LeftRayX(X,r,y)∩RightRayX(X,r,x)"
then have "⟨z,y⟩∈r""⟨x,z⟩∈r""z∈X-{x,y}" unfolding RightRayX_def LeftRayX_def by auto
with A2 T have "False" by auto
}
then have "LeftRayX(X,r,y)∩RightRayX(X,r,x)=0" by auto moreover
have "LeftRayX(X,r,y)∈(OrdTopology X r)""RightRayX(X,r,x)∈(OrdTopology X r)"
using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] AS by auto
ultimately have "∃U∈(OrdTopology X r). ∃V∈(OrdTopology X r). x∈U ∧ y∈V ∧ U∩V=0" by auto
}
moreover
{
assume TT:"⟨y,x⟩∈r"
with AS assms(1) have T:"⟨x,y⟩∉r" unfolding IsLinOrder_def antisym_def by auto
from TT AS(1-3) have "y∈LeftRayX(X,r,x)""x∈RightRayX(X,r,y)" unfolding LeftRayX_def RightRayX_def
by auto moreover
{
fix z assume "z∈LeftRayX(X,r,x)∩RightRayX(X,r,y)"
then have "⟨z,x⟩∈r""⟨y,z⟩∈r""z∈X-{x,y}" unfolding RightRayX_def LeftRayX_def by auto
with A2 T have "False" by auto
}
then have "LeftRayX(X,r,x)∩RightRayX(X,r,y)=0" by auto moreover
have "LeftRayX(X,r,x)∈(OrdTopology X r)""RightRayX(X,r,y)∈(OrdTopology X r)"
using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] AS by auto
ultimately have "∃U∈(OrdTopology X r). ∃V∈(OrdTopology X r). x∈U ∧ y∈V ∧ U∩V=0" by auto
}
ultimately have "∃U∈(OrdTopology X r). ∃V∈(OrdTopology X r). x∈U ∧ y∈V ∧ U∩V=0" by auto
}
ultimately have "∃U∈(OrdTopology X r). ∃V∈(OrdTopology X r). x∈U ∧ y∈V ∧ U∩V=0" by auto
}
then show ?thesis unfolding isT2_def by auto
qed
text‹Every order topology is $T_4$, but the proof needs lots of machinery.
At the end of the file, we will prove that every order topology is normal; sooner
or later.›
subsection‹Connectedness properties›
text‹Connectedness is related to two properties of orders: completeness and density›
text‹Some order-dense properties:›
definition
IsDenseSub ("_ {is dense in}_{with respect to}_") where
"A {is dense in}X{with respect to}r ≡
∀x∈X. ∀y∈X. ⟨x,y⟩∈r ∧ x≠y ⟶ (∃z∈A-{x,y}. ⟨x,z⟩∈r∧⟨z,y⟩∈r)"
definition
IsDenseUnp ("_ {is not-properly dense in}_{with respect to}_") where
"A {is not-properly dense in}X{with respect to}r ≡
∀x∈X. ∀y∈X. ⟨x,y⟩∈r ∧ x≠y ⟶ (∃z∈A. ⟨x,z⟩∈r∧⟨z,y⟩∈r)"
definition
IsWeaklyDenseSub ("_ {is weakly dense in}_{with respect to}_") where
"A {is weakly dense in}X{with respect to}r ≡
∀x∈X. ∀y∈X. ⟨x,y⟩∈r ∧ x≠y ⟶ ((∃z∈A-{x,y}. ⟨x,z⟩∈r∧⟨z,y⟩∈r)∨ IntervalX(X,r,x,y)=0)"
definition
IsDense ("_ {is dense with respect to}_") where
"X {is dense with respect to}r ≡
∀x∈X. ∀y∈X. ⟨x,y⟩∈r ∧ x≠y ⟶ (∃z∈X-{x,y}. ⟨x,z⟩∈r∧⟨z,y⟩∈r)"
lemma dense_sub:
shows "(X {is dense with respect to}r) ⟷ (X {is dense in}X{with respect to}r)"
unfolding IsDenseSub_def IsDense_def by auto
lemma not_prop_dense_sub:
shows "(A {is dense in}X{with respect to}r) ⟶ (A {is not-properly dense in}X{with respect to}r)"
unfolding IsDenseSub_def IsDenseUnp_def by auto
text‹In densely ordered sets, intervals are infinite.›
theorem dense_order_inf_intervals:
assumes "IsLinOrder(X,r)" "IntervalX(X, r, b, c)≠0""b∈X""c∈X" "X{is dense with respect to}r"
shows "¬Finite(IntervalX(X, r, b, c))"
proof
assume fin:"Finite(IntervalX(X, r, b, c))"
have sub:"IntervalX(X, r, b, c)⊆X" unfolding IntervalX_def by auto
have p:"Minimum(r,IntervalX(X, r, b, c))∈IntervalX(X, r, b, c)" using Finite_ZF_1_T2(2)[OF assms(1) Finite_Fin[OF fin sub] assms(2)]
by auto
then have "⟨b,Minimum(r,IntervalX(X, r, b, c))⟩∈r""b≠Minimum(r,IntervalX(X, r, b, c))"
unfolding IntervalX_def using Order_ZF_2_L1 by auto
with assms(3,5) sub p obtain z1 where z1:"z1∈X""z1≠b""z1≠Minimum(r,IntervalX(X, r, b, c))""⟨b,z1⟩∈r""⟨z1,Minimum(r,IntervalX(X, r, b, c))⟩∈r"
unfolding IsDense_def by blast
from p have B:"⟨Minimum(r,IntervalX(X, r, b, c)),c⟩∈r" unfolding IntervalX_def using Order_ZF_2_L1 by auto moreover
have "trans(r)" using assms(1) unfolding IsLinOrder_def by auto moreover
note z1(5) ultimately have z1a:"⟨z1,c⟩∈r" unfolding trans_def by fast
{
assume "z1=c"
with B have "⟨Minimum(r,IntervalX(X, r, b, c)),z1⟩∈r" by auto
with z1(5) have "z1=Minimum(r,IntervalX(X, r, b, c))" using assms(1) unfolding IsLinOrder_def antisym_def by auto
then have "False" using z1(3) by auto
}
then have "z1≠c" by auto
with z1(1,2,4) z1a have "z1∈IntervalX(X, r, b, c)" unfolding IntervalX_def using Order_ZF_2_L1 by auto
then have "⟨Minimum(r,IntervalX(X, r, b, c)),z1⟩∈r" using Finite_ZF_1_T2(4)[OF assms(1) Finite_Fin[OF fin sub] assms(2)] by auto
with z1(5) have "z1=Minimum(r,IntervalX(X, r, b, c))" using assms(1) unfolding IsLinOrder_def antisym_def by auto
with z1(3) show "False" by auto
qed
text‹Left rays are infinite.›
theorem dense_order_inf_lrays:
assumes "IsLinOrder(X,r)" "LeftRayX(X,r,c)≠0""c∈X" "X{is dense with respect to}r"
shows "¬Finite(LeftRayX(X,r,c))"
proof-
from assms(2) obtain b where "b∈X""⟨b,c⟩∈r""b≠c" unfolding LeftRayX_def by auto
with assms(3) obtain z where "z∈X-{b,c}""⟨b,z⟩∈r""⟨z,c⟩∈r" using assms(4) unfolding IsDense_def by auto
then have "IntervalX(X, r, b, c)≠0" unfolding IntervalX_def using Order_ZF_2_L1 by auto
then have nFIN:"¬Finite(IntervalX(X, r, b, c))" using dense_order_inf_intervals[OF assms(1) _ _ assms(3,4)]
‹b∈X› by auto
{
fix d assume "d∈IntervalX(X, r, b, c)"
then have "⟨b,d⟩∈r""⟨d,c⟩∈r""d∈X""d≠b""d≠c" unfolding IntervalX_def using Order_ZF_2_L1 by auto
then have "d∈LeftRayX(X,r,c)" unfolding LeftRayX_def by auto
}
then have "IntervalX(X, r, b, c)⊆LeftRayX(X,r,c)" by auto
with nFIN show ?thesis using subset_Finite by auto
qed
text‹Right rays are infinite.›
theorem dense_order_inf_rrays:
assumes "IsLinOrder(X,r)" "RightRayX(X,r,b)≠0""b∈X" "X{is dense with respect to}r"
shows "¬Finite(RightRayX(X,r,b))"
proof-
from assms(2) obtain c where "c∈X""⟨b,c⟩∈r""b≠c" unfolding RightRayX_def by auto
with assms(3) obtain z where "z∈X-{b,c}""⟨b,z⟩∈r""⟨z,c⟩∈r" using assms(4) unfolding IsDense_def by auto
then have "IntervalX(X, r, b, c)≠0" unfolding IntervalX_def using Order_ZF_2_L1 by auto
then have nFIN:"¬Finite(IntervalX(X, r, b, c))" using dense_order_inf_intervals[OF assms(1) _ assms(3) _ assms(4)]
‹c∈X› by auto
{
fix d assume "d∈IntervalX(X, r, b, c)"
then have "⟨b,d⟩∈r""⟨d,c⟩∈r""d∈X""d≠b""d≠c" unfolding IntervalX_def using Order_ZF_2_L1 by auto
then have "d∈RightRayX(X,r,b)" unfolding RightRayX_def by auto
}
then have "IntervalX(X, r, b, c)⊆RightRayX(X,r,b)" by auto
with nFIN show ?thesis using subset_Finite by auto
qed
text‹The whole space in a densely ordered set is infinite.›
corollary dense_order_infinite:
assumes "IsLinOrder(X,r)" "X{is dense with respect to}r"
"∃x y. x≠y∧x∈X∧y∈X"
shows "¬(X≺nat)"
proof-
from assms(3) obtain b c where B:"b∈X""c∈X""b≠c" by auto
{
assume "⟨b,c⟩∉r"
with assms(1) have "⟨c,b⟩∈r" unfolding IsLinOrder_def IsTotal_def using ‹b∈X›‹c∈X› by auto
with assms(2) B obtain z where "z∈X-{b,c}""⟨c,z⟩∈r""⟨z,b⟩∈r" unfolding IsDense_def by auto
then have "IntervalX(X,r,c,b)≠0" unfolding IntervalX_def using Order_ZF_2_L1 by auto
then have "¬(Finite(IntervalX(X,r,c,b)))" using dense_order_inf_intervals[OF assms(1) _ ‹c∈X›‹b∈X› assms(2)]
by auto moreover
have "IntervalX(X,r,c,b)⊆X" unfolding IntervalX_def by auto
ultimately have "¬(Finite(X))" using subset_Finite by auto
then have "¬(X≺nat)" using lesspoll_nat_is_Finite by auto
}
moreover
{
assume "⟨b,c⟩∈r"
with assms(2) B obtain z where "z∈X-{b,c}""⟨b,z⟩∈r""⟨z,c⟩∈r" unfolding IsDense_def by auto
then have "IntervalX(X,r,b,c)≠0" unfolding IntervalX_def using Order_ZF_2_L1 by auto
then have "¬(Finite(IntervalX(X,r,b,c)))" using dense_order_inf_intervals[OF assms(1) _ ‹b∈X›‹c∈X› assms(2)]
by auto moreover
have "IntervalX(X,r,b,c)⊆X" unfolding IntervalX_def by auto
ultimately have "¬(Finite(X))" using subset_Finite by auto
then have "¬(X≺nat)" using lesspoll_nat_is_Finite by auto
}
ultimately show ?thesis by auto
qed
text‹If an order topology is connected, then the order is complete.
It is equivalent to assume that $r\subseteq X\times X$ or prove that
$r\cap X\times X$ is complete.›
theorem conn_imp_complete:
assumes "IsLinOrder(X,r)" "∃x y. x≠y∧x∈X∧y∈X" "r⊆X×X"
"(OrdTopology X r){is connected}"
shows "r{is complete}"
proof-
{
assume "¬(r{is complete})"
then obtain A where A:"A≠0""IsBoundedAbove(A,r)""¬(HasAminimum(r, ⋂b∈A. r `` {b}))" unfolding
IsComplete_def by auto
from A(3) have r1:"∀m∈⋂b∈A. r `` {b}. ∃x∈⋂b∈A. r `` {b}. ⟨m,x⟩∉r" unfolding HasAminimum_def
by force
from A(1,2) obtain b where r2:"∀x∈A. ⟨x, b⟩ ∈ r" unfolding IsBoundedAbove_def by auto
with assms(3) A(1) have "A⊆X""b∈X" by auto
with assms(3) have r3:"∀c∈A. r `` {c}⊆X" using image_iff by auto
from r2 have "∀x∈A. b∈r``{x}" using image_iff by auto
then have noE:"b∈(⋂b∈A. r `` {b})" using A(1) by auto
{
fix x assume "x∈(⋂b∈A. r `` {b})"
then have "∀c∈A. x∈r``{c}" by auto
with A(1) obtain c where "c∈A" "x∈r``{c}" by auto
with r3 have "x∈X" by auto
}
then have sub:"(⋂b∈A. r `` {b})⊆X" by auto
{
fix x assume x:"x∈(⋂b∈A. r `` {b})"
with r1 have "∃z∈⋂b∈A. r `` {b}. ⟨x,z⟩∉r" by auto
then obtain z where z:"z∈(⋂b∈A. r `` {b})""⟨x,z⟩∉r" by auto
from x z(1) sub have "x∈X""z∈X" by auto
with z(2) have "⟨z,x⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def by auto
then have xx:"x∈RightRayX(X,r,z)" unfolding RightRayX_def using ‹x∈X›‹⟨x,z⟩∉r›
assms(1) unfolding IsLinOrder_def using total_is_refl unfolding refl_def by auto
{
fix m assume "m∈RightRayX(X,r,z)"
then have m:"m∈X-{z}""⟨z,m⟩∈r" unfolding RightRayX_def by auto
{
fix c assume "c∈A"
with z(1) have "⟨c,z⟩∈r" using image_iff by auto
with m(2) have "⟨c,m⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
then have "m∈r``{c}" using image_iff by auto
}
with A(1) have "m∈(⋂b∈A. r `` {b})" by auto
}
then have sub1:"RightRayX(X,r,z)⊆(⋂b∈A. r `` {b})" by auto
have "RightRayX(X,r,z)∈(OrdTopology X r)" using
base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] ‹z∈X› by auto
with sub1 xx have "∃U∈(OrdTopology X r). x∈U ∧ U⊆(⋂b∈A. r `` {b})" by auto
}
then have "(⋂b∈A. r `` {b})∈(OrdTopology X r)" using topology0.open_neigh_open[OF topology0_ordtopology[OF assms(1)]]
by auto moreover
{
fix x assume "x∈X-(⋂b∈A. r `` {b})"
then have "x∈X""x∉(⋂b∈A. r `` {b})" by auto
with A(1) obtain b where "x∉r``{b}""b∈A" by auto
then have "⟨b,x⟩∉r" using image_iff by auto
with ‹A⊆X› ‹b∈A›‹x∈X› have "⟨x,b⟩∈r" using assms(1) unfolding IsLinOrder_def
IsTotal_def by auto
then have xx:"x∈LeftRayX(X,r,b)" unfolding LeftRayX_def using ‹x∈X› ‹⟨b,x⟩∉r›
assms(1) unfolding IsLinOrder_def using total_is_refl unfolding refl_def by auto
{
fix y assume "y∈LeftRayX(X,r,b)∩(⋂b∈A. r `` {b})"
then have "y∈X-{b}""⟨y,b⟩∈r""∀c∈A. y∈r``{c}" unfolding LeftRayX_def by auto
then have "y∈X""⟨y,b⟩∈r""∀c∈A. ⟨c,y⟩∈r" using image_iff by auto
with ‹b∈A› have "y=b" using assms(1) unfolding IsLinOrder_def antisym_def by auto
then have "False" using ‹y∈X-{b}› by auto
}
then have sub1:"LeftRayX(X,r,b)⊆X-(⋂b∈A. r `` {b})" unfolding LeftRayX_def by auto
have "LeftRayX(X,r,b)∈(OrdTopology X r)" using
base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] ‹b∈A›‹A⊆X› by blast
with sub1 xx have "∃U∈(OrdTopology X r). x∈U∧U⊆X-(⋂b∈A. r `` {b})" by auto
}
then have "X - (⋂b∈A. r `` {b})∈(OrdTopology X r)" using topology0.open_neigh_open[OF topology0_ordtopology[OF assms(1)]]
by auto
then have "⋃(OrdTopology X r)-(⋂b∈A. r `` {b})∈(OrdTopology X r)" using union_ordtopology[OF assms(1,2)] by auto
then have "(⋂b∈A. r `` {b}){is closed in}(OrdTopology X r)" unfolding IsClosed_def using union_ordtopology[OF assms(1,2)]
sub by auto
moreover note assms(4) ultimately
have "(⋂b∈A. r `` {b})=0∨(⋂b∈A. r `` {b})=X" using union_ordtopology[OF assms(1,2)] unfolding IsConnected_def
by auto
then have e1:"(⋂b∈A. r `` {b})=X" using noE by auto
then have "∀x∈X. ∀b∈A. x∈r``{b}" by auto
then have r4:"∀x∈X. ∀b∈A. ⟨b,x⟩∈r" using image_iff by auto
{
fix a1 a2 assume aA:"a1∈A""a2∈A""a1≠a2"
with ‹A⊆X› have aX:"a1∈X""a2∈X" by auto
with r4 aA(1,2) have "⟨a1,a2⟩∈r""⟨a2,a1⟩∈r" by auto
then have "a1=a2" using assms(1) unfolding IsLinOrder_def antisym_def by auto
with aA(3) have "False" by auto
}
moreover
from A(1) obtain t where "t∈A" by auto
ultimately have "A={t}" by auto
with r4 have "∀x∈X. ⟨t,x⟩∈r""t∈X" using ‹A⊆X› by auto
then have "HasAminimum(r,X)" unfolding HasAminimum_def by auto
with e1 have "HasAminimum(r,⋂b∈A. r `` {b})" by auto
with A(3) have "False" by auto
}
then show ?thesis by auto
qed
text‹If an order topology is connected, then the order is dense.›
theorem conn_imp_dense:
assumes "IsLinOrder(X,r)" "∃x y. x≠y∧x∈X∧y∈X"
"(OrdTopology X r){is connected}"
shows "X {is dense with respect to}r"
proof-
{
assume "¬(X {is dense with respect to}r)"
then have "∃x1∈X. ∃x2∈X. ⟨x1,x2⟩∈r∧x1≠x2∧(∀z∈X-{x1,x2}. ⟨x1,z⟩∉r∨⟨z,x2⟩∉r)"
unfolding IsDense_def by auto
then obtain x1 x2 where x:"x1∈X""x2∈X""⟨x1,x2⟩∈r""x1≠x2""(∀z∈X-{x1,x2}. ⟨x1,z⟩∉r∨⟨z,x2⟩∉r)" by auto
from x(1,2) have P:"LeftRayX(X,r,x2)∈(OrdTopology X r)""RightRayX(X,r,x1)∈(OrdTopology X r)"
using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] by auto
{
fix x assume "x∈X-LeftRayX(X,r,x2)"
then have "x∈X" "x∉LeftRayX(X,r,x2)" by auto
then have "⟨x,x2⟩∉r∨x=x2" unfolding LeftRayX_def by auto
then have "⟨x2,x⟩∈r∨x=x2" using assms(1) ‹x∈X› ‹x2∈X› unfolding IsLinOrder_def
IsTotal_def by auto
then have s:"⟨x2,x⟩∈r" using assms(1) unfolding IsLinOrder_def using total_is_refl ‹x2∈X›
unfolding refl_def by auto
with x(3) have "⟨x1,x⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
then have "x=x1∨x∈RightRayX(X,r,x1)" unfolding RightRayX_def using ‹x∈X› by auto
with s have "⟨x2,x1⟩∈r∨x∈RightRayX(X,r,x1)" by auto
with x(3) have "x1=x2 ∨ x∈RightRayX(X,r,x1)" using assms(1) unfolding IsLinOrder_def
antisym_def by auto
with x(4) have "x∈RightRayX(X,r,x1)" by auto
}
then have "X-LeftRayX(X,r,x2)⊆RightRayX(X,r,x1)" by auto moreover
{
fix x assume "x∈RightRayX(X,r,x1)"
then have xr:"x∈X-{x1}""⟨x1,x⟩∈r" unfolding RightRayX_def by auto
{
assume "x∈LeftRayX(X,r,x2)"
then have xl:"x∈X-{x2}""⟨x,x2⟩∈r" unfolding LeftRayX_def by auto
from xl xr x(5) have "False" by auto
}
with xr(1) have "x∈X-LeftRayX(X,r,x2)" by auto
}
ultimately have "RightRayX(X,r,x1)=X-LeftRayX(X,r,x2)" by auto
then have "LeftRayX(X,r,x2){is closed in}(OrdTopology X r)" using P(2) union_ordtopology[
OF assms(1,2)] unfolding IsClosed_def LeftRayX_def by auto
with P(1) have "LeftRayX(X,r,x2)=0∨LeftRayX(X,r,x2)=X" using union_ordtopology[
OF assms(1,2)] assms(3) unfolding IsConnected_def by auto
with x(1,3,4) have "LeftRayX(X,r,x2)=X" unfolding LeftRayX_def by auto
then have "x2∈LeftRayX(X,r,x2)" using x(2) by auto
then have "False" unfolding LeftRayX_def by auto
}
then show ?thesis by auto
qed
text‹Actually a connected order topology is one that comes from a dense
and complete order.›
text‹First a lemma. In a complete ordered set, every non-empty set bounded from below has
a maximum lower bound.›
lemma complete_order_bounded_below:
assumes "r{is complete}" "IsBoundedBelow(A,r)" "A≠0" "r⊆X×X"
shows "HasAmaximum(r,⋂c∈A. r-``{c})"
proof-
let ?M="⋂c∈A. r-``{c}"
from assms(3) obtain t where A:"t∈A" by auto
{
fix m assume "m∈?M"
with A have "m∈r-``{t}" by auto
then have "⟨m,t⟩∈r" by auto
}
then have "(∀x∈⋂c∈A. r -`` {c}. ⟨x, t⟩ ∈ r)" by auto
then have "IsBoundedAbove(?M,r)" unfolding IsBoundedAbove_def by auto
moreover
from assms(2,3) obtain l where " ∀x∈A. ⟨l, x⟩ ∈ r" unfolding IsBoundedBelow_def by auto
then have "∀x∈A. l ∈ r-``{x}" using vimage_iff by auto
with assms(3) have "l∈?M" by auto
then have "?M≠0" by auto moreover note assms(1)
ultimately have "HasAminimum(r,⋂c∈?M. r `` {c})" unfolding IsComplete_def by auto
then obtain rr where rr:"rr∈(⋂c∈?M. r `` {c})" "∀s∈(⋂c∈?M. r `` {c}). ⟨rr,s⟩∈r" unfolding HasAminimum_def
by auto
{
fix aa assume A:"aa∈A"
{
fix c assume M:"c∈?M"
with A have "⟨c,aa⟩∈r" by auto
then have "aa∈r``{c}" by auto
}
then have "aa∈(⋂c∈?M. r `` {c})" using rr(1) by auto
}
then have "A⊆(⋂c∈?M. r `` {c})" by auto
with rr(2) have "∀s∈A. ⟨rr,s⟩∈r" by auto
then have "rr∈?M" using assms(3) by auto
moreover
{
fix m assume "m∈?M"
then have "rr∈r``{m}" using rr(1) by auto
then have "⟨m,rr⟩∈r" by auto
}
then have "∀m∈?M. ⟨m,rr⟩∈r" by auto
ultimately show ?thesis unfolding HasAmaximum_def by auto
qed
theorem comp_dense_imp_conn:
assumes "IsLinOrder(X,r)" "∃x y. x≠y∧x∈X∧y∈X" "r⊆X×X"
"X {is dense with respect to}r" "r{is complete}"
shows "(OrdTopology X r){is connected}"
proof-
{
assume "¬((OrdTopology X r){is connected})"
then obtain U where U:"U≠0""U≠X""U∈(OrdTopology X r)""U{is closed in}(OrdTopology X r)"
unfolding IsConnected_def using union_ordtopology[OF assms(1,2)] by auto
from U(4) have A:"X-U∈(OrdTopology X r)""U⊆X" unfolding IsClosed_def using union_ordtopology[OF assms(1,2)] by auto
from U(1) obtain u where "u∈U" by auto
from A(2) U(1,2) have "X-U≠0" by auto
then obtain v where "v∈X-U" by auto
with ‹u∈U› ‹U⊆X› have "⟨u,v⟩∈r∨⟨v,u⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def
by auto
{
assume "⟨u,v⟩∈r"
have "LeftRayX(X,r,v)∈(OrdTopology X r)" using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]]
‹v∈X-U› by auto
then have "U∩LeftRayX(X,r,v)∈(OrdTopology X r)" using U(3) using Ordtopology_is_a_topology(1)
[OF assms(1)] unfolding IsATopology_def by auto
{
fix b assume "b∈(U)∩LeftRayX(X,r,v)"
then have "⟨b,v⟩∈r" unfolding LeftRayX_def by auto
}
then have bound:"IsBoundedAbove(U∩LeftRayX(X,r,v),r)" unfolding IsBoundedAbove_def by auto moreover
with ‹⟨u,v⟩∈r›‹u∈U›‹U⊆X›‹v∈X-U› have nE:"U∩LeftRayX(X,r,v)≠0" unfolding LeftRayX_def by auto
ultimately have Hmin:"HasAminimum(r,⋂c∈U∩LeftRayX(X,r,v). r``{c})" using assms(5) unfolding IsComplete_def
by auto
let ?min="Supremum(r,U∩LeftRayX(X,r,v))"
{
fix c assume "c∈U∩LeftRayX(X,r,v)"
then have "⟨c,v⟩∈r" unfolding LeftRayX_def by auto
}
then have a1:"⟨?min,v⟩∈r" using Order_ZF_5_L3[OF _ nE Hmin] assms(1) unfolding IsLinOrder_def
by auto
{
assume ass:"?min∈U"
then obtain V where V:"?min∈V""V⊆U"
"V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X}" using point_open_base_neigh
[OF Ordtopology_is_a_topology(2)[OF assms(1)] ‹U∈(OrdTopology X r)› ass] by blast
{
assume "V∈{RightRayX(X,r,b). b∈X}"
then obtain b where b:"b∈X" "V=RightRayX(X,r,b)" by auto
note a1 moreover
from V(1) b(2) have a2:"⟨b,?min⟩∈r""?min≠b" unfolding RightRayX_def by auto
ultimately have "⟨b,v⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by blast moreover
{
assume "b=v"
with a1 a2(1) have "b=?min" using assms(1) unfolding IsLinOrder_def antisym_def by auto
with a2(2) have "False" by auto
}
ultimately have "False" using V(2) b(2) unfolding RightRayX_def using ‹v∈X-U› by auto
}
moreover
{
assume "V∈{LeftRayX(X,r,b). b∈X}"
then obtain b where b:"V=LeftRayX(X,r,b)" "b∈X" by auto
{
assume "⟨v,b⟩∈r"
then have "b=v∨v∈LeftRayX(X,r,b)" unfolding LeftRayX_def using ‹v∈X-U› by auto
then have "b=v" using b(1) V(2) ‹v∈X-U› by auto
}
then have bv:"⟨b,v⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def using b(2)
‹v∈X-U› by auto
from b(1) V(1) have "⟨?min,b⟩∈r""?min≠b" unfolding LeftRayX_def by auto
with assms(4) obtain z where z:"⟨?min,z⟩∈r""⟨z,b⟩∈r""z∈X-{b,?min}" unfolding IsDense_def
using b(2) V(1,2) ‹U⊆X› by blast
then have rayb:"z∈LeftRayX(X,r,b)" unfolding LeftRayX_def by auto
from z(2) bv have "⟨z,v⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
moreover
{
assume "z=v"
with bv have "⟨b,z⟩∈r" by auto
with z(2) have "b=z" using assms(1) unfolding IsLinOrder_def antisym_def by auto
then have "False" using z(3) by auto
}
ultimately have "z∈LeftRayX(X,r,v)" unfolding LeftRayX_def using z(3) by auto
with rayb have "z∈U∩LeftRayX(X,r,v)" using V(2) b(1) by auto
then have "?min∈r``{z}" using Order_ZF_4_L4(1)[OF _ Hmin] assms(1) unfolding Supremum_def IsLinOrder_def
by auto
then have "⟨z,?min⟩∈r" by auto
with z(1,3) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
}
moreover
{
assume "V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}"
then obtain b c where b:"V=IntervalX(X,r,b,c)" "b∈X""c∈X" by auto
from b V(1) have m:"⟨?min,c⟩∈r""⟨b,?min⟩∈r""?min≠b" "?min≠c" unfolding IntervalX_def Interval_def by auto
{
assume A:"⟨c,v⟩∈r"
from m obtain z where z:"⟨z,c⟩∈r" "⟨?min,z⟩∈r""z∈X-{c,?min}" using assms(4) unfolding IsDense_def
using b(3) V(1,2) ‹U⊆X› by blast
from z(2) have "⟨b,z⟩∈r" using m(2) assms(1) unfolding IsLinOrder_def trans_def
by fast
with z(1) have "z∈IntervalX(X,r,b,c)∨z=b" using z(3) unfolding IntervalX_def
Interval_def by auto
then have "z∈IntervalX(X,r,b,c)" using m(2) z(2,3) using assms(1) unfolding IsLinOrder_def
antisym_def by auto
with b(1) V(2) have "z∈U" by auto moreover
from A z(1) have "⟨z,v⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
moreover have "z≠v" using A z(1,3) assms(1) unfolding IsLinOrder_def antisym_def by auto
ultimately have "z∈U∩LeftRayX(X,r,v)" unfolding LeftRayX_def using z(3) by auto
then have "?min∈r``{z}" using Order_ZF_4_L4(1)[OF _ Hmin] assms(1) unfolding Supremum_def IsLinOrder_def
by auto
then have "⟨z,?min⟩∈r" by auto
with z(2,3) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
}
then have vc:"⟨v,c⟩∈r""v≠c" using assms(1) unfolding IsLinOrder_def IsTotal_def using ‹v∈X-U›
b(3) by auto
{
assume "?min=v"
with V(2,1) ‹v∈X-U› have "False" by auto
}
then have "?min≠v" by auto
with a1 obtain z where z:"⟨?min,z⟩∈r""⟨z,v⟩∈r""z∈X-{?min,v}" using assms(4) unfolding IsDense_def
using V(1,2) ‹U⊆X›‹v∈X-U› by blast
from z(2) vc(1) have zc:"⟨z,c⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def
by fast moreover
from m(2) z(1) have "⟨b,z⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def
by fast ultimately
have "z∈Interval(r,b,c)" using Order_ZF_2_L1B by auto moreover
{
assume "z=c"
then have "False" using z(2) vc using assms(1) unfolding IsLinOrder_def antisym_def
by fast
}
then have "z≠c" by auto moreover
{
assume "z=b"
then have "z=?min" using m(2) z(1) using assms(1) unfolding IsLinOrder_def
antisym_def by auto
with z(3) have "False" by auto
}
then have "z≠b" by auto moreover
have "z∈X" using z(3) by auto ultimately
have "z∈IntervalX(X,r,b,c)" unfolding IntervalX_def by auto
then have "z∈V" using b(1) by auto
then have "z∈U" using V(2) by auto moreover
from z(2,3) have "z∈LeftRayX(X,r,v)" unfolding LeftRayX_def by auto ultimately
have "z∈U∩LeftRayX(X,r,v)" by auto
then have "?min∈r``{z}" using Order_ZF_4_L4(1)[OF _ Hmin] assms(1) unfolding Supremum_def IsLinOrder_def
by auto
then have "⟨z,?min⟩∈r" by auto
with z(1,3) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
}
ultimately have "False" using V(3) by auto
}
then have ass:"?min∈X-U" using a1 assms(3) by auto
then obtain V where V:"?min∈V""V⊆X-U"
"V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X}" using point_open_base_neigh
[OF Ordtopology_is_a_topology(2)[OF assms(1)] ‹X-U∈(OrdTopology X r)› ass] by blast
{
assume "V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}"
then obtain b c where b:"V=IntervalX(X,r,b,c)""b∈X""c∈X" by auto
from b V(1) have m:"⟨?min,c⟩∈r""⟨b,?min⟩∈r""?min≠b" "?min≠c" unfolding IntervalX_def Interval_def by auto
{
fix x assume A:"x∈U∩LeftRayX(X,r,v)"
then have "⟨x,v⟩∈r""x∈U" unfolding LeftRayX_def by auto
then have "x∉V" using V(2) by auto
then have "x∉Interval(r, b, c) ∩ X∨x=b∨x=c" using b(1) unfolding IntervalX_def by auto
then have "(⟨b,x⟩∉r∨⟨x,c⟩∉r)∨x=b∨x=c""x∈X" using Order_ZF_2_L1B ‹x∈U›‹U⊆X› by auto
then have "(⟨x,b⟩∈r∨⟨c,x⟩∈r)∨x=b∨x=c" using assms(1) unfolding IsLinOrder_def IsTotal_def
using b(2,3) by auto
then have "(⟨x,b⟩∈r∨⟨c,x⟩∈r)" using assms(1) unfolding IsLinOrder_def using total_is_refl
unfolding refl_def using b(2,3) by auto moreover
from A have "⟨x,?min⟩∈r" using Order_ZF_4_L4(1)[OF _ Hmin] assms(1) unfolding Supremum_def IsLinOrder_def
by auto
ultimately have "(⟨x,b⟩∈r∨⟨c,?min⟩∈r)" using assms(1) unfolding IsLinOrder_def trans_def
by fast
with m(1) have "(⟨x,b⟩∈r∨c=?min)" using assms(1) unfolding IsLinOrder_def antisym_def by auto
with m(4) have "⟨x,b⟩∈r" by auto
}
then have "⟨?min,b⟩∈r" using Order_ZF_5_L3[OF _ nE Hmin] assms(1) unfolding IsLinOrder_def by auto
with m(2,3) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
}
moreover
{
assume "V∈{RightRayX(X,r,b). b∈X}"
then obtain b where b:"V=RightRayX(X,r,b)" "b∈X" by auto
from b V(1) have m:"⟨b,?min⟩∈r""?min≠b" unfolding RightRayX_def by auto
{
fix x assume A:"x∈U∩LeftRayX(X,r,v)"
then have "⟨x,v⟩∈r""x∈U" unfolding LeftRayX_def by auto
then have "x∉V" using V(2) by auto
then have "x∉RightRayX(X,r, b)" using b(1) by auto
then have "(⟨b,x⟩∉r∨x=b)""x∈X" unfolding RightRayX_def using ‹x∈U›‹U⊆X› by auto
then have "⟨x,b⟩∈r" using assms(1) unfolding IsLinOrder_def using total_is_refl unfolding
refl_def unfolding IsTotal_def using b(2) by auto
}
then have "⟨?min,b⟩∈r" using Order_ZF_5_L3[OF _ nE Hmin] assms(1) unfolding IsLinOrder_def by auto
with m(2,1) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
} moreover
{
assume "V∈{LeftRayX(X,r,b). b∈X}"
then obtain b where b:"V=LeftRayX(X,r,b)" "b∈X" by auto
from b V(1) have m:"⟨?min,b⟩∈r""?min≠b" unfolding LeftRayX_def by auto
{
fix x assume A:"x∈U∩LeftRayX(X,r,v)"
then have "⟨x,v⟩∈r""x∈U" unfolding LeftRayX_def by auto
then have "x∉V" using V(2) by auto
then have "x∉LeftRayX(X,r, b)" using b(1) by auto
then have "(⟨x,b⟩∉r∨x=b)""x∈X" unfolding LeftRayX_def using ‹x∈U›‹U⊆X› by auto
then have "⟨b,x⟩∈r" using assms(1) unfolding IsLinOrder_def using total_is_refl unfolding
refl_def unfolding IsTotal_def using b(2) by auto
with m(1) have "⟨?min,x⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
moreover
from bound A have "∃g. ∀y∈U∩LeftRayX(X,r,v). ⟨y,g⟩∈r" using nE
unfolding IsBoundedAbove_def by auto
then obtain g where g:"∀y∈U∩LeftRayX(X,r,v). ⟨y,g⟩∈r" by auto
with nE obtain t where "t∈U∩LeftRayX(X,r,v)" by auto
with g have "⟨t,g⟩∈r" by auto
with assms(3) have "g∈X" by auto
with g have boundX:"∃g∈X. ∀y∈U∩LeftRayX(X,r,v). ⟨y,g⟩∈r" by auto
have "⟨x,?min⟩∈r" using Order_ZF_5_L7(2)[OF assms(3) _ assms(5) _ boundX]
assms(1) ‹U⊆X› A unfolding LeftRayX_def IsLinOrder_def by auto
ultimately have "x=?min" using assms(1) unfolding IsLinOrder_def antisym_def by auto
}
then have "U∩LeftRayX(X,r,v)⊆{?min}" by auto moreover
{
assume "?min∈U∩LeftRayX(X,r,v)"
then have "?min∈U" by auto
then have "False" using V(1,2) by auto
}
ultimately have "False" using nE by auto
}
moreover note V(3)
ultimately have "False" by auto
}
with assms(1) have "⟨v,u⟩∈r" unfolding IsLinOrder_def IsTotal_def using ‹u∈U›‹U⊆X›
‹v∈X-U› by auto
have "RightRayX(X,r,v)∈(OrdTopology X r)" using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]]
‹v∈X-U› by auto
then have "U∩RightRayX(X,r,v)∈(OrdTopology X r)" using U(3) using Ordtopology_is_a_topology(1)
[OF assms(1)] unfolding IsATopology_def by auto
{
fix b assume "b∈(U)∩RightRayX(X,r,v)"
then have "⟨v,b⟩∈r" unfolding RightRayX_def by auto
}
then have bound:"IsBoundedBelow(U∩RightRayX(X,r,v),r)" unfolding IsBoundedBelow_def by auto
with ‹⟨v,u⟩∈r›‹u∈U›‹U⊆X›‹v∈X-U› have nE:"U∩RightRayX(X,r,v)≠0" unfolding RightRayX_def by auto
have Hmax:"HasAmaximum(r,⋂c∈U∩RightRayX(X,r,v). r-``{c})" using complete_order_bounded_below[OF assms(5) bound nE assms(3)].
let ?max="Infimum(r,U∩RightRayX(X,r,v))"
{
fix c assume "c∈U∩RightRayX(X,r,v)"
then have "⟨v,c⟩∈r" unfolding RightRayX_def by auto
}
then have a1:"⟨v,?max⟩∈r" using Order_ZF_5_L4[OF _ nE Hmax] assms(1) unfolding IsLinOrder_def
by auto
{
assume ass:"?max∈U"
then obtain V where V:"?max∈V""V⊆U"
"V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X}" using point_open_base_neigh
[OF Ordtopology_is_a_topology(2)[OF assms(1)] ‹U∈(OrdTopology X r)› ass] by blast
{
assume "V∈{RightRayX(X,r,b). b∈X}"
then obtain b where b:"b∈X" "V=RightRayX(X,r,b)" by auto
from V(1) b(2) have a2:"⟨b,?max⟩∈r""?max≠b" unfolding RightRayX_def by auto
{
assume "⟨b,v⟩∈r"
then have "b=v∨v∈RightRayX(X,r,b)" unfolding RightRayX_def using ‹v∈X-U› by auto
then have "b=v" using b(2) V(2) ‹v∈X-U› by auto
}
then have bv:"⟨v,b⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def using b(1)
‹v∈X-U› by auto
from a2 assms(4) obtain z where z:"⟨b,z⟩∈r""⟨z,?max⟩∈r""z∈X-{b,?max}" unfolding IsDense_def
using b(1) V(1,2) ‹U⊆X› by blast
then have rayb:"z∈RightRayX(X,r,b)" unfolding RightRayX_def by auto
from z(1) bv have "⟨v,z⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast moreover
{
assume "z=v"
with bv have "⟨z,b⟩∈r" by auto
with z(1) have "b=z" using assms(1) unfolding IsLinOrder_def antisym_def by auto
then have "False" using z(3) by auto
}
ultimately have "z∈RightRayX(X,r,v)" unfolding RightRayX_def using z(3) by auto
with rayb have "z∈U∩RightRayX(X,r,v)" using V(2) b(2) by auto
then have "?max∈r-``{z}" using Order_ZF_4_L3(1)[OF _ Hmax] assms(1) unfolding Infimum_def IsLinOrder_def
by auto
then have "⟨?max,z⟩∈r" by auto
with z(2,3) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
}
moreover
{
assume "V∈{LeftRayX(X,r,b). b∈X}"
then obtain b where b:"V=LeftRayX(X,r,b)" "b∈X" by auto
note a1 moreover
from V(1) b(1) have a2:"⟨?max,b⟩∈r""?max≠b" unfolding LeftRayX_def by auto
ultimately have "⟨v,b⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by blast moreover
{
assume "b=v"
with a1 a2(1) have "b=?max" using assms(1) unfolding IsLinOrder_def antisym_def by auto
with a2(2) have "False" by auto
}
ultimately have "False" using V(2) b(1) unfolding LeftRayX_def using ‹v∈X-U› by auto
}
moreover
{
assume "V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}"
then obtain b c where b:"V=IntervalX(X,r,b,c)" "b∈X""c∈X" by auto
from b V(1) have m:"⟨?max,c⟩∈r""⟨b,?max⟩∈r""?max≠b" "?max≠c" unfolding IntervalX_def Interval_def by auto
{
assume A:"⟨v,b⟩∈r"
from m obtain z where z:"⟨z,?max⟩∈r" "⟨b,z⟩∈r""z∈X-{b,?max}" using assms(4) unfolding IsDense_def
using b(2) V(1,2) ‹U⊆X› by blast
from z(1) have "⟨z,c⟩∈r" using m(1) assms(1) unfolding IsLinOrder_def trans_def
by fast
with z(2) have "z∈IntervalX(X,r,b,c)∨z=c" using z(3) unfolding IntervalX_def
Interval_def by auto
then have "z∈IntervalX(X,r,b,c)" using m(1) z(1,3) using assms(1) unfolding IsLinOrder_def
antisym_def by auto
with b(1) V(2) have "z∈U" by auto moreover
from A z(2) have "⟨v,z⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
moreover have "z≠v" using A z(2,3) assms(1) unfolding IsLinOrder_def antisym_def by auto
ultimately have "z∈U∩RightRayX(X,r,v)" unfolding RightRayX_def using z(3) by auto
then have "?max∈r-``{z}" using Order_ZF_4_L3(1)[OF _ Hmax] assms(1) unfolding Infimum_def IsLinOrder_def
by auto
then have "⟨?max,z⟩∈r" by auto
with z(1,3) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
}
then have vc:"⟨b,v⟩∈r""v≠b" using assms(1) unfolding IsLinOrder_def IsTotal_def using ‹v∈X-U›
b(2) by auto
{
assume "?max=v"
with V(2,1) ‹v∈X-U› have "False" by auto
}
then have "v≠?max" by auto moreover
note a1 moreover
have "?max∈X" using V(1,2) ‹U⊆X› by auto
moreover have "v∈X" using ‹v∈X-U› by auto
ultimately obtain z where z:"⟨v,z⟩∈r""⟨z,?max⟩∈r""z∈X-{v,?max}" using assms(4) unfolding IsDense_def
by auto
from z(1) vc(1) have zc:"⟨b,z⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def
by fast moreover
from m(1) z(2) have "⟨z,c⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def
by fast ultimately
have "z∈Interval(r,b,c)" using Order_ZF_2_L1B by auto moreover
{
assume "z=b"
then have "False" using z(1) vc using assms(1) unfolding IsLinOrder_def antisym_def
by fast
}
then have "z≠b" by auto moreover
{
assume "z=c"
then have "z=?max" using m(1) z(2) using assms(1) unfolding IsLinOrder_def
antisym_def by auto
with z(3) have "False" by auto
}
then have "z≠c" by auto moreover
have "z∈X" using z(3) by auto ultimately
have "z∈IntervalX(X,r,b,c)" unfolding IntervalX_def by auto
then have "z∈V" using b(1) by auto
then have "z∈U" using V(2) by auto moreover
from z(1,3) have "z∈RightRayX(X,r,v)" unfolding RightRayX_def by auto ultimately
have "z∈U∩RightRayX(X,r,v)" by auto
then have "?max∈r-``{z}" using Order_ZF_4_L3(1)[OF _ Hmax] assms(1) unfolding Infimum_def IsLinOrder_def
by auto
then have "⟨?max,z⟩∈r" by auto
with z(2,3) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
}
ultimately have "False" using V(3) by auto
}
then have ass:"?max∈X-U" using a1 assms(3) by auto
then obtain V where V:"?max∈V""V⊆X-U"
"V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X}" using point_open_base_neigh
[OF Ordtopology_is_a_topology(2)[OF assms(1)] ‹X-U∈(OrdTopology X r)› ass] by blast
{
assume "V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}"
then obtain b c where b:"V=IntervalX(X,r,b,c)""b∈X""c∈X" by auto
from b V(1) have m:"⟨?max,c⟩∈r""⟨b,?max⟩∈r""?max≠b" "?max≠c" unfolding IntervalX_def Interval_def by auto
{
fix x assume A:"x∈U∩RightRayX(X,r,v)"
then have "⟨v,x⟩∈r""x∈U" unfolding RightRayX_def by auto
then have "x∉V" using V(2) by auto
then have "x∉Interval(r, b, c) ∩ X∨x=b∨x=c" using b(1) unfolding IntervalX_def by auto
then have "(⟨b,x⟩∉r∨⟨x,c⟩∉r)∨x=b∨x=c""x∈X" using Order_ZF_2_L1B ‹x∈U›‹U⊆X› by auto
then have "(⟨x,b⟩∈r∨⟨c,x⟩∈r)∨x=b∨x=c" using assms(1) unfolding IsLinOrder_def IsTotal_def
using b(2,3) by auto
then have "(⟨x,b⟩∈r∨⟨c,x⟩∈r)" using assms(1) unfolding IsLinOrder_def using total_is_refl
unfolding refl_def using b(2,3) by auto moreover
from A have "⟨?max,x⟩∈r" using Order_ZF_4_L3(1)[OF _ Hmax] assms(1) unfolding Infimum_def IsLinOrder_def
by auto
ultimately have "(⟨?max,b⟩∈r∨⟨c,x⟩∈r)" using assms(1) unfolding IsLinOrder_def trans_def
by fast
with m(2) have "(?max=b∨⟨c,x⟩∈r)" using assms(1) unfolding IsLinOrder_def antisym_def by auto
with m(3) have "⟨c,x⟩∈r" by auto
}
then have "⟨c,?max⟩∈r" using Order_ZF_5_L4[OF _ nE Hmax] assms(1) unfolding IsLinOrder_def by auto
with m(1,4) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
}
moreover
{
assume "V∈{RightRayX(X,r,b). b∈X}"
then obtain b where b:"V=RightRayX(X,r,b)" "b∈X" by auto
from b V(1) have m:"⟨b,?max⟩∈r""?max≠b" unfolding RightRayX_def by auto
{
fix x assume A:"x∈U∩RightRayX(X,r,v)"
then have "⟨v,x⟩∈r""x∈U" unfolding RightRayX_def by auto
then have "x∉V" using V(2) by auto
then have "x∉RightRayX(X,r, b)" using b(1) by auto
then have "(⟨b,x⟩∉r∨x=b)""x∈X" unfolding RightRayX_def using ‹x∈U›‹U⊆X› by auto
then have "⟨x,b⟩∈r" using assms(1) unfolding IsLinOrder_def using total_is_refl unfolding
refl_def unfolding IsTotal_def using b(2) by auto moreover
from A have "⟨?max,x⟩∈r" using Order_ZF_4_L3(1)[OF _ Hmax] assms(1) unfolding Infimum_def IsLinOrder_def
by auto ultimately
have "⟨?max,b⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
with m have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
}
then have "False" using nE by auto
} moreover
{
assume "V∈{LeftRayX(X,r,b). b∈X}"
then obtain b where b:"V=LeftRayX(X,r,b)" "b∈X" by auto
from b V(1) have m:"⟨?max,b⟩∈r""?max≠b" unfolding LeftRayX_def by auto
{
fix x assume A:"x∈U∩RightRayX(X,r,v)"
then have "⟨v,x⟩∈r""x∈U" unfolding RightRayX_def by auto
then have "x∉V" using V(2) by auto
then have "x∉LeftRayX(X,r, b)" using b(1) by auto
then have "(⟨x,b⟩∉r∨x=b)""x∈X" unfolding LeftRayX_def using ‹x∈U›‹U⊆X› by auto
then have "⟨b,x⟩∈r" using assms(1) unfolding IsLinOrder_def using total_is_refl unfolding
refl_def unfolding IsTotal_def using b(2) by auto
then have "b∈r-``{x}" by auto
}
with nE have "b∈(⋂c∈U∩RightRayX(X,r,v). r-``{c})" by auto
then have "⟨b,?max⟩∈r" unfolding Infimum_def using Order_ZF_4_L3(2)[OF _ Hmax] assms(1)
unfolding IsLinOrder_def by auto
with m have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
}
moreover note V(3)
ultimately have "False" by auto
}
then show ?thesis by auto
qed
subsection‹Numerability axioms›
text‹A $\kappa$-separable order topology is in relation with order density.›
text‹If an order topology has a subset $A$ which is topologically
dense, then that subset is weakly order-dense in $X$.›
lemma dense_top_imp_Wdense_ord:
assumes "IsLinOrder(X,r)" "Closure(A,OrdTopology X r)=X" "A⊆X" "∃x y. x ≠ y ∧ x ∈ X ∧ y ∈ X"
shows "A{is weakly dense in}X{with respect to}r"
proof-
{
fix r1 r2 assume "r1∈X""r2∈X""r1≠r2" "⟨r1,r2⟩∈r"
then have "IntervalX(X,r,r1,r2)∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪
{RightRayX(X, r, b) . b ∈ X}" by auto
then have P:"IntervalX(X,r,r1,r2)∈(OrdTopology X r)" using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]]
by auto
have "IntervalX(X,r,r1,r2)⊆X" unfolding IntervalX_def by auto
then have int:"Closure(A,OrdTopology X r)∩IntervalX(X,r,r1,r2)=IntervalX(X,r,r1,r2)" using assms(2) by auto
{
assume "IntervalX(X,r,r1,r2)≠0"
then have "A∩(IntervalX(X,r,r1,r2))≠0" using topology0.cl_inter_neigh[OF topology0_ordtopology[OF assms(1)] _ P , of "A"]
using assms(3) union_ordtopology[OF assms(1,4)] int by auto
}
then have "(∃z∈A-{r1,r2}. ⟨r1,z⟩∈r∧⟨z,r2⟩∈r)∨IntervalX(X,r,r1,r2)=0" unfolding IntervalX_def
Interval_def by auto
}
then show ?thesis unfolding IsWeaklyDenseSub_def by auto
qed
text‹Conversely, a weakly order-dense set is topologically dense if it is also considered
that: if there is a maximum or a minimum elements whose singletons are open, this points
have to be in $A$. In conclusion, weakly order-density is a property closed to topological density.›
text‹Another way to see this: Consider a weakly order-dense set $A$:
\begin{itemize}
\item If $X$ has a maximum and a minimum and $\{min,max\}$ is open: $A$ is topologically dense in $X\setminus\{min,max\}$, where $min$ is the minimum in $X$ and $max$ is the maximum in $X$.
\item If $X$ has a maximum, $\{max\}$ is open and $X$ has no minimum
or $\{min\}$ isn't open: $A$ is topologically dense in $X\setminus\{max\}$, where $max$ is the maximum in $X$.
\item If $X$ has a minimum, $\{min\}$ is open and $X$ has no maximum
or $\{max\}$ isn't open $A$ is topologically dense in $X\setminus\{min\}$, where $min$ is the minimum in $X$.
\item If $X$ has no minimum or maximum, or $\{min,max\}$ has no proper open sets: $A$ is topologically dense in $X$.
\end{itemize}
›
lemma Wdense_ord_imp_dense_top:
assumes "IsLinOrder(X,r)" "A{is weakly dense in}X{with respect to}r" "A⊆X" "∃x y. x ≠ y ∧ x ∈ X ∧ y ∈ X"
"HasAminimum(r,X)⟶{Minimum(r,X)}∈(OrdTopology X r)⟶Minimum(r,X)∈A"
"HasAmaximum(r,X)⟶{Maximum(r,X)}∈(OrdTopology X r)⟶Maximum(r,X)∈A"
shows "Closure(A,OrdTopology X r)=X"
proof-
{
fix x assume "x∈X"
{
fix U assume ass:"x∈U""U∈(OrdTopology X r)"
then have "∃V∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪ {RightRayX(X, r, b) . b ∈ X} . V⊆U∧x∈V"
using point_open_base_neigh[OF Ordtopology_is_a_topology(2)[OF assms(1)]] by auto
then obtain V where V:"V∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪ {RightRayX(X, r, b) . b ∈ X}" "V⊆U" "x∈V"
by blast
note V(1) moreover
{
assume "V∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X}"
then obtain b c where b:"b∈X""c∈X""V=IntervalX(X, r, b, c)" by auto
with V(3) have x:"⟨b,x⟩∈r" "⟨x,c⟩∈r" "x≠b" "x≠c" unfolding IntervalX_def Interval_def by auto
then have "⟨b,c⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
moreover from x(1-3) have "b≠c" using assms(1) unfolding IsLinOrder_def antisym_def by fast
moreover note assms(2) b V(3)
ultimately have "∃z∈A-{b,c}. ⟨b,z⟩∈r∧⟨z,c⟩∈r" unfolding IsWeaklyDenseSub_def by auto
then obtain z where "z∈A""z≠b""z≠c""⟨b,z⟩∈r""⟨z,c⟩∈r" by auto
with assms(3) have "z∈A""z∈IntervalX(X, r, b, c)" unfolding IntervalX_def Interval_def by auto
then have "A∩U≠0" using V(2) b(3) by auto
}
moreover
{
assume "V∈{RightRayX(X, r, b) . b ∈ X}"
then obtain b where b:"b∈X""V=RightRayX(X, r, b)" by auto
with V(3) have x:"⟨b,x⟩∈r" "b≠x" unfolding RightRayX_def by auto moreover
note b(1) moreover
have "U⊆⋃(OrdTopology X r)" using ass(2) by auto
then have "U⊆X" using union_ordtopology[OF assms(1,4)] by auto
then have "x∈X" using ass(1) by auto moreover
note assms(2) ultimately
have disj:"(∃z∈A-{b,x}. ⟨b,z⟩∈r∧⟨z,x⟩∈r)∨ IntervalX(X, r, b, x) = 0" unfolding IsWeaklyDenseSub_def by auto
{
assume B:"IntervalX(X, r, b, x) = 0"
{
assume "∃y∈X. ⟨x,y⟩∈r ∧ x≠y"
then obtain y where y:"y∈X""⟨x,y⟩∈r" "x≠y" by auto
with x have "x∈IntervalX(X,r,b,y)" unfolding IntervalX_def Interval_def
using ‹x∈X› by auto moreover
have "⟨b,y⟩∈r" using y(2) x(1) assms(1) unfolding IsLinOrder_def trans_def by fast
moreover have "b≠y" using y(2,3) x(1) assms(1) unfolding IsLinOrder_def antisym_def by fast
ultimately
have "(∃z∈A-{b,y}. ⟨b,z⟩∈r∧⟨z,y⟩∈r)" using assms(2) unfolding IsWeaklyDenseSub_def
using y(1) b(1) by auto
then obtain z where "z∈A""⟨b,z⟩∈r""b≠z" by auto
then have "z∈A∩V" using b(2) unfolding RightRayX_def using assms(3) by auto
then have "z∈A∩U" using V(2) by auto
then have "A∩U≠0" by auto
}
moreover
{
assume R:"∀y∈X. ⟨x,y⟩∈r⟶x=y"
{
fix y assume "y∈RightRayX(X,r,b)"
then have y:"⟨b,y⟩∈r" "y∈X-{b}" unfolding RightRayX_def by auto
{
assume A:"y≠x"
then have "⟨x,y⟩∉r" using R y(2) by auto
then have "⟨y,x⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def
using ‹x∈X› y(2) by auto
with A y have "y∈IntervalX(X,r,b,x)" unfolding IntervalX_def Interval_def
by auto
then have "False" using B by auto
}
then have "y=x" by auto
}
then have "RightRayX(X,r,b)={x}" using V(3) b(2) by blast
moreover
{
fix t assume T:"t∈X"
{
assume "t=x"
then have "⟨t,x⟩∈r" using assms(1) unfolding IsLinOrder_def
using Order_ZF_1_L1 T by auto
}
moreover
{
assume "t≠x"
then have "⟨x,t⟩∉r" using R T by auto
then have "⟨t,x⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def
using T ‹x∈X› by auto
}
ultimately have "⟨t,x⟩∈r" by auto
}
with ‹x∈X› have HM:"HasAmaximum(r,X)" unfolding HasAmaximum_def by auto
then have "Maximum(r,X)∈X""∀t∈X. ⟨t,Maximum(r,X)⟩∈r" using Order_ZF_4_L3 assms(1) unfolding IsLinOrder_def
by auto
with R ‹x∈X› have xm:"x=Maximum(r,X)" by auto
moreover note b(2)
ultimately have "V={Maximum(r,X)}" by auto
then have "{Maximum(r,X)}∈(OrdTopology X r)" using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]]
V(1) by auto
with HM have "Maximum(r,X)∈A" using assms(6) by auto
with xm have "x∈A" by auto
with V(2,3) have "A∩U≠0" by auto
}
ultimately have "A∩U≠0" by auto
}
moreover
{
assume "IntervalX(X, r, b, x) ≠ 0"
with disj have "∃z∈A-{b,x}. ⟨b,z⟩∈r∧⟨z,x⟩∈r" by auto
then obtain z where "z∈A""z≠b""⟨b,z⟩∈r" by auto
then have "z∈A""z∈RightRayX(X,r,b)" unfolding RightRayX_def using assms(3) by auto
then have "z∈A∩U" using V(2) b(2) by auto
then have "A∩U≠0" by auto
}
ultimately have "A∩U≠0" by auto
}
moreover
{
assume "V∈{LeftRayX(X, r, b) . b ∈ X}"
then obtain b where b:"b∈X""V=LeftRayX(X, r, b)" by auto
with V(3) have x:"⟨x,b⟩∈r" "b≠x" unfolding LeftRayX_def by auto moreover
note b(1) moreover
have "U⊆⋃(OrdTopology X r)" using ass(2) by auto
then have "U⊆X" using union_ordtopology[OF assms(1,4)] by auto
then have "x∈X" using ass(1) by auto moreover
note assms(2) ultimately
have disj:"(∃z∈A-{b,x}. ⟨x,z⟩∈r∧⟨z,b⟩∈r)∨ IntervalX(X, r, x, b) = 0" unfolding IsWeaklyDenseSub_def by auto
{
assume B:"IntervalX(X, r, x, b) = 0"
{
assume "∃y∈X. ⟨y,x⟩∈r ∧ x≠y"
then obtain y where y:"y∈X""⟨y,x⟩∈r" "x≠y" by auto
with x have "x∈IntervalX(X,r,y,b)" unfolding IntervalX_def Interval_def
using ‹x∈X› by auto moreover
have "⟨y,b⟩∈r" using y(2) x(1) assms(1) unfolding IsLinOrder_def trans_def by fast
moreover have "b≠y" using y(2,3) x(1) assms(1) unfolding IsLinOrder_def antisym_def by fast
ultimately
have "(∃z∈A-{b,y}. ⟨y,z⟩∈r∧⟨z,b⟩∈r)" using assms(2) unfolding IsWeaklyDenseSub_def
using y(1) b(1) by auto
then obtain z where "z∈A""⟨z,b⟩∈r""b≠z" by auto
then have "z∈A∩V" using b(2) unfolding LeftRayX_def using assms(3) by auto
then have "z∈A∩U" using V(2) by auto
then have "A∩U≠0" by auto
}
moreover
{
assume R:"∀y∈X. ⟨y,x⟩∈r⟶x=y"
{
fix y assume "y∈LeftRayX(X,r,b)"
then have y:"⟨y,b⟩∈r" "y∈X-{b}" unfolding LeftRayX_def by auto
{
assume A:"y≠x"
then have "⟨y,x⟩∉r" using R y(2) by auto
then have "⟨x,y⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def
using ‹x∈X› y(2) by auto
with A y have "y∈IntervalX(X,r,x,b)" unfolding IntervalX_def Interval_def
by auto
then have "False" using B by auto
}
then have "y=x" by auto
}
then have "LeftRayX(X,r,b)={x}" using V(3) b(2) by blast
moreover
{
fix t assume T:"t∈X"
{
assume "t=x"
then have "⟨x,t⟩∈r" using assms(1) unfolding IsLinOrder_def
using Order_ZF_1_L1 T by auto
}
moreover
{
assume "t≠x"
then have "⟨t,x⟩∉r" using R T by auto
then have "⟨x,t⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def
using T ‹x∈X› by auto
}
ultimately have "⟨x,t⟩∈r" by auto
}
with ‹x∈X› have HM:"HasAminimum(r,X)" unfolding HasAminimum_def by auto
then have "Minimum(r,X)∈X""∀t∈X. ⟨Minimum(r,X),t⟩∈r" using Order_ZF_4_L4 assms(1) unfolding IsLinOrder_def
by auto
with R ‹x∈X› have xm:"x=Minimum(r,X)" by auto
moreover note b(2)
ultimately have "V={Minimum(r,X)}" by auto
then have "{Minimum(r,X)}∈(OrdTopology X r)" using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]]
V(1) by auto
with HM have "Minimum(r,X)∈A" using assms(5) by auto
with xm have "x∈A" by auto
with V(2,3) have "A∩U≠0" by auto
}
ultimately have "A∩U≠0" by auto
}
moreover
{
assume "IntervalX(X, r, x, b) ≠ 0"
with disj have "∃z∈A-{b,x}. ⟨x,z⟩∈r∧⟨z,b⟩∈r" by auto
then obtain z where "z∈A""z≠b""⟨z,b⟩∈r" by auto
then have "z∈A""z∈LeftRayX(X,r,b)" unfolding LeftRayX_def using assms(3) by auto
then have "z∈A∩U" using V(2) b(2) by auto
then have "A∩U≠0" by auto
}
ultimately have "A∩U≠0" by auto
}
ultimately have "A∩U≠0" by auto
}
then have "∀U∈(OrdTopology X r). x∈U ⟶ U∩A≠0" by auto
moreover note ‹x∈X› moreover
note assms(3) topology0.inter_neigh_cl[OF topology0_ordtopology[OF assms(1)]]
union_ordtopology[OF assms(1,4)] ultimately have "x∈Closure(A,OrdTopology X r)"
by auto
}
then have "X⊆Closure(A,OrdTopology X r)" by auto
with topology0.Top_3_L11(1)[OF topology0_ordtopology[OF assms(1)]]
assms(3) union_ordtopology[OF assms(1,4)] show ?thesis by auto
qed
text‹The conclusion is that an order topology is $\kappa$-separable
iff there is a set $A$ with cardinality strictly less than $\kappa$
which is weakly-dense in $X$.›
theorem separable_imp_wdense:
assumes "(OrdTopology X r){is separable of cardinal}Q" "∃x y. x ≠ y ∧ x ∈ X ∧ y ∈ X"
"IsLinOrder(X,r)"
shows "∃A∈Pow(X). A≺Q ∧ (A{is weakly dense in}X{with respect to}r)"
proof-
from assms obtain U where "U∈Pow(⋃(OrdTopology X r))" "Closure(U,OrdTopology X r)=⋃(OrdTopology X r)" "U≺Q"
unfolding IsSeparableOfCard_def by auto
then have "U∈Pow(X)" "Closure(U,OrdTopology X r)=X" "U≺Q" using union_ordtopology[OF assms(3,2)]
by auto
with dense_top_imp_Wdense_ord[OF assms(3) _ _ assms(2)] show ?thesis by auto
qed
theorem wdense_imp_separable:
assumes "∃x y. x ≠ y ∧ x ∈ X ∧ y ∈ X" "(A{is weakly dense in}X{with respect to}r)"
"IsLinOrder(X,r)" "A≺Q" "InfCard(Q)" "A⊆X"
shows "(OrdTopology X r){is separable of cardinal}Q"
proof-
{
assume Hmin:"HasAmaximum(r,X)"
then have MaxX:"Maximum(r,X)∈X" using Order_ZF_4_L3(1) assms(3) unfolding IsLinOrder_def
by auto
{
assume HMax:"HasAminimum(r,X)"
then have MinX:"Minimum(r,X)∈X" using Order_ZF_4_L4(1) assms(3) unfolding IsLinOrder_def
by auto
let ?A="A ∪{Maximum(r,X),Minimum(r,X)}"
have "Finite({Maximum(r,X),Minimum(r,X)})" by auto
then have "{Maximum(r,X),Minimum(r,X)}≺nat" using n_lesspoll_nat
unfolding Finite_def using eq_lesspoll_trans by auto
moreover
from assms(5) have "nat≺Q∨nat=Q" unfolding InfCard_def
using lt_Card_imp_lesspoll[of "Q""nat"] unfolding lt_def succ_def
using Card_is_Ord[of "Q"] by auto
ultimately have "{Maximum(r,X),Minimum(r,X)}≺Q" using lesspoll_trans by auto
with assms(4,5) have C:"?A≺Q" using less_less_imp_un_less
by auto
have WeakDense:"?A{is weakly dense in}X{with respect to}r" using assms(2) unfolding
IsWeaklyDenseSub_def by auto
from MaxX MinX assms(6) have S:"?A⊆X" by auto
then have "Closure(?A,OrdTopology X r)=X" using Wdense_ord_imp_dense_top
[OF assms(3) WeakDense _ assms(1)] by auto
then have ?thesis unfolding IsSeparableOfCard_def using union_ordtopology[OF assms(3,1)]
S C by auto
}
moreover
{
assume nmin:"¬HasAminimum(r,X)"
let ?A="A ∪{Maximum(r,X)}"
have "Finite({Maximum(r,X)})" by auto
then have "{Maximum(r,X)}≺nat" using n_lesspoll_nat
unfolding Finite_def using eq_lesspoll_trans by auto
moreover
from assms(5) have "nat≺Q∨nat=Q" unfolding InfCard_def
using lt_Card_imp_lesspoll[of "Q""nat"] unfolding lt_def succ_def
using Card_is_Ord[of "Q"] by auto
ultimately have "{Maximum(r,X)}≺Q" using lesspoll_trans by auto
with assms(4,5) have C:"?A≺Q" using less_less_imp_un_less
by auto
have WeakDense:"?A{is weakly dense in}X{with respect to}r" using assms(2) unfolding
IsWeaklyDenseSub_def by auto
from MaxX assms(6) have S:"?A⊆X" by auto
then have "Closure(?A,OrdTopology X r)=X" using Wdense_ord_imp_dense_top
[OF assms(3) WeakDense _ assms(1)] nmin by auto
then have ?thesis unfolding IsSeparableOfCard_def using union_ordtopology[OF assms(3,1)]
S C by auto
}
ultimately have ?thesis by auto
}
moreover
{
assume nmax:"¬HasAmaximum(r,X)"
{
assume HMin:"HasAminimum(r,X)"
then have MinX:"Minimum(r,X)∈X" using Order_ZF_4_L4(1) assms(3) unfolding IsLinOrder_def
by auto
let ?A="A ∪{Minimum(r,X)}"
have "Finite({Minimum(r,X)})" by auto
then have "{Minimum(r,X)}≺nat" using n_lesspoll_nat
unfolding Finite_def using eq_lesspoll_trans by auto
moreover
from assms(5) have "nat≺Q∨nat=Q" unfolding InfCard_def
using lt_Card_imp_lesspoll[of "Q""nat"] unfolding lt_def succ_def
using Card_is_Ord[of "Q"] by auto
ultimately have "{Minimum(r,X)}≺Q" using lesspoll_trans by auto
with assms(4,5) have C:"?A≺Q" using less_less_imp_un_less
by auto
have WeakDense:"?A{is weakly dense in}X{with respect to}r" using assms(2) unfolding
IsWeaklyDenseSub_def by auto
from MinX assms(6) have S:"?A⊆X" by auto
then have "Closure(?A,OrdTopology X r)=X" using Wdense_ord_imp_dense_top
[OF assms(3) WeakDense _ assms(1)] nmax by auto
then have ?thesis unfolding IsSeparableOfCard_def using union_ordtopology[OF assms(3,1)]
S C by auto
}
moreover
{
assume nmin:"¬HasAminimum(r,X)"
let ?A="A"
from assms(4,5) have C:"?A≺Q" by auto
have WeakDense:"?A{is weakly dense in}X{with respect to}r" using assms(2) unfolding
IsWeaklyDenseSub_def by auto
from assms(6) have S:"?A⊆X" by auto
then have "Closure(?A,OrdTopology X r)=X" using Wdense_ord_imp_dense_top
[OF assms(3) WeakDense _ assms(1)] nmin nmax by auto
then have ?thesis unfolding IsSeparableOfCard_def using union_ordtopology[OF assms(3,1)]
S C by auto
}
ultimately have ?thesis by auto
}
ultimately show ?thesis by auto
qed
end