Theory Topology_ZF_7

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written for Isabelle/Isar.

    Copyright (C) 2012 Daniel de la Concepcion

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED 
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF 
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; 
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR 
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, 
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)

section ‹Topology 7›

theory Topology_ZF_7 imports Topology_ZF_5
begin

subsection‹Connection Properties›

text‹Another type of topological properties are the connection properties.
These properties establish if the space is formed of several pieces or just one.›

text‹A space is connected iff there is no clopen set other that the empty set
and the total set.›

definition IsConnected ("_{is connected}" 70)
  where "T {is connected} ≡ ∀U. (U∈T ∧ (U {is closed in}T)) ⟶ U=0∨U=⋃T"

lemma indiscrete_connected:
  shows "{0,X} {is connected}"
  unfolding IsConnected_def IsClosed_def by auto

text‹The anti-property of connectedness is called total-diconnectedness.›

definition IsTotDis ("_ {is totally-disconnected}" 70)
  where "IsTotDis ≡ ANTI(IsConnected)"

lemma conn_spectrum:
  shows "(A{is in the spectrum of}IsConnected) ⟷ A≲1"
proof
  assume "A{is in the spectrum of}IsConnected"
  then have "∀T. (T{is a topology}∧⋃T≈A) ⟶ (T{is connected})" using Spec_def by auto
  moreover
  have "Pow(A){is a topology}" using Pow_is_top by auto
  moreover
  have "⋃(Pow(A))=A" by auto
  then have "⋃(Pow(A))≈A" by auto
  ultimately have "Pow(A) {is connected}" by auto
  {
    assume "A≠0"
    then obtain E where "E∈A" by blast
    then have "{E}∈Pow(A)" by auto
    moreover
    have "A-{E}∈Pow(A)" by auto
    ultimately have "{E}∈Pow(A)∧{E}{is closed in}Pow(A)" unfolding IsClosed_def by auto
    with ‹Pow(A) {is connected}› have "{E}=A" unfolding IsConnected_def by auto
    then have "A≈1" using singleton_eqpoll_1 by auto
    then have "A≲1" using eqpoll_imp_lepoll by auto
  }
  moreover
  {
    assume "A=0"
    then have "A≲1" using empty_lepollI[of "1"] by auto
  }
  ultimately show "A≲1" by auto
next
  assume "A≲1"
  {
    fix T
    assume "T{is a topology}""⋃T≈A"
    {
      assume "⋃T=0"
      with ‹T{is a topology}› have "T={0}" using empty_open by auto
      then have "T{is connected}" unfolding IsConnected_def by auto
    }
    moreover
    {
      assume "⋃T≠0"
      moreover
      from ‹A≲1›‹⋃T≈A› have "⋃T≲1" using eq_lepoll_trans by auto
      ultimately
      obtain E where "⋃T={E}" using lepoll_1_is_sing by blast
      moreover
      have "T⊆Pow(⋃T)" by auto
      ultimately have "T⊆Pow({E})" by auto
      then have "T⊆{0,{E}}" by blast
      with ‹T{is a topology}› have "{0}⊆T" "T⊆{0,{E}}" using empty_open by auto
      then have "T{is connected}" unfolding IsConnected_def by auto
    }
    ultimately have "T{is connected}" by auto
  }
  then show "A{is in the spectrum of}IsConnected" unfolding Spec_def by auto
qed

text‹The discrete space is a first example of totally-disconnected space.›

lemma discrete_tot_dis:
  shows "Pow(X) {is totally-disconnected}"
proof-
  {
    fix A assume "A∈Pow(X)" and con:"(Pow(X){restricted to}A){is connected}"
    have res:"(Pow(X){restricted to}A)=Pow(A)" unfolding RestrictedTo_def using ‹A∈Pow(X)›
      by blast
    {
      assume "A=0"
      then have "A≲1" using empty_lepollI[of "1"] by auto
      then have "A{is in the spectrum of}IsConnected" using conn_spectrum by auto
    }
    moreover
    {
      assume "A≠0"
      then obtain E where "E∈A" by blast
      then have "{E}∈Pow(A)" by auto
      moreover
      have "A-{E}∈Pow(A)" by auto
      ultimately have "{E}∈Pow(A)∧{E}{is closed in}Pow(A)" unfolding IsClosed_def by auto
      with con res have "{E}=A" unfolding IsConnected_def by auto
      then have "A≈1" using singleton_eqpoll_1 by auto
      then have "A≲1" using eqpoll_imp_lepoll by auto
      then have "A{is in the spectrum of}IsConnected" using conn_spectrum by auto
    }
    ultimately have "A{is in the spectrum of}IsConnected" by auto
  }
  then show ?thesis unfolding IsTotDis_def antiProperty_def by auto
qed

text‹An space is hyperconnected iff every two non-empty open sets meet.›

definition IsHConnected ("_{is hyperconnected}"90)
  where "T{is hyperconnected} ≡∀U V. U∈T ∧ V∈T ∧ U∩V=0 ⟶ U=0∨V=0"

text‹Every hyperconnected space is connected.›
  
lemma HConn_imp_Conn:
  assumes "T{is hyperconnected}"
  shows "T{is connected}"
proof-
  {
    fix U
    assume "U∈T""U {is closed in}T"
    then have "⋃T-U∈T""U∈T" using IsClosed_def by auto
    moreover
    have "(⋃T-U)∩U=0" by auto
    moreover
    note assms
    ultimately
    have "U=0∨(⋃T-U)=0" using IsHConnected_def by auto
    with ‹U∈T› have "U=0∨U=⋃T" by auto
  }
  then show ?thesis using IsConnected_def by auto
qed

lemma Indiscrete_HConn:
  shows "{0,X}{is hyperconnected}"
  unfolding IsHConnected_def by auto

text‹A first example of an hyperconnected space but not indiscrete, is the cofinite topology on 
the natural numbers.›

lemma Cofinite_nat_HConn:
  assumes "¬(X≺nat)"
  shows "(CoFinite X){is hyperconnected}"
proof-
  {
    fix U V
    assume "U∈(CoFinite X)""V∈(CoFinite X)""U∩V=0"
    then have eq:"(X-U)≺nat∨U=0""(X-V)≺nat∨V=0" unfolding Cofinite_def
      CoCardinal_def by auto
    from ‹U∩V=0› have un:"(X-U)∪(X-V)=X" by auto
    {
      assume AS:"(X-U)≺nat""(X-V)≺nat"
      from un have "X≺nat" using less_less_imp_un_less[OF AS InfCard_nat] by auto
      then have "False" using assms by auto
    }
    with eq(1,2) have "U=0∨V=0" by auto
  }
  then show "(CoFinite X){is hyperconnected}" using IsHConnected_def by auto
qed

lemma HConn_spectrum:
  shows "(A{is in the spectrum of}IsHConnected) ⟷ A≲1"
proof
  assume "A{is in the spectrum of}IsHConnected"
  then have "∀T. (T{is a topology}∧⋃T≈A) ⟶ (T{is hyperconnected})" using Spec_def by auto
  moreover
  have "Pow(A){is a topology}" using Pow_is_top by auto
  moreover
  have "⋃(Pow(A))=A" by auto
  then have "⋃(Pow(A))≈A" by auto
  ultimately
  have HC_Pow:"Pow(A){is hyperconnected}" by auto
  {
    assume "A=0"
    then have "A≲1" using empty_lepollI by auto
  }
  moreover
  {
    assume "A≠0"
    then obtain e where "e∈A" by blast
    then have "{e}∈Pow(A)" by auto
    moreover
    have "A-{e}∈Pow(A)" by auto
    moreover
    have "{e}∩(A-{e})=0" by auto
    moreover
    note HC_Pow
    ultimately have "A-{e}=0" unfolding IsHConnected_def by blast
    with ‹e∈A› have "A={e}" by auto
    then have "A≈1" using singleton_eqpoll_1 by auto
    then have "A≲1" using eqpoll_imp_lepoll by auto
  }
  ultimately show "A≲1" by auto
