Theory Topology_ZF_properties_2

(* 
    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 ‹Properties in topology 2›

theory Topology_ZF_properties_2 imports Topology_ZF_7 Topology_ZF_1b
  Finite_ZF_1 Topology_ZF_11

begin

subsection‹Local properties.›
text‹This theory file deals with local topological properties; and applies local compactness
to the one point compactification.›

text‹We will say that a topological space is locally @term{"P"} iff every point has a neighbourhood basis
of subsets that have the property @term{"P"} as subspaces.›

definition
  IsLocally ("_{is locally}_" 90)
  where "T{is a topology}  T{is locally}P  (xT. bT. xb  (cPow(b). xInterior(c,T)  P(c,T)))"

subsection‹First examples›
text‹Our first examples deal with the locally finite property. Finiteness is a property of sets,
and hence it is preserved by homeomorphisms; which are in particular bijective.›

text‹The discrete topology is locally finite.›

lemma discrete_locally_finite:
  shows "Pow(A){is locally}(λA.(λB. Finite(A)))"
proof-
  have "bPow(A). (Pow(A){restricted to}b)=b" unfolding RestrictedTo_def by blast
  then have "b{{x}. xA}. Finite(b)" by auto moreover
  have reg:"SPow(A). Interior(S,Pow(A))=S" unfolding Interior_def by auto
  {
    fix x b assume "xPow(A)" "bPow(A)" "xb"
    then have "{x}b" "xInterior({x},Pow(A))" "Finite({x})" using reg by auto
    then have "cPow(b). xInterior(c,Pow(A))Finite(c)" by blast
  }
  then have "xPow(A). bPow(A). xb  (cPow(b). xInterior(c,Pow(A))  Finite(c))" by auto
  then show ?thesis using IsLocally_def[OF Pow_is_top] by auto
qed

text‹The included set topology is locally finite when the set is finite.›

lemma included_finite_locally_finite:
  assumes "Finite(A)" and "AX"
  shows "(IncludedSet(X,A)){is locally}(λA.(λB. Finite(A)))"
proof-
  have "bPow(X). bAb" by auto moreover
  note assms(1)
  ultimately have rr:"b{A{x}. xX}. Finite(b)" by force
  {
    fix x b assume "x(IncludedSet(X,A))" "b(IncludedSet(X,A))" "xb"
    then have "A{x}b" "A{x}{A{x}. xX}" and sub: "bX" unfolding IncludedSet_def by auto
    moreover have "A  {x}  X" using assms(2) sub xb by auto
    then have "xInterior(A{x},IncludedSet(X,A))" using interior_set_includedset[of "A{x}""X""A"] by auto
    ultimately have "cPow(b). xInterior(c,IncludedSet(X,A)) Finite(c)" using rr by blast
  }
  then have "x(IncludedSet(X,A)). b(IncludedSet(X,A)). xb  (cPow(b). xInterior(c,IncludedSet(X,A)) Finite(c))" by auto
  then show ?thesis using IsLocally_def includedset_is_topology by auto
qed

subsection‹Local compactness›

definition
  IsLocallyComp ("_{is locally-compact}" 70)
  where "T{is locally-compact}T{is locally}(λB. λT. B{is compact in}T)"

text‹We center ourselves in local compactness, because it is a very important tool in topological groups
and compactifications.›

text‹If a subset is compact of some cardinal for a topological space, it is compact of the same cardinal
in the subspace topology.›

lemma compact_imp_compact_subspace:
  assumes "A{is compact of cardinal}K{in}T" "AB"
  shows "A{is compact of cardinal}K{in}(T{restricted to}B)" unfolding IsCompactOfCard_def
proof
  from assms show C:"Card(K)" unfolding IsCompactOfCard_def by auto
  from assms have "AT" unfolding IsCompactOfCard_def by auto
  then have AA:"A(T{restricted to}B)" using assms(2) unfolding RestrictedTo_def by auto moreover
  {
    fix M assume "MPow(T{restricted to}B)" "AM"
    let ?M="{ST. BSM}"
    from MPow(T{restricted to}B) have "M?M" unfolding RestrictedTo_def by auto
    with AM have "A?M""?MPow(T)" by auto
    with assms have "NPow(?M). ANNK" unfolding IsCompactOfCard_def by auto
    then obtain N where "NPow(?M)" "AN" "NK" by auto
    then have "N{restricted to}BM" unfolding RestrictedTo_def FinPow_def by auto
    moreover
    let ?f="{𝔅,B𝔅. 𝔅N}"
    have "?f:N(N{restricted to}B)" unfolding Pi_def function_def domain_def RestrictedTo_def by auto
    then have "?fsurj(N,N{restricted to}B)" unfolding surj_def RestrictedTo_def using apply_equality
      by auto
    from NK have "NK" unfolding lesspoll_def by auto
    with ?fsurj(N,N{restricted to}B) have "N{restricted to}BN" using surj_fun_inv_2 Card_is_Ord C by auto
    with NK have "N{restricted to}BK" using lesspoll_trans1 by auto
    moreover from AN have "A(N{restricted to}B)" using assms(2) unfolding RestrictedTo_def by auto
    ultimately have "NPow(M). AN  NK" by auto
  }
  with AA show "A  (T {restricted to} B)  (MPow(T {restricted to} B). A  M  (NPow(M). A  N  NK))" by auto
qed

text‹The converse of the previous result is not always true. For compactness, it holds because the axiom of finite choice
always holds.›

lemma compact_subspace_imp_compact:
  assumes "A{is compact in}(T{restricted to}B)" "AB"
  shows "A{is compact in}T" unfolding IsCompact_def
proof
  from assms show "AT" unfolding IsCompact_def RestrictedTo_def by auto
next
  {
    fix M assume "MPow(T)" "AM"
    let ?M="M{restricted to}B"
    from MPow(T) have "?MPow(T{restricted to}B)" unfolding RestrictedTo_def by auto
    from AM have "A?M" unfolding RestrictedTo_def using assms(2) by auto
    with assms ?MPow(T{restricted to}B) obtain N where "NFinPow(?M)" "AN" unfolding IsCompact_def by blast
    from NFinPow(?M) have "Nnat" unfolding FinPow_def Finite_def using n_lesspoll_nat eq_lesspoll_trans
      by auto
    then have "Finite(N)" using lesspoll_nat_is_Finite by auto
    then obtain n where "nnat" "Nn" unfolding Finite_def by auto
    then have "Nn" using eqpoll_imp_lepoll by auto
    moreover 
    {
      fix BB assume "BBN"
      with NFinPow(?M) have "BB?M" unfolding FinPow_def by auto
      then obtain S where "SM" and "BB=BS" unfolding RestrictedTo_def by auto
      then have "S{SM. BS=BB}" by auto
      then obtain "{SM. BS=BB}0" by auto
    }
    then have "BBN. ((λWN. {SM. BS=W})`BB)0" by auto moreover
    from nnat have " (N  n  (tN. (λWN. {SM. BS=W}) ` t  0)  (f. f  Pi(N,λt. (λWN. {SM. BS=W}) ` t)  (tN. f ` t  (λWN. {SM. BS=W}) ` t)))" using finite_choice unfolding AxiomCardinalChoiceGen_def by blast
    ultimately
    obtain f where AA:"fPi(N,λt. (λWN. {SM. BS=W}) ` t)" "tN. f`t(λWN. {SM. BS=W}) ` t" by blast
    from AA(2) have ss:"tN. f`t{SM. BS=t}" using beta_if by auto
    then have "{f`t. tN}M" by auto
    {
      fix t assume "tN"
      with ss have "f`t{SM. BSN}" by auto
    }
    with AA(1) have FF:"f:N{SM. BSN}" unfolding Pi_def Sigma_def using beta_if by auto moreover
    {
      fix aa bb assume AAA:"aaN" "bbN" "f`aa=f`bb"
      from AAA(1) ss have "B (f`aa) =aa" by auto
      with AAA(3) have "B(f`bb)=aa" by auto
      with ss AAA(2) have "aa=bb" by auto
    }
    ultimately have "finj(N,{SM. BSN})" unfolding inj_def by auto
    then have "fbij(N,range(f))" using inj_bij_range by auto
    then have "fbij(N,f``N)" using range_image_domain FF by auto
    then have "fbij(N,{f`t. tN})" using func_imagedef FF by auto
    then have "N{f`t. tN}" unfolding eqpoll_def by auto
    with Nn have "{f`t. tN}n" using eqpoll_sym eqpoll_trans by blast
    with nnat have "Finite({f`t. tN})" unfolding Finite_def by auto
    with ss have "{f`t. tN}FinPow(M)" unfolding FinPow_def by auto moreover
    {
      fix aa assume "aaA"
      with AN obtain b where "bN" and "aab" by auto
      with ss have "B(f`b)=b" by auto
      with aab have "aaB(f`b)" by auto
      then have "aa f`b" by auto
      with bN have "aa{f`t. tN}" by auto
    }
    then have "A{f`t. tN}" by auto ultimately
    have "RFinPow(M). AR" by auto
  }
  then show "MPow(T). A  M  (NFinPow(M). A  N)" by auto
qed

text‹If the axiom of choice holds for some cardinal,
then we can drop the compact sets of that cardial are compact of the same cardinal
as subspaces of every superspace.›

lemma Kcompact_subspace_imp_Kcompact:
  assumes "A{is compact of cardinal}Q{in}(T{restricted to}B)" "AB" "({the axiom of} Q {choice holds})"
  shows "A{is compact of cardinal}Q{in}T"
proof -
  from assms(1) have a1:"Card(Q)" unfolding IsCompactOfCard_def RestrictedTo_def by auto
  from assms(1) have a2:"AT" unfolding IsCompactOfCard_def RestrictedTo_def by auto
  {
    fix M assume "MPow(T)" "AM"
    let ?M="M{restricted to}B"
    from MPow(T) have "?MPow(T{restricted to}B)" unfolding RestrictedTo_def by auto
    from AM have "A?M" unfolding RestrictedTo_def using assms(2) by auto
    with assms ?MPow(T{restricted to}B) obtain N where N:"NPow(?M)" "AN" "N  Q" unfolding IsCompactOfCard_def by blast
    from N(3) have "NQ" using lesspoll_imp_lepoll by auto moreover 
    {
      fix BB assume "BBN"
      with NPow(?M) have "BB?M" unfolding FinPow_def by auto
      then obtain S where "SM" and "BB=BS" unfolding RestrictedTo_def by auto
      then have "S{SM. BS=BB}" by auto
      then obtain "{SM. BS=BB}0" by auto
    }
    then have "BBN. ((λWN. {SM. BS=W})`BB)0" by auto moreover
    have " (N  Q  (tN. (λWN. {SM. BS=W}) ` t  0)  (f. f  Pi(N,λt. (λWN. {SM. BS=W}) ` t)  (tN. f ` t  (λWN. {SM. BS=W}) ` t)))" 
      using assms(3) unfolding AxiomCardinalChoiceGen_def by blast
    ultimately
    obtain f where AA:"fPi(N,λt. (λWN. {SM. BS=W}) ` t)" "tN. f`t(λWN. {SM. BS=W}) ` t" by blast
    from AA(2) have ss:"tN. f`t{SM. BS=t}" using beta_if by auto
    then have "{f`t. tN}M" by auto
    {
      fix t assume "tN"
      with ss have "f`t{SM. BSN}" by auto
    }
    with AA(1) have FF:"f:N{SM. BSN}" unfolding Pi_def Sigma_def using beta_if by auto moreover
    {
      fix aa bb assume AAA:"aaN" "bbN" "f`aa=f`bb"
      from AAA(1) ss have "B (f`aa) =aa" by auto
      with AAA(3) have "B(f`bb)=aa" by auto
      with ss AAA(2) have "aa=bb" by auto
    }
    ultimately have "finj(N,{SM. BSN})" unfolding inj_def by auto
    then have "fbij(N,range(f))" using inj_bij_range by auto
    then have "fbij(N,f``N)" using range_image_domain FF by auto
    then have "fbij(N,{f`t. tN})" using func_imagedef FF by auto
    then have "N{f`t. tN}" unfolding eqpoll_def by auto
    with NQ have "{f`t. tN}Q" using eqpoll_sym eq_lesspoll_trans by blast moreover
    with ss have "{f`t. tN}Pow(M)" unfolding FinPow_def by auto moreover
    {
      fix aa assume "aaA"
      with AN obtain b where "bN" and "aab" by auto
      with ss have "B(f`b)=b" by auto
      with aab have "aaB(f`b)" by auto
      then have "aa f`b" by auto
      with bN have "aa{f`t. tN}" by auto
    }
    then have "A{f`t. tN}" by auto ultimately
    have "RPow(M). AR  RQ" by auto
  }
  then show ?thesis using a1 a2 unfolding IsCompactOfCard_def by auto
qed

text‹Every set, with the cofinite topology is compact.›

lemma cofinite_compact:
  shows "X {is compact in}(CoFinite X)" unfolding IsCompact_def
proof
  show "X(CoFinite X)" using union_cocardinal unfolding Cofinite_def by auto
next
  {
    fix M assume "MPow(CoFinite X)" "XM"
    {
      assume "M=0M={0}"
      then have "MFinPow(M)" unfolding FinPow_def by auto
      with XM have "NFinPow(M). XN" by auto
    }
    moreover
    {
      assume "M0""M{0}"
      then obtain U where "UM""U0" by auto
      with MPow(CoFinite X) have "UCoFinite X" by auto
      with U0 have "UX" "(X-U)nat" unfolding Cofinite_def CoCardinal_def by auto
      then have "Finite(X-U)" using lesspoll_nat_is_Finite by auto
      then have "(X-U){is in the spectrum of}(λT. (T){is compact in}T)" using compact_spectrum
        by auto
      then have "(((CoFinite (X-U)))X-U)  (((CoFinite (X-U))){is compact in}(CoFinite (X-U)))" unfolding Spec_def
        using InfCard_nat CoCar_is_topology unfolding Cofinite_def by auto
      then have com:"(X-U){is compact in}(CoFinite (X-U))" using union_cocardinal unfolding Cofinite_def by auto
      have "(X-U)X=X-U" by auto
      then have "(CoFinite X){restricted to}(X-U)=(CoFinite (X-U))" using subspace_cocardinal unfolding Cofinite_def by auto
      with com have "(X-U){is compact in}(CoFinite X)" using compact_subspace_imp_compact[of "X-U""CoFinite X""X-U"] by auto
      moreover have "X-UM" using XM by auto
      moreover note MPow(CoFinite X)
      ultimately have "NFinPow(M). X-UN" unfolding IsCompact_def by auto
      then obtain N where "NM" "Finite(N)" "X-UN" unfolding FinPow_def by auto
      with UM have "N {U}M" "Finite(N {U})" "X(N {U})" by auto
      then have "NFinPow(M). XN" unfolding FinPow_def by blast
    }
    ultimately
    have "NFinPow(M). XN" by auto
  }
  then show "MPow(CoFinite X). X  M  (NFinPow(M). X  N)" by auto
qed

text‹A corollary is then that the cofinite topology is locally compact; since every subspace
of a cofinite space is cofinite.›

corollary cofinite_locally_compact:
  shows "(CoFinite X){is locally-compact}"
proof-
  have cof:"topology0(CoFinite X)" and cof1:"(CoFinite X){is a topology}" 
    using CoCar_is_topology InfCard_nat Cofinite_def unfolding topology0_def by auto
  {
    fix x B assume "x(CoFinite X)" "B(CoFinite X)" "xB"
    then have "xInterior(B,CoFinite X)" using topology0.Top_2_L3[OF cof] by auto moreover
    from B(CoFinite X) have "BX" unfolding Cofinite_def CoCardinal_def by auto
    then have "BX=B" by auto
    then have "(CoFinite X){restricted to}B=CoFinite B" using subspace_cocardinal unfolding Cofinite_def by auto
    then have "B{is compact in}((CoFinite X){restricted to}B)" using cofinite_compact
      union_cocardinal unfolding Cofinite_def by auto
    then have "B{is compact in}(CoFinite X)" using compact_subspace_imp_compact by auto
    ultimately have "cPow(B). xInterior(c,CoFinite X) c{is compact in}(CoFinite X)" by auto
  }
  then have "(x(CoFinite X). b(CoFinite X). xb  (cPow(b). xInterior(c,CoFinite X)  c{is compact in}(CoFinite X)))"
    by auto
  then show ?thesis unfolding IsLocallyComp_def IsLocally_def[OF cof1] by auto
qed

text‹In every locally compact space, by definition, every point has a compact neighbourhood.›

theorem (in topology0) locally_compact_exist_compact_neig:
  assumes "T{is locally-compact}"
  shows "xT. APow(T). A{is compact in}T  xint(A)"
proof-
  {
    fix x assume "xT" moreover
    then have "T0" by auto
    have "TT" using union_open topSpaceAssum by auto
    ultimately have "cPow(T). xint(c) c{is compact in}T" using assms 
      IsLocally_def topSpaceAssum unfolding IsLocallyComp_def by auto
    then have "cPow(T). c{is compact in}T  xint(c)" by auto
  }
  then show ?thesis by auto
qed

text‹In Hausdorff spaces, the previous result is an equivalence.›

theorem (in topology0) exist_compact_neig_T2_imp_locally_compact:
  assumes "xT. APow(T). xint(A)  A{is compact in}T" "T{is T2}"
  shows "T{is locally-compact}"
proof-
  {
    fix x assume "xT"
    with assms(1) obtain A where "APow(T)" "xint(A)" and Acom:"A{is compact in}T" by blast
    then have Acl:"A{is closed in}T" using in_t2_compact_is_cl assms(2) by auto
    then have sub:"AT" unfolding IsClosed_def by auto
    {
      fix U assume "UT" "xU"
      let ?V="int(AU)"
      from xU xint(A) have "xU(int (A))" by auto
      moreover from UT have "U(int(A))T" using Top_2_L2 topSpaceAssum unfolding IsATopology_def
        by auto moreover
      have "U(int(A))AU" using Top_2_L1 by auto
      ultimately have "x?V" using Top_2_L5 by blast
      have "?VA" using Top_2_L1 by auto
      then have "cl(?V)A" using Acl Top_3_L13 by auto
      then have "Acl(?V)=cl(?V)" by auto moreover
      have clcl:"cl(?V){is closed in}T" using cl_is_closed(1) ?VA AT by auto
      ultimately have comp:"cl(?V){is compact in}T" using Acom compact_closed[of "A""nat""T""cl(?V)"] Compact_is_card_nat
        by auto
      {
        then have "cl(?V){is compact in}(T{restricted to}cl(?V))" using compact_imp_compact_subspace[of "cl(?V)""nat""T"] Compact_is_card_nat
          by auto moreover
        have "(T{restricted to}cl(?V))=cl(?V)" unfolding RestrictedTo_def using clcl unfolding IsClosed_def by auto moreover
        ultimately have "((T{restricted to}cl(?V))){is compact in}(T{restricted to}cl(?V))" by auto
      }
      then have "((T{restricted to}cl(?V))){is compact in}(T{restricted to}cl(?V))" by auto moreover
      have "(T{restricted to}cl(?V)){is T2}" using assms(2) T2_here clcl unfolding IsClosed_def by auto
      ultimately have "(T{restricted to}cl(?V)){is T4}" using topology0.T2_compact_is_normal unfolding topology0_def
        using Top_1_L4 unfolding isT4_def using T2_is_T1 by auto
      then have clvreg:"(T{restricted to}cl(?V)){is regular}" using topology0.T4_is_T3 unfolding topology0_def isT3_def using Top_1_L4
        by auto 
      have "?Vcl(?V)" using cl_contains_set ?VA AT by auto
      then have "?V(T{restricted to}cl(?V))" unfolding RestrictedTo_def using Top_2_L2 by auto
      with x?V obtain W where Wop:"W(T{restricted to}cl(?V))" and clcont:"Closure(W,(T{restricted to}cl(?V)))?V" and cinW:"xW"
      using topology0.regular_imp_exist_clos_neig unfolding topology0_def using Top_1_L4 clvreg
        by blast
      from clcont Wop have "W?V" using topology0.cl_contains_set unfolding topology0_def using Top_1_L4 by auto
      with Wop have "W(T{restricted to}cl(?V)){restricted to}?V" unfolding RestrictedTo_def by auto
      moreover from ?VA AT have "?VT" by auto
      then have "?Vcl(?V)""cl(?V)T" using ?Vcl(?V) Top_3_L11(1) by auto
      then have "(T{restricted to}cl(?V)){restricted to}?V=(T{restricted to}?V)" using subspace_of_subspace by auto
      ultimately have "W(T{restricted to}?V)" by auto
      then obtain UU where "UUT" "W=UU?V" unfolding RestrictedTo_def by auto
      then have "WT" using Top_2_L2 topSpaceAssum unfolding IsATopology_def by auto moreover
      have "WClosure(W,(T{restricted to}cl(?V)))" using topology0.cl_contains_set unfolding topology0_def
        using Top_1_L4 Wop by auto
      ultimately have A1:"xint(Closure(W,(T{restricted to}cl(?V))))" using Top_2_L6 cinW by auto
      from clcont have A2:"Closure(W,(T{restricted to}cl(?V)))U" using Top_2_L1 by auto
      have clwcl:"Closure(W,(T{restricted to}cl(?V))) {is closed in}(T{restricted to}cl(?V))"
        using topology0.cl_is_closed(1) Top_1_L4 Wop unfolding topology0_def by auto
      from comp have "cl(?V){is compact in}(T{restricted to}cl(?V))" using compact_imp_compact_subspace[of "cl(?V)""nat""T"] Compact_is_card_nat
          by auto
      with clwcl have "((cl(?V)(Closure(W,(T{restricted to}cl(?V)))))){is compact in}(T{restricted to}cl(?V))"
        using compact_closed Compact_is_card_nat by auto moreover
      from clcont have cont:"(Closure(W,(T{restricted to}cl(?V))))cl(?V)" using cl_contains_set ?VAAT
        by blast
      then have "((cl(?V)(Closure(W,(T{restricted to}cl(?V))))))=Closure(W,(T{restricted to}cl(?V)))" by auto
      ultimately have "Closure(W,(T{restricted to}cl(?V))){is compact in}(T{restricted to}cl(?V))" by auto
      then have "Closure(W,(T{restricted to}cl(?V))){is compact in}T" using compact_subspace_imp_compact[of "Closure(W,T{restricted to}cl(?V))"]
        cont by auto
      with A1 A2 have "cPow(U). xint(c)c{is compact in}T" by auto
    }
    then have "UT. xU  (cPow(U). xint(c)c{is compact in}T)" by auto
  }
  then show ?thesis unfolding IsLocally_def[OF topSpaceAssum] IsLocallyComp_def by auto
qed

subsection‹Compactification by one point›

text‹Given a topological space, we can always add one point to the space and get a new compact topology; as we
will check in this section.›

definition 
  OPCompactification ("{one-point compactification of}_" 90)
  where "{one-point compactification of}TT{{T}((T)-K). K{BPow(T). B{is compact in}T  B{is closed in}T}}"

text‹Firstly, we check that what we defined is indeed a topology.›

theorem (in topology0) op_comp_is_top:
  shows "({one-point compactification of}T){is a topology}" unfolding IsATopology_def
proof(safe)
  fix M assume "M{one-point compactification of}T"
  then have disj:"MT{{T}((T)-K). K{BPow(T). B{is compact in}T  B{is closed in}T}}" unfolding OPCompactification_def by auto
  let ?MT="{AM. AT}"
  have "?MTT" by auto
  then have c1:"?MTT" using topSpaceAssum unfolding IsATopology_def by auto
  let ?MK="{AM. AT}"
  have "M=?MK  ?MT" by auto
  from disj have "?MK{AM. A{{T}((T)-K). K{BPow(T). B{is compact in}T  B{is closed in}T}}}" by auto
  moreover have N:"T(T)" using mem_not_refl by auto
  {
    fix B assume "BM" "B{{T}((T)-K). K{BPow(T). B{is compact in}T  B{is closed in}T}}"
    then obtain K where "KPow(T)" "B={T}((T)-K)" by auto
    with N have "TB" by auto
    with N have "BT" by auto
    with BM have "B?MK" by auto
  }
  then have "{AM. A{{T}((T)-K). K{BPow(T). B{is compact in}T  B{is closed in}T}}}?MK" by auto
  ultimately have MK_def:"?MK={AM. A{{T}((T)-K). K{BPow(T). B{is compact in}T  B{is closed in}T}}}" by auto
  let ?KK="{KPow(T). {T}((T)-K)?MK}"
  {
    assume "?MK=0"
    then have "M=?MT" by auto
    then have "MT" using c1 by auto
    then have "M{one-point compactification of}T" unfolding OPCompactification_def by auto
  }
  moreover
  {
    assume "?MK0"
    then obtain A where "A?MK" by auto
    then obtain K1 where "A={T}((T)-K1)" "K1Pow(T)" "K1{is closed in}T" "K1{is compact in}T" using MK_def by auto
    with A?MK have "?KKK1" by auto
    from A?MK A={T}((T)-K1) K1Pow(T) have "?KK0" by blast
    {
      fix K assume "K?KK"
      then have "{T}((T)-K)?MK" "KT" by auto
      then obtain KK where A:"{T}((T)-K)={T}((T)-KK)" "KKT" "KK{is compact in}T" "KK{is closed in}T" using MK_def by auto
      note A(1) moreover
      have "(T)-K{T}((T)-K)" "(T)-KK{T}((T)-KK)" by auto
      ultimately have "(T)-K{T}((T)-KK)" "(T)-KK{T}((T)-K)" by auto moreover
      from N have "T(T)-K" "T(T)-KK" by auto ultimately
      have "(T)-K((T)-KK)" "(T)-KK((T)-K)" by auto
      then have "(T)-K=(T)-KK" by auto moreover
      from KT have "K=(T)-((T)-K)" by auto ultimately
      have "K=(T)-((T)-KK)" by auto
      with KKT have "K=KK" by auto
      with A(4) have "K{is closed in}T" by auto
    }
    then have "K?KK. K{is closed in}T" by auto
    with ?KK0 have "(?KK){is closed in}T" using Top_3_L4 by auto
    with K1{is compact in}T have "(K1(?KK)){is compact in}T" using Compact_is_card_nat
      compact_closed[of "K1""nat""T""?KK"] by auto moreover
    from ?KKK1 have "K1(?KK)=(?KK)" by auto ultimately
    have "(?KK){is compact in}T" by auto
    with (?KK){is closed in}T ?KKK1 K1Pow(T) have "({T}((T)-(?KK)))({one-point compactification of}T)"
      unfolding OPCompactification_def by blast
    have t:"?MK={AM. A{{T}((T)-K). K{BPow(T). B{is compact in}T  B{is closed in}T}}}"
      using MK_def by auto
    {
      fix x assume "x?MK"
      with t have "x{AM. A{{T}((T)-K). K{BPow(T). B{is compact in}T  B{is closed in}T}}}" by auto 
      then have "AA{AM. A{{T}((T)-K). K{BPow(T). B{is compact in}T  B{is closed in}T}}}. xAA"
        using Union_iff by auto
      then obtain AA where AAp:"AA{AM. A{{T}((T)-K). K{BPow(T). B{is compact in}T  B{is closed in}T}}}" "xAA" by auto
      then obtain K2 where "AA={T}((T)-K2)" "K2Pow(T)""K2{is compact in}T" "K2{is closed in}T" by auto
      with xAA have "x=T  (x(T)  xK2)" by auto
      from K2Pow(T) AA={T}((T)-K2) AAp(1) MK_def have "K2?KK" by auto
      then have "?KKK2" by auto
      with x=T  (x(T)  xK2) have "x=T(xT  x?KK)" by auto
     then have "x{T}((T)-(?KK))" by auto
    }
    then have "?MK{T}((T)-(?KK))" by auto
    moreover
    {
      fix x assume "x{T}((T)-(?KK))"
      then have "x=T(x(T) x?KK)" by auto
      with ?KK0 obtain K2 where "K2?KK" "x=T(xT xK2)" by auto
      then have "{T}((T)-K2)?MK" by auto
      with x=T(xT xK2) have "x?MK" by auto
    }
    then have "{T}((T)-(?KK))?MK" by (safe,auto)
    ultimately have "?MK={T}((T)-(?KK))" by blast
    from ?MTT have "T-(T-?MT)=?MT" by auto
    with ?MTT have "(T-?MT){is closed in}T" unfolding IsClosed_def by auto
    have "((T)-(?KK))(T-(T-?MT))=(T)-((?KK)(T-?MT))" by auto
    then have "({T}((T)-(?KK)))(T-(T-?MT))={T}((T)-((?KK)(T-?MT)))" by auto
    with ?MK={T}((T)-(?KK))T-(T-?MT)=?MT have "?MK?MT={T}((T)-((?KK)(T-?MT)))"
    by auto
    with M=?MK ?MT have unM:"M={T}((T)-((?KK)(T-?MT)))" by auto
    have "((?KK)(T-?MT)) {is closed in}T" using (?KK){is closed in}T(T-(?MT)){is closed in}T
      Top_3_L5 by auto
    moreover  
    note (T-(?MT)){is closed in}T (?KK){is compact in}T
    then have "((?KK)(T-?MT)){is compact of cardinal}nat{in}T" using compact_closed[of "?KK""nat""T""(T-?MT)"] Compact_is_card_nat
      by auto
    then have "((?KK)(T-?MT)){is compact in}T" using Compact_is_card_nat by auto
    ultimately have "{T}(T-((?KK)(T-?MT))){one-point compactification of}T"
      unfolding OPCompactification_def IsClosed_def by auto
    with unM have "M{one-point compactification of}T" by auto
  }
  ultimately show "M{one-point compactification of}T" by auto
next
  fix U V assume "U{one-point compactification of}T" and "V{one-point compactification of}T"
  then have A:"UT(KUPow(T). U={T}(T-KU)KU{is closed in}TKU{is compact in}T)"
    "VT(KVPow(T). V={T}(T-KV)KV{is closed in}TKV{is compact in}T)" unfolding OPCompactification_def
    by auto
 have N:"T(T)" using mem_not_refl by auto
  {
    assume "UT""VT"
    then have "UVT" using topSpaceAssum unfolding IsATopology_def by auto
    then have "UV{one-point compactification of}T" unfolding OPCompactification_def
    by auto
  }
  moreover
  {
    assume "UT""VT"
    then obtain KV where V:"KV{is closed in}T""KV{is compact in}T""V={T}(T-KV)"
    using A(2) by auto
    with N UT have "TU" by auto
    then have "TUV" by auto
    then have "UV=U(T-KV)" using V(3) by auto
    moreover have "T-KVT" using V(1) unfolding IsClosed_def by auto
    with UT have "U(T-KV)T" using topSpaceAssum unfolding IsATopology_def by auto
    with UV=U(T-KV) have "UVT" by auto
    then have "UV{one-point compactification of}T" unfolding OPCompactification_def by auto
    }
  moreover
  {
    assume "UT""VT"
    then obtain KV where V:"KV{is closed in}T""KV{is compact in}T""U={T}(T-KV)"
    using A(1) by auto
    with N VT have "TV" by auto
    then have "TUV" by auto
    then have "UV=(T-KV)V" using V(3) by auto
    moreover have "T-KVT" using V(1) unfolding IsClosed_def by auto
    with VT have "(T-KV)VT" using topSpaceAssum unfolding IsATopology_def by auto
    with UV=(T-KV)V have "UVT" by auto
    then have "UV{one-point compactification of}T" unfolding OPCompactification_def by auto
  }
  moreover
  {
    assume "UT""VT"
    then obtain KV KU where V:"KV{is closed in}T""KV{is compact in}T""V={T}(T-KV)"
     and U:"KU{is closed in}T""KU{is compact in}T""U={T}(T-KU)"
    using A by auto
    with V(3) U(3) have "TUV" by auto
    then have "UV={T}((T-KV)(T-KU))" using V(3) U(3) by auto
    moreover have "T-KVT""T-KUT" using V(1) U(1) unfolding IsClosed_def by auto
    then have "(T-KV)(T-KU)T" using topSpaceAssum unfolding IsATopology_def by auto
    then have "(T-KV)(T-KU)=T-(T-((T-KV)(T-KU)))" by auto moreover
    with (T-KV)(T-KU)T have "(T-(T-KV)(T-KU)){is closed in}T" unfolding IsClosed_def
      by auto moreover
    from V(1) U(1) have "(T-(T-KV)(T-KU))=KVKU" unfolding IsClosed_def by auto
    with V(2) U(2) have "(T-(T-KV)(T-KU)){is compact in}T" using union_compact[of "KV""nat""T""KU"] Compact_is_card_nat
      InfCard_nat by auto ultimately
    have "UV{one-point compactification of}T" unfolding OPCompactification_def by auto
  }
  ultimately show "UV{one-point compactification of}T" by auto
qed

text‹The original topology is an open subspace of the new topology.›

theorem (in topology0) open_subspace:
  shows "T{one-point compactification of}T" and "({one-point compactification of}T){restricted to}T=T"
proof-
  show "T{one-point compactification of}T"
  unfolding OPCompactification_def using topSpaceAssum unfolding IsATopology_def by auto
  have "T({one-point compactification of}T){restricted to}T" unfolding OPCompactification_def RestrictedTo_def by auto
  moreover
  {
    fix A assume "A({one-point compactification of}T){restricted to}T"
    then obtain R where "R({one-point compactification of}T)" "A=TR" unfolding RestrictedTo_def by auto
    then obtain K where K:"RT  (R={T}(T-K)  K{is closed in}T)" unfolding OPCompactification_def by auto
    with A=TR have "(A=RRT)(A=T-K  K{is closed in}T)" using mem_not_refl unfolding IsClosed_def by auto
    with K have "AT" unfolding IsClosed_def by auto
  }
  ultimately
  show "({one-point compactification of}T){restricted to}T=T" by auto
qed

text‹We added only one new point to the space.›

lemma (in topology0) op_compact_total:
  shows "({one-point compactification of}T)={T}(T)"
proof-
  have "0{is compact in}T" unfolding IsCompact_def FinPow_def by auto
  moreover note Top_3_L2 ultimately have TT:"0{APow(T). A{is compact in}T A{is closed in}T}" by auto
  have "({one-point compactification of}T)=(T)({{T}(T-K). K{BPow(T). B{is compact in}TB{is closed in}T}})" unfolding OPCompactification_def
    by blast
  also have "=(T){T}({(T-K). K{BPow(T). B{is compact in}TB{is closed in}T}})" using TT by auto
  ultimately show "({one-point compactification of}T)={T}(T)" by auto
qed

text‹The one point compactification, gives indeed a compact topological space.›

theorem (in topology0) compact_op:
  shows "({T}(T)){is compact in}({one-point compactification of}T)" unfolding IsCompact_def
proof(safe)
  have "0{is compact in}T" unfolding IsCompact_def FinPow_def by auto
  moreover note Top_3_L2 ultimately have "0{APow(T). A{is compact in}T A{is closed in}T}" by auto
  then have "{T}(T){one-point compactification of}T" unfolding OPCompactification_def by auto
  then show "T  {one-point compactification of}T" by auto
next
  fix x B assume "xB""BT"
  then show "x({one-point compactification of}T)" using open_subspace by auto
next
  fix M assume A:"M({one-point compactification of}T)" "{T}  T  M"
  then obtain R where "RM""TR" by auto
  have "TT" using mem_not_refl by auto
  with RM TR A(1) obtain K where K:"R={T}(T-K)" "K{is compact in}T""K{is closed in}T"
    unfolding OPCompactification_def by auto
  from K(1,2) have B:"{T}  (T) = R  K" unfolding IsCompact_def by auto
  with A(2) have "KM" by auto
  from K(2) have "K{is compact in}(({one-point compactification of}T){restricted to}T)" using open_subspace(2)
    by auto
  then have "K{is compact in}({one-point compactification of}T)" using compact_subspace_imp_compact
    K{is closed in}T unfolding IsClosed_def by auto
  with KM A(1) have "(NFinPow(M). K  N)" unfolding IsCompact_def by auto
  then obtain N where "NFinPow(M)" "KN" by auto
  with RM have "(N {R})FinPow(M)""RK(N{R})" unfolding FinPow_def by auto
  with B show "NFinPow(M). {T}  (T)N" by auto
qed

text‹The one point compactification is Hausdorff iff the original space is also
Hausdorff and locally compact.›

lemma (in topology0) op_compact_T2_1:
  assumes "({one-point compactification of}T){is T2}"
  shows "T{is T2}"
  using T2_here[OF assms, of "T"] open_subspace by auto

lemma (in topology0) op_compact_T2_2:
  assumes "({one-point compactification of}T){is T2}"
  shows "T{is locally-compact}"
proof-
  {
    fix x assume "xT"
    then have "x{T}(T)" by auto
    moreover have "T{T}(T)" by auto moreover
    from xT have "xT" using mem_not_refl by auto
    ultimately have "U{one-point compactification of}T. V{one-point compactification of}T. x  U  (T)  V  U  V = 0"
      using assms op_compact_total unfolding isT2_def by auto
    then obtain U V where UV:"U{one-point compactification of}T""V{one-point compactification of}T"
      "xU""TV""UV=0" by auto
    from V{one-point compactification of}T TV mem_not_refl obtain K where K:"V={T}(T-K)""K{is closed in}T""K{is compact in}T"
      unfolding OPCompactification_def by auto
    from U{one-point compactification of}T have "U{T}(T)" unfolding OPCompactification_def 
      using op_compact_total by auto
    with UV=0 K have "UK""KT" unfolding IsClosed_def by auto
    then have "(T)U=U" by auto moreover
    from UV(1) have "((T)U)({one-point compactification of}T){restricted to}T" 
      unfolding RestrictedTo_def by auto
    ultimately have "UT" using open_subspace(2) by auto
    with xUUK have "xint(K)" using Top_2_L6 by auto
    with KT K{is compact in}T have "APow(T). xint(A) A{is compact in}T" by auto
  }
  then have "xT. APow(T). xint(A) A{is compact in}T" by auto
  then show ?thesis using op_compact_T2_1[OF assms] exist_compact_neig_T2_imp_locally_compact
    by auto
qed

lemma (in topology0) op_compact_T2_3:
  assumes "T{is locally-compact}" "T{is T2}"
  shows "({one-point compactification of}T){is T2}"
proof-
  {
    fix x y assume "xy""x({one-point compactification of}T)""y({one-point compactification of}T)"
    then have S:"x{T}(T)""y{T}(T)" using op_compact_total by auto
    {
      assume "xT""yT"
      with xy have "UT. VT. xUyVUV=0" using assms(2) unfolding isT2_def by auto
      then have "U({one-point compactification of}T). V({one-point compactification of}T). xUyVUV=0"
        unfolding OPCompactification_def by auto
    }
    moreover
    {
      assume "xTyT"
      with S have "x=Ty=T" by auto
      with xy have "(x=TyT)(y=TxT)" by auto
      with S have "(x=TyT)(y=TxT)" by auto
      then obtain Ky Kx where "(x=T Ky{is compact in}Tyint(Ky))(y=T Kx{is compact in}Txint(Kx))"
        using assms(1) locally_compact_exist_compact_neig by blast
      then have "(x=T Ky{is compact in}T Ky{is closed in}Tyint(Ky))(y=T Kx{is compact in}T Kx{is closed in}Txint(Kx))"
        using in_t2_compact_is_cl assms(2) by auto
      then have "(x{T}(T-Ky)yint(Ky) Ky{is compact in}T Ky{is closed in}T)(y{T}(T-Kx)xint(Kx) Kx{is compact in}T Kx{is closed in}T)"
        by auto moreover
      {
        fix K
        assume A:"K{is closed in}T""K{is compact in}T"
        then have "KT" unfolding IsClosed_def by auto
        moreover have "TT" using mem_not_refl by auto
        ultimately have "({T}(T-K))K=0" by auto
        then have "({T}(T-K))int(K)=0" using Top_2_L1 by auto moreover
        from A have "{T}(T-K)({one-point compactification of}T)" unfolding OPCompactification_def
          IsClosed_def by auto moreover
        have "int(K)({one-point compactification of}T)" using Top_2_L2 unfolding OPCompactification_def
          by auto ultimately
        have "int(K)({one-point compactification of}T){T}(T-K)({one-point compactification of}T)({T}(T-K))int(K)=0"
          by auto
      }
      ultimately have "({T}  (T - Ky)({one-point compactification of}T)int(Ky)({one-point compactification of}T)x  {T}  (T - Ky)  y  int(Ky)  ({T}(T-Ky))int(Ky)=0) 
        ({T}  (T - Kx)({one-point compactification of}T)int(Kx)({one-point compactification of}T)y  {T}  (T - Kx)  x  int(Kx)  ({T}(T-Kx))int(Kx)=0)" by auto
      moreover
      {
        assume "({T}  (T - Ky)({one-point compactification of}T)int(Ky)({one-point compactification of}T)x  {T}  (T - Ky)  y  int(Ky)  ({T}(T-Ky))int(Ky)=0)"
        then have "U({one-point compactification of}T). V({one-point compactification of}T). xUyVUV=0" using exI[OF exI[of _ "int(Ky)"],of "λU V. U({one-point compactification of}T)V({one-point compactification of}T)  xUyVUV=0" "{T}(T-Ky)"]
          by auto          
      } moreover
      {
        assume "({T}  (T - Kx)({one-point compactification of}T)int(Kx)({one-point compactification of}T)y  {T}  (T - Kx)  x  int(Kx)  ({T}(T-Kx))int(Kx)=0)"
        then have "U({one-point compactification of}T). V({one-point compactification of}T). xUyVUV=0" using exI[OF exI[of _ "{T}(T-Kx)"],of "λU V. U({one-point compactification of}T)V({one-point compactification of}T)  xUyVUV=0""int(Kx)" ]
          by blast
      }
      ultimately have "U({one-point compactification of}T). V({one-point compactification of}T). xUyVUV=0" by auto
    }
    ultimately have "U({one-point compactification of}T). V({one-point compactification of}T). xUyVUV=0" by auto
  }
  then show ?thesis unfolding isT2_def by auto
qed

text‹In conclusion, every locally compact Hausdorff topological space is regular; since this property is hereditary.›

corollary (in topology0) locally_compact_T2_imp_regular:
  assumes "T{is locally-compact}" "T{is T2}"
  shows "T{is regular}"
proof-
  from assms have "( {one-point compactification of}T) {is T2}" using op_compact_T2_3 by auto
  then have "({one-point compactification of}T) {is T4}" unfolding isT4_def using T2_is_T1 topology0.T2_compact_is_normal
    op_comp_is_top unfolding topology0_def using op_compact_total compact_op by auto
  then have "({one-point compactification of}T) {is T3}" using topology0.T4_is_T3 op_comp_is_top unfolding topology0_def
    by auto
  then have "({one-point compactification of}T) {is regular}" using isT3_def by auto moreover
  have "T({one-point compactification of}T)" using op_compact_total by auto
  ultimately have "(({one-point compactification of}T){restricted to}T) {is regular}" using regular_here by auto
  then show "T{is regular}" using open_subspace(2) by auto
qed

text‹This last corollary has an explanation: In Hausdorff spaces, compact sets are closed
and regular spaces are exactly the "locally closed spaces"(those which have a neighbourhood basis of closed sets).
So the neighbourhood basis of compact sets also works as the neighbourhood basis of closed sets we needed to find.›

definition
  IsLocallyClosed ("_{is locally-closed}")
  where "T{is locally-closed}  T{is locally}(λB TT. B{is closed in}TT)"

lemma (in topology0) regular_locally_closed:
  shows "T{is regular}  (T{is locally-closed})"
proof
  assume "T{is regular}"
  then have a:"xT. UT. (xU)  (VT. x  V  cl(V)  U)"  using regular_imp_exist_clos_neig by auto
  {
    fix x b assume "xT""bT""xb"
    with a obtain V where "VT""xV""cl(V)b" by blast
    note cl(V)b moreover
    from VT have "VT" by auto
    then have "Vcl(V)" using cl_contains_set by auto
    with xVVT have "xint(cl(V))" using Top_2_L6 by auto moreover
    from VT have "cl(V){is closed in}T" using cl_is_closed by auto
    ultimately have "xint(cl(V))""cl(V)b""cl(V){is closed in}T" by auto
    then have "KPow(b). xint(K)K{is closed in}T" by auto
  }
  then show "T{is locally-closed}" unfolding IsLocally_def[OF topSpaceAssum] IsLocallyClosed_def
    by auto
next
  assume "T{is locally-closed}"
  then have a:"xT. bT. xb  (KPow(b). xint(K)K{is closed in}T)" unfolding IsLocally_def[OF topSpaceAssum]
    IsLocallyClosed_def by auto
  {
    fix x b assume "xT""bT""xb"
    with a obtain K where K:"Kb""xint(K)""K{is closed in}T" by blast
    have "int(K)K" using Top_2_L1 by auto
    with K(3) have "cl(int(K))K" using Top_3_L13 by auto
    with K(1) have "cl(int(K))b" by auto moreover
    have "int(K)T" using Top_2_L2 by auto moreover
    note xint(K) ultimately have "VT. xV cl(V)b" by auto
  }
  then have "xT. bT. xb  (VT. xV cl(V)b)" by auto
  then show "T{is regular}" using exist_clos_neig_imp_regular by auto
qed

subsection‹Hereditary properties and local properties›

text‹In this section, we prove a relation between a property and its local property
for hereditary properties. Then we apply it to locally-Hausdorff or locally-$T_2$.
We also prove the relation between locally-$T_2$ and
another property that appeared when considering anti-properties, the
anti-hyperconnectness.›

text‹If a property is hereditary in open sets, then local properties are equivalent
to find just one open neighbourhood with that property instead of a whole local basis.›

lemma (in topology0) her_P_is_loc_P:
  assumes "TT. BPow(TT). ATT. TT{is a topology}P(B,TT)  P(BA,TT)"
  shows "(T{is locally}P)  (xT. AT. xAP(A,T))"
proof
  assume A:"T{is locally}P"
  {
    fix x assume x:"xT"
    with A have "bT. xb  (cPow(b). xint(c)P(c,T))" unfolding IsLocally_def[OF topSpaceAssum]
      by auto moreover
    note x moreover
    have "TT" using topSpaceAssum unfolding IsATopology_def by auto
    ultimately have "cPow(T). xint(c) P(c,T)" by auto
    then obtain c where c:"cT""xint(c)""P(c,T)" by auto
    have P:"int(c)T" using Top_2_L2 by auto moreover
    from c(1,3) topSpaceAssum assms have "AT. P(cA,T)" by auto
    ultimately have "P(cint(c),T)" by auto moreover
    from Top_2_L1[of "c"] have "int(c)c" by auto
    then have "cint(c)=int(c)" by auto
    ultimately have "P(int(c),T)" by auto
    with P c(2) have "VT. xVP(V,T)" by auto
  }
  then show "xT. VT. xVP(V,T)" by auto
  next
  assume A:"xT. AT. x  A  P(A, T)"
  {
    fix x assume x:"xT"
    {
      fix b assume b:"xb""bT"
      from x A obtain A where A_def:"AT""xA""P(A,T)" by auto
      from A_def(1,3) assms topSpaceAssum have "GT. P(AG,T)" by auto
      with b(2) have "P(Ab,T)" by auto
      moreover from b(1) A_def(2) have "xAb" by auto moreover
      have "AbT" using b(2) A_def(1) topSpaceAssum IsATopology_def by auto
      then have "int(Ab)=Ab" using Top_2_L3 by auto
      ultimately have "xint(Ab)P(Ab,T)" by auto
      then have "cPow(b). xint(c)P(c,T)" by auto
    }
    then have "bT. xb(cPow(b). xint(c)P(c,T))" by auto
  }
  then show "T{is locally}P" unfolding IsLocally_def[OF topSpaceAssum] by auto
qed


definition
  IsLocallyT2 ("_{is locally-T2}" 70)
  where "T{is locally-T2}T{is locally}(λB. λT. (T{restricted to}B){is T2})"

text‹Since $T_2$ is an hereditary property, we can apply the previous lemma.›

corollary (in topology0) loc_T2:
  shows "(T{is locally-T2})  (xT. AT. xA(T{restricted to}A){is T2})"
proof-
  {
    fix TT B A assume TT:"TT{is a topology}" "(TT{restricted to}B){is T2}" "ATT""BPow(TT)"
    then have s:"BAB""BTT" by auto
    then have "(TT{restricted to}(BA))=(TT{restricted to}B){restricted to}(BA)" using subspace_of_subspace
      by auto moreover
    have "(TT{restricted to}B)=B" unfolding RestrictedTo_def using s(2) by auto
    then have "BA(TT{restricted to}B)" using s(1) by auto moreover
    note TT(2) ultimately have "(TT{restricted to}(BA)){is T2}" using T2_here
      by auto
  }
  then have "TT. BPow(TT). ATT. TT{is a topology}(TT{restricted to}B){is T2}  (TT{restricted to}(BA)){is T2}"
    by auto
  with her_P_is_loc_P[where P="λA. λTT. (TT{restricted to}A){is T2}"] show ?thesis unfolding IsLocallyT2_def by auto
qed


text‹First, we prove that a locally-$T_2$ space is anti-hyperconnected.›

text‹Before starting, let's prove that an open subspace of an hyperconnected
space is hyperconnected.›

lemma(in topology0) open_subspace_hyperconn:
  assumes "T{is hyperconnected}" "UT"
  shows "(T{restricted to}U){is hyperconnected}"
proof-
  {
    fix A B assume "A(T{restricted to}U)""B(T{restricted to}U)""AB=0"
    then obtain AU BU where "A=UAU""B=UBU" "AUT""BUT" unfolding RestrictedTo_def by auto
    then have "AT""BT" using topSpaceAssum assms(2) unfolding IsATopology_def by auto
    with AB=0 have "A=0B=0" using assms(1) unfolding IsHConnected_def by auto
  }
  then show ?thesis unfolding IsHConnected_def by auto
qed

lemma(in topology0) locally_T2_is_antiHConn:
  assumes "T{is locally-T2}"
  shows "T{is anti-}IsHConnected"
proof-
  {
    fix A assume A:"APow(T)""(T{restricted to}A){is hyperconnected}"
    {
      fix x assume "xA"
      with A(1) have "xT" by auto moreover
      have "TT" using topSpaceAssum unfolding IsATopology_def by auto ultimately
      have "cPow(T). x  int(c)  (T {restricted to} c) {is T2}" using