(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2013 Daniel de la Concepcion This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section ‹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 op:"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 op(2) union_ordtopology[ OF assms(1,2)] unfolding IsClosed_def LeftRayX_def by auto with op(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) _ nE 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 op:"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)] _ op, 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