next
  assume "A≲1"
  {
    fix T
    assume "T{is a topology}""⋃T≈A"
    {
      assume "⋃T=0"
      with ‹T{is a topology}› have "T={0}" using empty_open by auto
      then have "T{is hyperconnected}" unfolding IsHConnected_def by auto
    }
    moreover
    {
      assume "⋃T≠0"
      moreover
      from ‹A≲1›‹⋃T≈A› have "⋃T≲1" using eq_lepoll_trans by auto
      ultimately
      obtain E where "⋃T={E}" using lepoll_1_is_sing by blast
      moreover
      have "T⊆Pow(⋃T)" by auto
      ultimately have "T⊆Pow({E})" by auto
      then have "T⊆{0,{E}}" by blast
      with ‹T{is a topology}› have "{0}⊆T" "T⊆{0,{E}}" using empty_open by auto
      then have "T{is hyperconnected}" unfolding IsHConnected_def by auto
    }
    ultimately have "T{is hyperconnected}" by auto
  }
  then show "A{is in the spectrum of}IsHConnected" unfolding Spec_def by auto
qed

text‹In the following results we will show that anti-hyperconnectedness is a separation
property between $T_1$ and $T_2$. We will show also that both implications are proper.›

text‹First, the closure of a point in every topological space is always hyperconnected.
This is the reason why every anti-hyperconnected space must be $T_1$: every singleton
must be closed.›

lemma (in topology0)cl_point_imp_HConn:
  assumes "x∈⋃T"
  shows "(T{restricted to}Closure({x},T)){is hyperconnected}"
proof-
  from assms have sub:"Closure({x},T)⊆⋃T" using Top_3_L11 by auto
  then have tot:"⋃(T{restricted to}Closure({x},T))=Closure({x},T)" unfolding RestrictedTo_def by auto
  {
    fix A B
    assume AS:"A∈(T{restricted to}Closure({x},T))""B∈(T{restricted to}Closure({x},T))""A∩B=0"
    then have "B⊆⋃((T{restricted to}Closure({x},T)))""A⊆⋃((T{restricted to}Closure({x},T)))"
      by auto
    with tot have "B⊆Closure({x},T)""A⊆Closure({x},T)" by auto
    from AS(1,2) obtain UA UB where UAUB:"UA∈T""UB∈T""A=UA∩Closure({x},T)""B=UB∩Closure({x},T)"
      unfolding RestrictedTo_def by auto
    then have "Closure({x},T)-A=Closure({x},T)-(UA∩Closure({x},T))" "Closure({x},T)-B=Closure({x},T)-(UB∩Closure({x},T))"
      by auto
    then have "Closure({x},T)-A=Closure({x},T)-(UA)" "Closure({x},T)-B=Closure({x},T)-(UB)"
      by auto
    with sub have "Closure({x},T)-A=Closure({x},T)∩(⋃T-UA)" "Closure({x},T)-B=Closure({x},T)∩(⋃T-UB)" by auto
    moreover
    from UAUB have "(⋃T-UA){is closed in}T""(⋃T-UB){is closed in}T" using Top_3_L9 by auto
    moreover
    have "Closure({x},T){is closed in}T" using cl_is_closed assms by auto
    ultimately have "(Closure({x},T)-A){is closed in}T""(Closure({x},T)-B){is closed in}T"
      using Top_3_L5(1) by auto
    moreover
    {
      have "x∈Closure({x},T)" using cl_contains_set assms by auto
      moreover
      from AS(3) have "x∉A∨x∉B" by auto
      ultimately have "x∈(Closure({x},T)-A)∨x∈(Closure({x},T)-B)" by auto
    }
    ultimately have "Closure({x},T)⊆(Closure({x},T)-A) ∨ Closure({x},T)⊆(Closure({x},T)-B)"
      using Top_3_L13 by auto
    then have "A∩Closure({x},T)=0 ∨ B∩Closure({x},T)=0" by auto
    with ‹B⊆Closure({x},T)›‹A⊆Closure({x},T)› have "A=0∨B=0" using cl_contains_set assms by blast
  }
  then show ?thesis unfolding IsHConnected_def by auto
qed

text‹A consequence is that every totally-disconnected space is $T_1$.›

lemma (in topology0) tot_dis_imp_T1:
  assumes "T{is totally-disconnected}"
  shows "T{is T1}"
proof-
  {
    fix x y
    assume "y∈⋃T""x∈⋃T""y≠x"
    then have "(T{restricted to}Closure({x},T)){is hyperconnected}" using cl_point_imp_HConn by auto
    then have "(T{restricted to}Closure({x},T)){is connected}" using HConn_imp_Conn by auto
    moreover
    from ‹x∈⋃T› have "Closure({x},T)⊆⋃T" using Top_3_L11(1) by auto
    moreover
    note assms 
    ultimately have "Closure({x},T){is in the spectrum of}IsConnected" unfolding IsTotDis_def antiProperty_def
      by auto
    then have "Closure({x},T)≲1" using conn_spectrum by auto
    moreover
    from ‹x∈⋃T› have "x∈Closure({x},T)" using cl_contains_set by auto
    ultimately have "Closure({x},T)={x}" using lepoll_1_is_sing[of "Closure({x},T)" "x"] by auto
    then have "{x}{is closed in}T" using Top_3_L8 ‹x∈⋃T› by auto
    then have "⋃T-{x}∈T" unfolding IsClosed_def by auto
    moreover
    from ‹y∈⋃T›‹y≠x› have "y∈⋃T-{x}∧x∉⋃T-{x}" by auto
    ultimately have "∃U∈T. y∈U∧x∉U" by force
  }
  then show ?thesis unfolding isT1_def by auto
qed

text‹In the literature, there exists a class of spaces called sober spaces; where the only non-empty closed
hyperconnected subspaces are the closures of points and closures of different singletons
are different.›

definition IsSober ("_{is sober}"90)
  where "T{is sober} ≡ ∀A∈Pow(⋃T)-{0}. (A{is closed in}T ∧ ((T{restricted to}A){is hyperconnected})) ⟶ (∃x∈⋃T. A=Closure({x},T) ∧ (∀y∈⋃T. A=Closure({y},T) ⟶ y=x) )"

text‹Being sober is weaker than being anti-hyperconnected.›

theorem (in topology0) anti_HConn_imp_sober:
  assumes "T{is anti-}IsHConnected"
  shows "T{is sober}"
proof-
  {
    fix A assume "A∈Pow(⋃T)-{0}""A{is closed in}T""(T{restricted to}A){is hyperconnected}"
    with assms have "A{is in the spectrum of}IsHConnected" unfolding antiProperty_def by auto
    then have "A≲1" using HConn_spectrum by auto
    moreover
    with ‹A∈Pow(⋃T)-{0}› have "A≠0" by auto
    then obtain x where "x∈A" by auto
    ultimately have "A={x}" using lepoll_1_is_sing by auto
    with ‹A{is closed in}T› have "{x}{is closed in}T" by auto
    moreover from ‹x∈A› ‹A∈Pow(⋃T)-{0}› have "{x}∈Pow(⋃T)" by auto
    ultimately
    have "Closure({x},T)={x}" unfolding Closure_def ClosedCovers_def by auto
    with ‹A={x}› have "A=Closure({x},T)" by auto
    moreover
    {
      fix y assume "y∈⋃T""A=Closure({y},T)"
      then have "{y}⊆Closure({y},T)" using cl_contains_set by auto
      with ‹A=Closure({y},T)› have "y∈A" by auto
      with ‹A={x}› have "y=x" by auto
    }
    then have "∀y∈⋃T. A=Closure({y},T) ⟶ y=x" by auto
    moreover note ‹{x}∈Pow(⋃T)› 
    ultimately have "∃x∈⋃T. A=Closure({x},T)∧(∀y∈⋃T. A=Closure({y},T) ⟶ y=x)" by auto
  }
  then show ?thesis using IsSober_def by auto
qed
  
text‹Every sober space is $T_0$.›

lemma (in topology0) sober_imp_T0:
  assumes "T{is sober}"
  shows "T{is T0}"
proof-
  {
    fix x y
    assume AS:"x∈⋃T""y∈⋃T""x≠y""∀U∈T. x∈U ⟷ y∈U"
    from ‹x∈⋃T› have clx:"Closure({x},T) {is closed in}T" using cl_is_closed by auto
    with ‹x∈⋃T› have "(⋃T-Closure({x},T))∈T" using Top_3_L11(1) unfolding IsClosed_def by auto
    moreover
    from ‹x∈⋃T› have "x∈Closure({x},T)" using cl_contains_set by auto
    moreover
    note AS(1,4)
    ultimately have "y∉(⋃T-Closure({x},T))" by auto
    with AS(2) have "y∈Closure({x},T)" by auto
    with clx have ineq1:"Closure({y},T)⊆Closure({x},T)" using Top_3_L13 by auto
    from ‹y∈⋃T› have cly:"Closure({y},T) {is closed in}T" using cl_is_closed by auto
    with ‹y∈⋃T› have "(⋃T-Closure({y},T))∈T" using Top_3_L11(1) unfolding IsClosed_def by auto
    moreover
    from ‹y∈⋃T› have "y∈Closure({y},T)" using cl_contains_set by auto
    moreover
    note AS(2,4)
    ultimately have "x∉(⋃T-Closure({y},T))" by auto
    with AS(1) have "x∈Closure({y},T)" by auto
    with cly have "Closure({x},T)⊆Closure({y},T)" using Top_3_L13 by auto
    with ineq1 have eq:"Closure({x},T)=Closure({y},T)" by auto
    have "Closure({x},T)∈Pow(⋃T)-{0}" using Top_3_L11(1) ‹x∈⋃T› ‹x∈Closure({x},T)› by auto
    moreover note assms clx
    ultimately have "∃t∈⋃T.( Closure({x},T) = Closure({t}, T) ∧ (∀y∈⋃T. Closure({x},T) = Closure({y}, T) ⟶ y = t))" 
      unfolding IsSober_def using cl_point_imp_HConn[OF ‹x∈⋃T›] by auto
    then obtain t where t_def:"t∈⋃T""Closure({x},T) = Closure({t}, T)""∀y∈⋃T. Closure({x},T) = Closure({y}, T) ⟶ y = t"
      by blast
    with eq have "y=t" using ‹y∈⋃T› by auto
    moreover from t_def ‹x∈⋃T› have "x=t" by blast
    ultimately have "y=x" by auto
    with ‹x≠y› have "False" by auto
  }
  then have "∀x y. x∈⋃T∧y∈⋃T∧x≠y ⟶ (∃U∈T. (x∈U∧y∉U)∨(y∈U∧x∉U))" by auto
  then show ?thesis using isT0_def by auto
qed

text‹Every $T_2$ space is anti-hyperconnected.›

theorem (in topology0) T2_imp_anti_HConn:
  assumes "T{is T2}"
  shows "T{is anti-}IsHConnected"
proof-
  {
    fix TT
    assume "TT{is a topology}" "TT{is hyperconnected}""TT{is T2}"
    {
      assume "⋃TT=0"
      then have "⋃TT≲1" using empty_lepollI by auto
      then have "(⋃TT){is in the spectrum of}IsHConnected" using HConn_spectrum by auto
    }
    moreover
    {
      assume "⋃TT≠0"
      then obtain x where "x∈⋃TT" by blast
      {
        fix y
        assume "y∈⋃TT""x≠y"
        with ‹TT{is T2}›‹x∈⋃TT› obtain U V where "U∈TT""V∈TT""x∈U""y∈V""U∩V=0" unfolding isT2_def by blast
        with ‹TT{is hyperconnected}› have "False" using IsHConnected_def by auto
      }
      with ‹x∈⋃TT› have "⋃TT={x}" by auto
      then have "⋃TT≈1" using singleton_eqpoll_1 by auto
      then have "⋃TT≲1" using eqpoll_imp_lepoll by auto
      then have "(⋃TT){is in the spectrum of}IsHConnected" using HConn_spectrum by auto
    }
    ultimately have "(⋃TT){is in the spectrum of}IsHConnected" by blast
  }
  then have "∀T. ((T{is a topology}∧(T{is hyperconnected})∧(T{is T2}))⟶ ((⋃T){is in the spectrum of}IsHConnected))"
    by auto
  moreover
  note here_T2
  ultimately
  have "∀T.  T{is a topology} ⟶ ((T{is T2})⟶(T{is anti-}IsHConnected))" using Q_P_imp_Spec[where P=IsHConnected and Q=isT2]
    by auto
  then show ?thesis using assms topSpaceAssum by auto
qed

text‹Every anti-hyperconnected space is $T_1$.›

theorem anti_HConn_imp_T1:
  assumes "T{is anti-}IsHConnected"
  shows "T{is T1}"
proof-
  {
    fix x y
    assume "x∈⋃T""y∈⋃T""x≠y"
    {
      assume AS:"∀U∈T. x∉U∨y∈U"
      from ‹x∈⋃T›‹y∈⋃T› have "{x,y}∈Pow(⋃T)" by auto
      then have sub:"(T{restricted to}{x,y})⊆Pow({x,y})" using RestrictedTo_def by auto
      {
        fix U V
        assume H:"U∈T{restricted to}{x,y}" "V∈(T{restricted to}{x,y})""U∩V=0"
        with AS have "x∈U⟶y∈U""x∈V⟶y∈V" unfolding RestrictedTo_def by auto
        with H(1,2) sub have "x∈U⟶U={x,y}""x∈V⟶V={x,y}" by auto
        with H sub have "x∈U⟶(U={x,y}∧V=0)""x∈V⟶(V={x,y}∧U=0)" by auto
        then have "(x∈U∨x∈V)⟶(U=0∨V=0)" by auto
        moreover
        from sub H have "(x∉U∧x∉V)⟶ (U=0∨V=0)" by blast
        ultimately have "U=0∨V=0" by auto
      }
      then have "(T{restricted to}{x,y}){is hyperconnected}" unfolding IsHConnected_def by auto
      with assms‹{x,y}∈Pow(⋃T)› have "{x,y}{is in the spectrum of}IsHConnected" unfolding antiProperty_def
        by auto
      then have "{x,y}≲1" using HConn_spectrum by auto
      moreover
      have "x∈{x,y}" by auto
      ultimately have "{x,y}={x}" using lepoll_1_is_sing[of "{x,y}""x"] by auto
      moreover
      have "y∈{x,y}" by auto
      ultimately have "y∈{x}" by auto
      then have "y=x" by auto
      with ‹x≠y› have "False" by auto
    }
    then have "∃U∈T. x∈U∧y∉U" by auto
  }
  then show ?thesis using isT1_def by auto
qed

text‹There is at least one topological space that is $T_1$, but not anti-hyperconnected.
This space is the cofinite topology on the natural numbers.›

lemma Cofinite_not_anti_HConn:
  shows "¬((CoFinite nat){is anti-}IsHConnected)" and "(CoFinite nat){is T1}"
proof-
  {
    assume "(CoFinite nat){is anti-}IsHConnected"
    moreover
    have "⋃(CoFinite nat)=nat" unfolding Cofinite_def using union_cocardinal by auto
    moreover
    have "(CoFinite nat){restricted to}nat=(CoFinite nat)" using subspace_cocardinal unfolding Cofinite_def
      by auto
    moreover
    have "¬(nat≺nat)" by auto
    then have "(CoFinite nat){is hyperconnected}" using Cofinite_nat_HConn[of "nat"] by auto
    ultimately have "nat{is in the spectrum of}IsHConnected" unfolding antiProperty_def by auto
    then have "nat≲1" using HConn_spectrum by auto
    moreover
    have "1∈nat" by auto
    then have "1≺nat" using n_lesspoll_nat by auto
    ultimately have "nat≺nat" using lesspoll_trans1 by auto
    then have "False" by auto
  }
  then show "¬((CoFinite nat){is anti-}IsHConnected)" by auto
next
  show "(CoFinite nat){is T1}" using cocardinal_is_T1 InfCard_nat unfolding Cofinite_def by auto
qed

text‹The join-topology build from the cofinite topology on the natural numbers,
and the excluded set topology on the natural numbers excluding ‹{0,1}›;
is just the union of both.›

lemma join_top_cofinite_excluded_set:
  shows "(joinT {CoFinite nat,ExcludedSet(nat,{0,1})})=(CoFinite nat)∪ ExcludedSet(nat,{0,1})"
proof-
  have coftop:"(CoFinite nat){is a topology}" unfolding Cofinite_def using CoCar_is_topology InfCard_nat by auto
  moreover
  have "ExcludedSet(nat,{0,1}){is a topology}" using excludedset_is_topology by auto
  moreover
  have exuni:"⋃ExcludedSet(nat,{0,1})=nat" using union_excludedset by auto
  moreover
  have cofuni:"⋃(CoFinite nat)=nat" using union_cocardinal unfolding Cofinite_def by auto
  ultimately have "(joinT {CoFinite nat,ExcludedSet(nat,{0,1})}) = (THE T. (CoFinite nat)∪ExcludedSet(nat,{0,1}) {is a subbase for} T)"
    using joinT_def by auto
  moreover
  have "⋃(CoFinite nat)∈CoFinite nat" using CoCar_is_topology[OF InfCard_nat] unfolding Cofinite_def IsATopology_def
    by auto
  with cofuni have n:"nat∈CoFinite nat" by auto
  have Pa:"(CoFinite nat)∪ExcludedSet(nat,{0,1}) {is a subbase for}{⋃A. A∈Pow({⋂B. B∈FinPow((CoFinite nat)∪ExcludedSet(nat,{0,1}))})}"
    using Top_subbase(2) by auto
  have "{⋃A. A∈Pow({⋂B. B∈FinPow((CoFinite nat)∪ExcludedSet(nat,{0,1}))})}=(THE T. (CoFinite nat)∪ExcludedSet(nat,{0,1}) {is a subbase for} T)"
    using same_subbase_same_top[where B="(CoFinite nat)∪ExcludedSet(nat,{0,1})", OF _ Pa] the_equality[where a="{⋃A. A∈Pow({⋂B. B∈FinPow((CoFinite nat)∪ExcludedSet(nat,{0,1}))})}" and P="λT. ((CoFinite nat)∪ExcludedSet(nat,{0,1})){is a subbase for}T",
      OF Pa] by auto
  ultimately have equal:"(joinT {CoFinite nat,ExcludedSet(nat,{0,1})}) ={⋃A. A∈Pow({⋂B. B∈FinPow((CoFinite nat)∪ExcludedSet(nat,{0,1}))})}"
    by auto
  {
    fix U assume "U∈{⋃A. A∈Pow({⋂B. B∈FinPow((CoFinite nat)∪ExcludedSet(nat,{0,1}))})}"
    then obtain AU where "U=⋃AU" and base:"AU∈Pow({⋂B. B∈FinPow((CoFinite nat)∪ExcludedSet(nat,{0,1}))})"
      by auto
    have "(CoFinite nat)⊆Pow(⋃(CoFinite nat))" by auto
    moreover
    have "ExcludedSet(nat,{0,1})⊆Pow(⋃ExcludedSet(nat,{0,1}))" by auto
    moreover
    note cofuni exuni
    ultimately have sub:"(CoFinite nat)∪ExcludedSet(nat,{0,1})⊆Pow(nat)" by auto
    from base have "∀S∈AU. S∈{⋂B. B∈FinPow((CoFinite nat)∪ExcludedSet(nat,{0,1}))}" by blast
    then have "∀S∈AU. ∃B∈FinPow((CoFinite nat)∪ExcludedSet(nat,{0,1})). S=⋂B" by blast
    then have eq:"∀S∈AU. ∃B∈Pow((CoFinite nat)∪ExcludedSet(nat,{0,1})). S=⋂B" unfolding FinPow_def by blast
    { 
      fix S assume "S∈AU"
      with eq obtain B where "B∈Pow((CoFinite nat)∪ExcludedSet(nat,{0,1}))""S=⋂B" by auto
      with sub have "B∈Pow(Pow(nat))" by auto
      {
        fix x assume "x∈⋂B"
        then have "∀N∈B. x∈N""B≠0" by auto
        with ‹B∈Pow(Pow(nat))› have "x∈nat" by blast
      }
      with ‹S=⋂B› have "S∈Pow(nat)" by auto
    }
    then have "∀S∈AU. S∈Pow(nat)" by blast
    with ‹U=⋃AU› have "U∈Pow(nat)" by auto
    {
      assume "0∈U∨1∈U"
      with ‹U=⋃AU› obtain S where "S∈AU""0∈S∨1∈S" by auto
      with base obtain BS where "S=⋂BS" and bsbase:"BS∈FinPow((CoFinite nat)∪ExcludedSet(nat,{0,1}))" by auto
      with ‹0∈S∨1∈S› have "∀M∈BS. 0∈M∨1∈M" by auto
      then have "∀M∈BS. M∉ExcludedSet(nat,{0,1})-{nat}" unfolding ExcludedPoint_def ExcludedSet_def by auto
      moreover
      note bsbase n
      ultimately have "BS∈FinPow(CoFinite nat)" unfolding FinPow_def by auto
      moreover
      from ‹0∈S∨1∈S› have "S≠0" by auto
      with ‹S=⋂BS› have "BS≠0" by auto
      moreover
      note coftop 
      ultimately have "⋂BS∈CoFinite nat" using topology0.fin_inter_open_open[OF topology0_CoCardinal[OF InfCard_nat]]
        unfolding Cofinite_def by auto
      with ‹S=⋂BS› have "S∈CoFinite nat" by auto
      with ‹0∈S∨1∈S› have "nat-S≺nat" unfolding Cofinite_def CoCardinal_def by auto
      moreover
      from ‹U=⋃AU›‹S∈AU› have "S⊆U" by auto
      then have "nat-U⊆nat-S" by auto
      then have "nat-U≲nat-S" using subset_imp_lepoll by auto
      ultimately
      have "nat-U≺nat" using lesspoll_trans1 by auto
      with ‹U∈Pow(nat)› have "U∈CoFinite nat" unfolding Cofinite_def CoCardinal_def by auto
      with ‹U∈Pow(nat)› have "U∈ (CoFinite nat)∪ ExcludedSet(nat,{0,1})" by auto
    }
    with ‹U∈Pow(nat)› have "U∈(CoFinite nat)∪ ExcludedSet(nat,{0,1})" unfolding ExcludedSet_def by blast
  }
  then have "({⋃A . A ∈ Pow({⋂B . B ∈ FinPow((CoFinite nat) ∪ ExcludedSet(nat,{0,1}))})}) ⊆ (CoFinite nat)∪ ExcludedSet(nat,{0,1})"
    by blast
  moreover
  {
    fix U
    assume "U∈(CoFinite nat)∪ ExcludedSet(nat,{0,1})"
    then have "{U}∈FinPow((CoFinite nat) ∪ ExcludedSet(nat,{0,1}))" unfolding FinPow_def by auto
    then have "{U}∈Pow({⋂B . B ∈ FinPow((CoFinite nat) ∪ ExcludedSet(nat,{0,1}))})" by blast
    moreover
    have "U=⋃{U}" by auto
    ultimately have "U∈{⋃A . A ∈ Pow({⋂B . B ∈ FinPow((CoFinite nat) ∪ ExcludedSet(nat,{0,1}))})}" by blast
  }
  then have "(CoFinite nat)∪ ExcludedSet(nat,{0,1})⊆{⋃A . A ∈ Pow({⋂B . B ∈ FinPow((CoFinite nat) ∪ ExcludedSet(nat,{0,1}))})}"
    by auto
  ultimately have "(CoFinite nat)∪ ExcludedSet(nat,{0,1})={⋃A . A ∈ Pow({⋂B . B ∈ FinPow((CoFinite nat) ∪ ExcludedSet(nat,{0,1}))})}"
    by auto
  with equal show ?thesis by auto
qed

text‹The previous topology in not $T_2$, but is anti-hyperconnected.›

theorem join_Cofinite_ExclPoint_not_T2:
  shows 
    "¬((joinT {CoFinite nat, ExcludedSet(nat,{0,1})}){is T2})" and 
    "(joinT {CoFinite nat,ExcludedSet(nat,{0,1})}){is anti-} IsHConnected"
proof-
  have "(CoFinite nat) ⊆ (CoFinite nat) ∪ ExcludedSet(nat,{0,1})" by auto
  have "⋃((CoFinite nat)∪ ExcludedSet(nat,{0,1}))=(⋃(CoFinite nat))∪ (⋃ExcludedSet(nat,{0,1}))"
    by auto
  moreover
  have "…=nat "unfolding Cofinite_def using union_cocardinal union_excludedset by auto
  ultimately have tot:"⋃((CoFinite nat)∪ ExcludedSet(nat,{0,1}))=nat" by auto
  { 
    assume "(joinT {CoFinite nat,ExcludedSet(nat,{0,1})}) {is T2}"
    then have t2:"((CoFinite nat)∪ ExcludedSet(nat,{0,1})){is T2}" using join_top_cofinite_excluded_set
      by auto
    with tot have "∃U∈((CoFinite nat)∪ ExcludedSet(nat,{0,1})). ∃V∈((CoFinite nat)∪ ExcludedSet(nat,{0,1})). 0∈U∧1∈V∧U∩V=0" using isT2_def by auto
    then obtain U V where "U ∈ (CoFinite nat) ∨ (0 ∉ U∧1∉U)""V ∈ (CoFinite nat) ∨ (0 ∉ V∧1∉V)""0∈U""1∈V""U∩V=0" 
      unfolding ExcludedSet_def by auto
    then have "U∈(CoFinite nat)""V∈(CoFinite nat)" by auto
    with ‹0∈U›‹1∈V› have "U∩V≠0" using Cofinite_nat_HConn IsHConnected_def by auto
    with ‹U∩V=0› have "False" by auto
  }
  then show "¬((joinT {CoFinite nat,ExcludedSet(nat,{0,1})}){is T2})" by auto
  {
    fix A assume AS:"A∈Pow(⋃((CoFinite nat)∪ ExcludedSet(nat,{0,1})))""(((CoFinite nat)∪ ExcludedSet(nat,{0,1})){restricted to}A){is hyperconnected}"
    with tot have "A∈Pow(nat)" by auto
    then have sub:"A∩nat=A" by auto
    have "((CoFinite nat)∪ ExcludedSet(nat,{0,1})){restricted to}A=((CoFinite nat){restricted to}A)∪ (ExcludedSet(nat,{0,1}){restricted to}A)"
      unfolding RestrictedTo_def by auto
    also from sub have "…=(CoFinite A)∪ExcludedSet(A,{0,1})" using subspace_excludedset[of"nat""{0,1}""A"] subspace_cocardinal[of "nat""nat""A"] unfolding Cofinite_def
      by auto
    finally have "((CoFinite nat)∪ ExcludedSet(nat,{0,1})){restricted to}A=(CoFinite A)∪ExcludedSet(A,{0,1})" by auto
    with AS(2) have eq:"((CoFinite A)∪ExcludedSet(A,{0,1})){is hyperconnected}" by auto
    {
      assume "{0,1}∩A=0"
      then have "(CoFinite A)∪ExcludedSet(A,{0,1})=Pow(A)" using empty_excludedset[of "{0,1}""A"] unfolding Cofinite_def CoCardinal_def
        by auto
      with eq have "Pow(A){is hyperconnected}" by auto
      then have "Pow(A){is connected}" using HConn_imp_Conn by auto
      moreover
      have "Pow(A){is anti-}IsConnected" using discrete_tot_dis unfolding IsTotDis_def by auto
      moreover
      have "⋃(Pow(A))∈Pow(⋃(Pow(A)))" by auto
      moreover
      have "Pow(A){restricted to}⋃(Pow(A))=Pow(A)" unfolding RestrictedTo_def by blast
      ultimately have "(⋃(Pow(A))){is in the spectrum of}IsConnected" unfolding antiProperty_def
        by auto
      then have "A{is in the spectrum of}IsConnected" by auto
      then have "A≲1" using conn_spectrum  by auto
      then have "A{is in the spectrum of}IsHConnected" using HConn_spectrum by auto
    }
    moreover
    {
      assume AS:"{0,1}∩A≠0"
      {
        assume "A={0}∨A={1}"
        then have "A≈1" using singleton_eqpoll_1 by auto
        then have "A≲1" using eqpoll_imp_lepoll by auto
        then have "A{is in the spectrum of}IsHConnected" using HConn_spectrum by auto
      }
      moreover
      {  
        assume AS2:"¬(A={0}∨A={1})"
        {
          assume AS3:"A⊆{0,1}"
          with AS AS2 have A_def:"A={0,1}" by blast
          then have "ExcludedSet(A,{0,1})=ExcludedSet(A,A)" by auto
          moreover have "ExcludedSet(A,A)={0,A}" unfolding ExcludedSet_def by blast
          ultimately have "ExcludedSet(A,{0,1})={0,A}" by auto
          moreover
          have "0∈(CoFinite A)" using empty_open[of "CoFinite A"]
            CoCar_is_topology[OF InfCard_nat,of "A"] unfolding Cofinite_def by auto
          moreover
          have "⋃(CoFinite A)=A" using union_cocardinal unfolding Cofinite_def by auto
          then have "A∈(CoFinite A)" using CoCar_is_topology[OF InfCard_nat,of "A"] unfolding Cofinite_def
            IsATopology_def by auto
          ultimately have "(CoFinite A)∪ExcludedSet(A,{0,1})=(CoFinite A)" by auto
          with eq have"(CoFinite A){is hyperconnected}" by auto
          with A_def have  hyp:"(CoFinite {0,1}){is hyperconnected}" by auto
          have "{0}≈1""{1}≈1" using singleton_eqpoll_1 by auto
          moreover
          have "1≺nat" using n_lesspoll_nat by auto
          ultimately have "{0}≺nat""{1}≺nat" using eq_lesspoll_trans by auto
          moreover
          have "{0,1}-{1}={0}""{0,1}-{0}={1}" by auto
          ultimately have "{1}∈(CoFinite {0,1})""{0}∈(CoFinite {0,1})" "{1}∩{0}=0" unfolding Cofinite_def CoCardinal_def
            by auto
          with hyp have "False" unfolding IsHConnected_def by auto
        }
        then obtain t where "t∈A" "t≠0" "t≠1" by auto
        then have "{t}∈ExcludedSet(A,{0,1})" unfolding ExcludedSet_def by auto
        moreover
        {
          have "{t}≈1" using singleton_eqpoll_1 by auto
          moreover
          have "1≺nat" using n_lesspoll_nat by auto
          ultimately have "{t}≺nat" using eq_lesspoll_trans by auto
          moreover
          with ‹t∈A› have "A-(A-{t})={t}" by auto
          ultimately have "A-{t}∈(CoFinite A)" unfolding Cofinite_def CoCardinal_def
            by auto
        }
        ultimately have "{t}∈((CoFinite A)∪ExcludedSet(A,{0,1}))""A-{t}∈((CoFinite A)∪ExcludedSet(A,{0,1}))"
          "{t}∩(A-{t})=0" by auto
        with eq have "A-{t}=0" unfolding IsHConnected_def by auto
        with ‹t∈A› have "A={t}" by auto
        then have "A≈1" using singleton_eqpoll_1 by auto
        then have "A≲1" using eqpoll_imp_lepoll by auto
        then have "A{is in the spectrum of}IsHConnected" using HConn_spectrum by auto
      }
      ultimately have "A{is in the spectrum of}IsHConnected" by auto
    }
    ultimately have "A{is in the spectrum of}IsHConnected" by auto
  }
  then have "((CoFinite nat)∪ExcludedSet(nat,{0,1})){is anti-}IsHConnected" unfolding antiProperty_def
    by auto
  then show "(joinT {CoFinite nat, ExcludedSet(nat,{0,1})}){is anti-}IsHConnected" using join_top_cofinite_excluded_set
    by auto
qed

text‹Let's show that anti-hyperconnected is in fact $T_1$ and sober. The trick of the proof lies
in the fact that if a subset is hyperconnected, its closure is so too (the closure of a point
is then always hyperconnected because singletons are in the spectrum); since the closure
is closed, we can apply the sober property on it.›

theorem (in topology0) T1_sober_imp_anti_HConn:
  assumes "T{is T1}" and "T{is sober}"
  shows "T{is anti-}IsHConnected"
proof-
  {
    fix A assume AS:"A∈Pow(⋃T)""(T{restricted to}A){is hyperconnected}"
    {
      assume "A=0"
      then have "A≲1" using empty_lepollI by auto
      then have "A{is in the spectrum of}IsHConnected" using HConn_spectrum by auto
    }
    moreover
    {
      assume "A≠0"
      then obtain x where "x∈A" by blast
      {
        assume "¬((T{restricted to}Closure(A,T)){is hyperconnected})"
        then obtain U V where UV_def:"U∈(T{restricted to}Closure(A,T))""V∈(T{restricted to}Closure(A,T))"
          "U∩V=0""U≠0""V≠0" using IsHConnected_def by auto
        then obtain UCA VCA where "UCA∈T""VCA∈T""U=UCA∩Closure(A,T)""V=VCA∩Closure(A,T)"
          unfolding RestrictedTo_def by auto
        from ‹A∈Pow(⋃T)› have "A⊆Closure(A,T)" using cl_contains_set by auto
        then have "UCA∩A⊆UCA∩Closure(A,T)""VCA∩A⊆VCA∩Closure(A,T)" by auto
        with ‹U=UCA∩Closure(A,T)›‹V=VCA∩Closure(A,T)›‹U∩V=0› have "(UCA∩A)∩(VCA∩A)=0" by auto
        moreover
        from ‹UCA∈T›‹VCA∈T› have "UCA∩A∈(T{restricted to}A)""VCA∩A∈(T{restricted to}A)"
          unfolding RestrictedTo_def by auto
        moreover
        note AS(2)
        ultimately have "UCA∩A=0∨VCA∩A=0" using IsHConnected_def by auto
        with ‹A⊆Closure(A,T)› have "A⊆Closure(A,T)-UCA∨A⊆Closure(A,T)-VCA" by auto
        moreover
        {
          have "Closure(A,T)-UCA=Closure(A,T)∩(⋃T-UCA)""Closure(A,T)-VCA=Closure(A,T)∩(⋃T-VCA)"
            using Top_3_L11(1) AS(1) by auto
          moreover 
          with ‹UCA∈T›‹VCA∈T› have "(⋃T-UCA){is closed in}T""(⋃T-VCA){is closed in}T""Closure(A,T){is closed in}T"
            using Top_3_L9 cl_is_closed AS(1) by auto
          ultimately have "(Closure(A,T)-UCA){is closed in}T""(Closure(A,T)-VCA){is closed in}T"
            using Top_3_L5(1) by auto
        }
        ultimately
        have "Closure(A,T)⊆Closure(A,T)-UCA∨Closure(A,T)⊆Closure(A,T)-VCA" using Top_3_L13
          by auto
        then have "UCA∩Closure(A,T)=0∨VCA∩Closure(A,T)=0" by auto
        with ‹U=UCA∩Closure(A,T)›‹V=VCA∩Closure(A,T)› have "U=0∨V=0" by auto
        with ‹U≠0›‹V≠0› have "False" by auto
      }
      then have "(T{restricted to}Closure(A,T)){is hyperconnected}" by auto
      moreover
      have "Closure(A,T){is closed in}T" using cl_is_closed AS(1) by auto
      moreover
      from ‹x∈A› have "Closure(A,T)≠0" using cl_contains_set AS(1) by auto
      moreover
      from AS(1) have "Closure(A,T)⊆⋃T" using Top_3_L11(1) by auto
      ultimately have "Closure(A,T)∈Pow(⋃T)-{0}""(T {restricted to} Closure(A, T)){is hyperconnected}" "Closure(A, T) {is closed in} T"
        by auto
      moreover note assms(2) 
      ultimately have "∃x∈⋃T. (Closure(A,T)=Closure({x},T)∧ (∀y∈⋃T. Closure(A,T) = Closure({y}, T) ⟶ y = x))" unfolding IsSober_def
        by auto
      then obtain y where "y∈⋃T""Closure(A,T)=Closure({y},T)" by auto
      moreover
      {
        fix z assume "z∈(⋃T)-{y}"
        with assms(1) ‹y∈⋃T› obtain U where "U∈T" "z∈U" "y∉U" using isT1_def by blast
        then have "U∈T" "z∈U" "U⊆(⋃T)-{y}" by auto
        then have "∃U∈T. z∈U ∧ U⊆(⋃T)-{y}" by auto
      }
      then have "∀z∈(⋃T)-{y}. ∃U∈T. z∈U ∧ U⊆(⋃T)-{y}" by auto
      then have "⋃T-{y}∈T" using open_neigh_open by auto
      with ‹y∈⋃T› have "{y} {is closed in}T" using IsClosed_def by auto
      with ‹y∈⋃T› have "Closure({y},T)={y}" using Top_3_L8 by auto
      with ‹Closure(A,T)=Closure({y},T)› have "Closure(A,T)={y}" by auto
      with AS(1) have "A⊆{y}" using cl_contains_set[of "A"] by auto
      with ‹A≠0› have "A={y}" by auto
      then have "A≈1" using singleton_eqpoll_1 by auto
      then have "A≲1" using eqpoll_imp_lepoll by auto
      then have "A{is in the spectrum of}IsHConnected" using HConn_spectrum by auto
    }
    ultimately have "A{is in the spectrum of}IsHConnected" by blast
  }
  then show ?thesis using antiProperty_def by auto
qed

theorem (in topology0) anti_HConn_iff_T1_sober:
  shows "(T{is anti-}IsHConnected) ⟷ (T{is sober}∧T{is T1})"
  using T1_sober_imp_anti_HConn anti_HConn_imp_T1 anti_HConn_imp_sober by auto


text‹A space is ultraconnected iff every two non-empty closed sets meet.›

definition IsUConnected ("_{is ultraconnected}"80)
  where "T{is ultraconnected}≡ ∀A B. A{is closed in}T∧B{is closed in}T∧A∩B=0 ⟶ A=0∨B=0"

text‹Every ultraconnected space is trivially normal.›

lemma (in topology0)UConn_imp_normal:
  assumes "T{is ultraconnected}"
  shows "T{is normal}"
proof-
  {
    fix A B
    assume AS:"A{is closed in}T" "B{is closed in}T""A∩B=0"
    with assms have "A=0∨B=0" using IsUConnected_def by auto
    with AS(1,2) have "(A⊆0∧B⊆⋃T)∨(A⊆⋃T∧B⊆0)" unfolding IsClosed_def by auto
    moreover
    have "0∈T" using empty_open topSpaceAssum by auto
    moreover
    have "⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto
    ultimately have "∃U∈T. ∃V∈T. A⊆U∧B⊆V∧U∩V=0" by auto
  }
  then show ?thesis unfolding IsNormal_def by auto
qed

text‹Every ultraconnected space is connected.›

lemma UConn_imp_Conn:
  assumes "T{is ultraconnected}"
  shows "T{is connected}"
proof-
  {
    fix U V
    assume "U∈T""U{is closed in}T"
    then have "⋃T-(⋃T-U)=U" by auto
    with ‹U∈T› have "(⋃T-U){is closed in}T" unfolding IsClosed_def by auto
    with ‹U{is closed in}T› assms have "U=0∨⋃T-U=0" unfolding IsUConnected_def by auto
    with ‹U∈T› have "U=0∨U=⋃T" by auto
  }
  then show ?thesis unfolding IsConnected_def by auto
qed

lemma UConn_spectrum:
  shows "(A{is in the spectrum of}IsUConnected) ⟷ A≲1"
proof
  assume A_spec:"(A{is in the spectrum of}IsUConnected)"
  {
    assume "A=0"
    then have "A≲1" using empty_lepollI by auto
  }
  moreover
  {
    assume "A≠0"
    from A_spec have "∀T. (T{is a topology}∧⋃T≈A) ⟶ (T{is ultraconnected})" unfolding Spec_def by auto
    moreover
    have "Pow(A){is a topology}" using Pow_is_top by auto
    moreover
    have "⋃Pow(A)=A" by auto
    then have "⋃Pow(A)≈A" by auto
    ultimately have ult:"Pow(A){is ultraconnected}" by auto
    moreover
    from ‹A≠0› obtain b where "b∈A" by auto
    then have "{b}{is closed in}Pow(A)" unfolding IsClosed_def by auto
    {
      fix c
      assume "c∈A""c≠b"
      then have "{c}{is closed in}Pow(A)""{c}∩{b}=0" unfolding IsClosed_def by auto
      with ult ‹{b}{is closed in}Pow(A)› have "False" using IsUConnected_def by auto
    }
    with ‹b∈A› have "A={b}" by auto
    then have "A≈1" using singleton_eqpoll_1 by auto
    then have "A≲1" using eqpoll_imp_lepoll by auto
  }
  ultimately show "A≲1" by auto
next
  assume "A≲1"
  {
    fix T
    assume "T{is a topology}""⋃T≈A"
    {
      assume "⋃T=0"
      with ‹T{is a topology}› have "T={0}" using empty_open by auto
      then have "T{is ultraconnected}" unfolding IsUConnected_def IsClosed_def by auto
    }
    moreover
    {
      assume "⋃T≠0"
      moreover
      from ‹A≲1›‹⋃T≈A› have "⋃T≲1" using eq_lepoll_trans by auto
      ultimately
      obtain E where eq:"⋃T={E}" using lepoll_1_is_sing by blast
      moreover
      have "T⊆Pow(⋃T)" by auto
      ultimately have "T⊆Pow({E})" by auto
      then have "T⊆{0,{E}}" by blast
      with ‹T{is a topology}› have "{0}⊆T" "T⊆{0,{E}}" using empty_open by auto
      then have "T{is ultraconnected}" unfolding IsUConnected_def IsClosed_def by (simp only: eq, safe, force)
    }
    ultimately have "T{is ultraconnected}" by auto
  }
  then show "A{is in the spectrum of}IsUConnected" unfolding Spec_def by auto
qed

text‹This time, anti-ultraconnected is an old property.›

theorem (in topology0) anti_UConn:
  shows "(T{is anti-}IsUConnected) ⟷ T{is T1}"
proof
  assume "T{is T1}"
  {
    fix TT
    {
      assume "TT{is a topology}""TT{is T1}""TT{is ultraconnected}"
      {
        assume "⋃TT=0"
        then have "⋃TT≲1" using empty_lepollI by auto
        then have "((⋃TT){is in the spectrum of}IsUConnected)" using UConn_spectrum by auto
      }
      moreover
      {
        assume "⋃TT≠0"
        then obtain t where "t∈⋃TT" by blast
        {
          fix x
          assume p:"x∈⋃TT"
          {
            fix y assume "y∈(⋃TT)-{x}"
            with ‹TT{is T1}› p obtain U where "U∈TT" "y∈U" "x∉U" using isT1_def by blast
            then have "U∈TT" "y∈U" "U⊆(⋃TT)-{x}" by auto
            then have "∃U∈TT. y∈U ∧ U⊆(⋃TT)-{x}" by auto
          }
          then have "∀y∈(⋃TT)-{x}. ∃U∈TT. y∈U ∧ U⊆(⋃TT)-{x}" by auto
          with ‹TT{is a topology}› have "⋃TT-{x}∈TT" using topology0.open_neigh_open unfolding topology0_def by auto
          with p have "{x} {is closed in}TT" using IsClosed_def by auto
        }
        then have reg:"∀x∈⋃TT. {x}{is closed in}TT" by auto
        with ‹t∈⋃TT› have t_cl:"{t}{is closed in}TT" by auto
        {
          fix y
          assume "y∈⋃TT"
          with reg have "{y}{is closed in}TT" by auto
          with ‹TT{is ultraconnected}› t_cl have "y=t" unfolding IsUConnected_def by auto
        }
        with ‹t∈⋃TT› have "⋃TT={t}" by blast
        then have "⋃TT≈1" using singleton_eqpoll_1 by auto
        then have "⋃TT≲1" using eqpoll_imp_lepoll by auto
        then have "(⋃TT){is in the spectrum of}IsUConnected" using UConn_spectrum by auto
      }
      ultimately have "(⋃TT){is in the spectrum of}IsUConnected" by blast
    }
    then have "(TT{is a topology}∧TT{is T1}∧(TT{is ultraconnected}))⟶ ((⋃TT){is in the spectrum of}IsUConnected)"
      by auto
  }
  then have "∀TT. (TT{is a topology}∧TT{is T1}∧(TT{is ultraconnected}))⟶ ((⋃TT){is in the spectrum of}IsUConnected)"
    by auto
  moreover
  note here_T1
  ultimately have "∀T. T{is a topology} ⟶ ((T{is T1})⟶(T{is anti-}IsUConnected))" using Q_P_imp_Spec[where Q=isT1 and P=IsUConnected]
    by auto
  with topSpaceAssum have "(T{is T1})⟶(T{is anti-}IsUConnected)" by auto
  with ‹T{is T1}› show "T{is anti-}IsUConnected" by auto
next
  assume ASS:"T{is anti-}IsUConnected"
  {
    fix x y
    assume "x∈⋃T""y∈⋃T""x≠y"
    then have tot:"⋃(T{restricted to}{x,y})={x,y}" unfolding RestrictedTo_def by auto
    {
      assume AS:"∀U∈T. x∈U⟶y∈U"
      {
        assume "{y}{is closed in}(T{restricted to}{x,y})"
        moreover
        from ‹x≠y› have "{x,y}-{y}={x}" by auto
        ultimately have "{x}∈(T{restricted to}{x,y})" unfolding IsClosed_def by (simp only:tot)
        then obtain U where "U∈T""{x}={x,y}∩U" unfolding RestrictedTo_def by auto
        moreover
        with ‹x≠y› have "y∉{x}" "y∈{x,y}" by (blast+)
        with ‹{x}={x,y}∩U› have "y∉U" by auto
        moreover have "x∈{x}" by auto
        with ‹{x}={x,y}∩U› have "x∈U" by auto
        ultimately have "x∈U""y∉U""U∈T" by auto
        with AS have "False" by auto
      }
      then have y_no_cl:"¬({y}{is closed in}(T{restricted to}{x,y}))" by auto
      {
        fix A B 
        assume cl:"A{is closed in}(T{restricted to}{x,y})""B{is closed in}(T{restricted to}{x,y})""A∩B=0"
        with tot have "A⊆{x,y}""B⊆{x,y}""A∩B=0" unfolding IsClosed_def by auto
        then have "x∈A⟶x∉B""y∈A⟶y∉B""A⊆{x,y}""B⊆{x,y}" by auto
        {
          assume "x∈A"
          with ‹x∈A⟶x∉B›‹B⊆{x,y}› have "B⊆{y}" by auto
          then have "B=0∨B={y}" by auto
          with y_no_cl cl(2) have "B=0" by auto
        }
        moreover
        {
          assume "x∉A"
          with ‹A⊆{x,y}› have "A⊆{y}" by auto
          then have "A=0∨A={y}" by auto
          with y_no_cl cl(1) have "A=0" by auto
        }
        ultimately have "A=0∨B=0" by auto
      }
      then have "(T{restricted to}{x,y}){is ultraconnected}" unfolding IsUConnected_def by auto
      with ASS ‹x∈⋃T›‹y∈⋃T› have "{x,y}{is in the spectrum of}IsUConnected" unfolding antiProperty_def
        by auto
      then have "{x,y}≲1" using UConn_spectrum by auto
      moreover have "x∈{x,y}" by auto
      ultimately have "{x}={x,y}" using lepoll_1_is_sing[of "{x,y}""x"] by auto
      moreover
      have "y∈{x,y}" by auto
      ultimately have "y∈{x}" by auto
      then have "y=x" by auto
      then have "False" using ‹x≠y› by auto
    }
    then have "∃U∈T. x∈U∧y∉U" by auto
  }
  then show "T{is T1}" unfolding isT1_def by auto
qed

text‹Is is natural that separation axioms and connection axioms are anti-properties of each other;
as the concepts of connectedness and separation are opposite.›

text‹To end this section, let's try to charaterize anti-sober spaces.›

lemma sober_spectrum:
  shows "(A{is in the spectrum of}IsSober) ⟷ A≲1"
proof
  assume AS:"A{is in the spectrum of}IsSober"
  {
    assume "A=0"
    then have "A≲1" using empty_lepollI by auto
  }
  moreover
  { 
    assume "A≠0"
    note AS
    moreover
    have top:"{0,A}{is a topology}" unfolding IsATopology_def by auto
    moreover
    have "⋃{0,A}=A" by auto
    then have "⋃{0,A}≈A" by auto
    ultimately have "{0,A}{is sober}" using Spec_def by auto
    moreover
    have "{0,A}{is hyperconnected}" using Indiscrete_HConn by auto
    moreover
    have "{0,A}{restricted to}A={0,A}" unfolding RestrictedTo_def by auto
    moreover
    have "A{is closed in}{0,A}" unfolding IsClosed_def by auto
    moreover
    note ‹A≠0›
    ultimately have "∃x∈A. A=Closure({x},{0,A})∧ (∀y∈⋃{0, A}. A = Closure({y}, {0, A}) ⟶ y = x)" unfolding IsSober_def by auto
    then obtain x where "x∈A" "A=Closure({x},{0,A})" and reg:"∀y∈A. A = Closure({y}, {0, A}) ⟶ y = x" by auto
    {
      fix y assume "y∈A"
      with top have "Closure({y},{0,A}){is closed in}{0,A}" using topology0.cl_is_closed
        topology0_def by auto
      moreover
      from ‹y∈A› top have "y∈Closure({y},{0,A})" using topology0.cl_contains_set
        topology0_def by auto
      ultimately have "A-Closure({y},{0,A})∈{0,A}""Closure({y},{0,A})∩A≠0" unfolding IsClosed_def
        by auto
      then have "A-Closure({y},{0,A})=A∨A-Closure({y},{0,A})=0"
        by auto
      moreover
      from ‹y∈A›‹y∈Closure({y},{0,A})› have "y∈A""y∉A-Closure({y},{0,A})" by auto
      ultimately have "A-Closure({y},{0,A})=0" by (cases "A-Closure({y},{0,A})=A", simp, auto)
      moreover
      from ‹y∈A› top have "Closure({y},{0,A})⊆A" using topology0_def topology0.Top_3_L11(1) by blast
      then have "A-(A-Closure({y},{0,A}))=Closure({y},{0,A})" by auto
      ultimately have "A=Closure({y},{0,A})" by auto
    }
    with reg have "∀y∈A. x=y" by auto
    with ‹x∈A› have "A={x}" by blast
    then have "A≈1" using singleton_eqpoll_1 by auto
    then have "A≲1" using eqpoll_imp_lepoll by auto
  }
  ultimately show "A≲1" by auto
next
  assume "A≲1"
  {
    fix T assume "T{is a topology}""⋃T≈A"
    {
      assume "⋃T=0"
      then have "T{is sober}" unfolding IsSober_def by auto
    }
    moreover
    {
      assume "⋃T≠0"
      then obtain x where "x∈⋃T" by blast
      moreover
      from ‹⋃T≈A› ‹A≲1› have "⋃T≲1" using eq_lepoll_trans by auto
      ultimately have "⋃T={x}" using lepoll_1_is_sing by auto
      moreover
      have "T⊆Pow(⋃T)" by auto
      ultimately have "T⊆Pow({x})" by auto
      then have "T⊆{0,{x}}" by blast
      moreover
      from ‹T{is a topology}› have "0∈T" using empty_open by auto
      moreover
      from ‹T{is a topology}› have "⋃T∈T" unfolding IsATopology_def by auto
      with ‹⋃T={x}› have "{x}∈T" by auto
      ultimately have T_def:"T={0,{x}}" by auto
      then have dd:"Pow(⋃T)-{0}={{x}}" by auto
      {
        fix B assume "B∈Pow(⋃T)-{0}"
        with dd have B_def:"B={x}" by auto
        from ‹T{is a topology}› have "(⋃T){is closed in}T" using topology0_def topology0.Top_3_L1
          by auto
        with ‹⋃T={x}› ‹T{is a topology}› have "Closure({x},T)={x}" using topology0.Top_3_L8
          unfolding topology0_def by auto
        with B_def have "B=Closure({x},T)" by auto
        moreover
        {
          fix y assume "y∈⋃T"
          with ‹⋃T={x}› have "y=x" by auto
          }
        then have "(∀y∈⋃T. B = Closure({y}, T) ⟶ y = x)" by auto
        moreover note ‹x∈⋃T›
        ultimately have "(∃x∈⋃T. B = Closure({x}, T) ∧ (∀y∈⋃T. B = Closure({y}, T) ⟶ y = x))"
          by auto
      }
      then have "T{is sober}" unfolding IsSober_def by auto
    }
    ultimately have "T{is sober}" by blast
  }
  then show "A {is in the spectrum of} IsSober" unfolding Spec_def by auto
qed

theorem (in topology0)anti_sober:
  shows "(T{is anti-}IsSober) ⟷ T={0,⋃T}"
proof
  assume "T={0,⋃T}"
  {
    fix A assume "A∈Pow(⋃T)""(T{restricted to}A){is sober}"
    {
      assume "A=0"
      then have "A≲1" using empty_lepollI by auto
      then have "A{is in the spectrum of}IsSober" using sober_spectrum by auto
    }
    moreover
    {
      assume "A≠0"
      have "⋃T∈{0,⋃T}""0∈{0,⋃T}" by auto
      with ‹T={0,⋃T}› have "(⋃T)∈T" "0∈T" by auto
      with ‹A∈Pow(⋃T)› have "{0,A}⊆(T{restricted to}A)" unfolding RestrictedTo_def by auto
      moreover
      have "∀B∈{0,⋃T}. B=0∨B=⋃T" by auto
      with ‹T={0,⋃T}› have "∀B∈T. B=0