Theory Topology_ZF_5

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

    Copyright (C) 2012-2013 Daniel de la Concepcion

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

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

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

section ‹Topology 5›

theory Topology_ZF_5 imports Topology_ZF_properties Topology_ZF_examples_1 Topology_ZF_4
begin

subsection‹Some results for separation axioms›

text‹First we will give a global characterization of $T_1$-spaces; which is interesting
because it involves the cardinal $\mathbb{N}$.›

lemma (in topology0)  T1_cocardinal_coarser:
  shows "(T {is T⇩1}) ⟷ (CoFinite (⋃T))⊆T"
proof
  {
    assume AS:"T {is T⇩1}"
    {
      fix x assume p:"x∈⋃T"
      {
        fix y assume "y∈(⋃T)-{x}"
        with AS p obtain U where "U∈T" "y∈U" "x∉U" using isT1_def by blast
        then have "U∈T" "y∈U" "U⊆(⋃T)-{x}" by auto
        then have "∃U∈T. y∈U ∧ U⊆(⋃T)-{x}" by auto
      }
      then have "∀y∈(⋃T)-{x}. ∃U∈T. y∈U ∧ U⊆(⋃T)-{x}" by auto
      then have "⋃T-{x}∈T" using open_neigh_open by auto
      with p have "{x} {is closed in}T" using IsClosed_def by auto
    }
    then have pointCl:"∀x∈⋃T. {x} {is closed in} T" by auto
    {
      fix A
      assume AS2:"A∈FinPow(⋃T)"
      let ?p="{⟨x,{x}⟩. x∈A}"
      have "?p∈A→{{x}. x∈A}" using Pi_def unfolding function_def by auto
      then have "?p:bij(A,{{x}. x∈A})" unfolding bij_def inj_def surj_def using apply_equality
        by auto
      then have "A≈{{x}. x∈A}" unfolding eqpoll_def by auto
      with AS2 have "Finite({{x}. x∈A})" unfolding FinPow_def using eqpoll_imp_Finite_iff by auto
      then have "{{x}. x∈A}∈FinPow({D ∈ Pow(⋃T) . D {is closed in} T})" using AS2 pointCl unfolding FinPow_def
      by (safe, blast+) 
      then have "(⋃{{x}. x∈A}) {is closed in} T" using fin_union_cl_is_cl by auto
      moreover
      have "⋃{{x}. x∈A}=A" by auto
      ultimately have "A {is closed in} T" by simp
    }
    then have reg:"∀A∈FinPow(⋃T). A {is closed in} T" by auto
    {
      fix U
      assume AS2:"U ∈ CoCardinal(⋃T,nat)"
      then have "U∈Pow(⋃T)" "U=0 ∨ ((⋃T)-U)≺nat" using CoCardinal_def by auto
      then have "U∈Pow(⋃T)" "U=0 ∨ Finite(⋃T-U)" using lesspoll_nat_is_Finite by auto
      then have "U∈Pow(⋃T)" "U∈T∨(⋃T-U) {is closed in} T" using empty_open topSpaceAssum
        reg unfolding FinPow_def by auto
      then have "U∈Pow(⋃T)" "U∈T∨(⋃T-(⋃T-U))∈T" using IsClosed_def by auto
      moreover
      then have "(⋃T-(⋃T-U))=U" by blast
      ultimately have "U∈T" by auto
    }
    then show "(CoFinite (⋃T))⊆T" using Cofinite_def by auto
  }
  {
    assume "(CoFinite (⋃T))⊆T"
    then have AS:"CoCardinal(⋃T,nat) ⊆ T" using Cofinite_def by auto
    {
      fix x y
      assume AS2:"x∈⋃T" "y∈⋃T""x≠y"
      have "Finite({y})" by auto
      then obtain n where "{y}≈n" "n∈nat" using Finite_def by auto
      then have "{y}≺nat" using n_lesspoll_nat eq_lesspoll_trans by auto
      then have "{y} {is closed in} CoCardinal(⋃T,nat)" using closed_sets_cocardinal
        AS2(2) by auto
      then have "(⋃T)-{y}∈CoCardinal(⋃T,nat)" using union_cocardinal IsClosed_def by auto
      with AS have "(⋃T)-{y}∈T" by auto
      moreover
      with AS2(1,3) have "x∈((⋃T)-{y}) ∧ y∉((⋃T)-{y})" by auto
      ultimately have "∃V∈T. x∈V∧y∉V" by(safe,auto)
    }
    then show "T {is T⇩1}" using isT1_def by auto
  }
qed

text‹In the previous proof, it is obvious that we don't need to check
if ever cofinite set is open. It is enough to check if every singleton is closed.›

corollary(in topology0) T1_iff_singleton_closed:
  shows "(T {is T⇩1}) ⟷ (∀x∈⋃T. {x}{is closed in}T)"
proof
  assume AS:"T {is T⇩1}"
  {
    fix x assume p:"x∈⋃T"
    {
      fix y assume "y∈(⋃T)-{x}"
      with AS p obtain U where "U∈T" "y∈U" "x∉U" using isT1_def by blast
      then have "U∈T" "y∈U" "U⊆(⋃T)-{x}" by auto
      then have "∃U∈T. y∈U ∧ U⊆(⋃T)-{x}" by auto
    }
    then have "∀y∈(⋃T)-{x}. ∃U∈T. y∈U ∧ U⊆(⋃T)-{x}" by auto
    then have "⋃T-{x}∈T" using open_neigh_open by auto
    with p have "{x} {is closed in}T" using IsClosed_def by auto
  }
  then show pointCl:"∀x∈⋃T. {x} {is closed in} T" by auto
next
  assume pointCl:"∀x∈⋃T. {x} {is closed in} T"
  {
    fix A
    assume AS2:"A∈FinPow(⋃T)"
    let ?p="{⟨x,{x}⟩. x∈A}"
    have "?p∈A→{{x}. x∈A}" using Pi_def unfolding function_def by auto
    then have "?p:bij(A,{{x}. x∈A})" unfolding bij_def inj_def surj_def using apply_equality
      by auto
    then have "A≈{{x}. x∈A}" unfolding eqpoll_def by auto
    with AS2 have "Finite({{x}. x∈A})" unfolding FinPow_def using eqpoll_imp_Finite_iff by auto
    then have "{{x}. x∈A}∈FinPow({D ∈ Pow(⋃T) . D {is closed in} T})" using AS2 pointCl unfolding FinPow_def
    by (safe, blast+) 
    then have "(⋃{{x}. x∈A}) {is closed in} T" using fin_union_cl_is_cl by auto
    moreover
    have "⋃{{x}. x∈A}=A" by auto
    ultimately have "A {is closed in} T" by simp
  }
  then have reg:"∀A∈FinPow(⋃T). A {is closed in} T" by auto
  {
    fix U
    assume AS2:"U∈CoCardinal(⋃T,nat)"
    then have "U∈Pow(⋃T)" "U=0 ∨ ((⋃T)-U)≺nat" using CoCardinal_def by auto
    then have "U∈Pow(⋃T)" "U=0 ∨ Finite(⋃T-U)" using lesspoll_nat_is_Finite by auto
    then have "U∈Pow(⋃T)" "U∈T∨(⋃T-U) {is closed in} T" using empty_open topSpaceAssum
      reg unfolding FinPow_def by auto
    then have "U∈Pow(⋃T)" "U∈T∨(⋃T-(⋃T-U))∈T" using IsClosed_def by auto
    moreover
    then have "(⋃T-(⋃T-U))=U" by blast
    ultimately have "U∈T" by auto
  }
  then have "(CoFinite (⋃T))⊆T" using Cofinite_def by auto
  then show "T {is T⇩1}" using T1_cocardinal_coarser by auto
qed

text‹Secondly, let's show that the ‹CoCardinal X Q›
topologies for different sets $Q$ are all ordered
as the partial order of sets. (The order is linear when considering only cardinals)›

lemma order_cocardinal_top:
  fixes X
  assumes "Q1≲Q2"
  shows "CoCardinal(X,Q1) ⊆ CoCardinal(X,Q2)"
proof
  fix x
  assume "x ∈ CoCardinal(X,Q1)"
  then have "x∈Pow(X)" "x=0∨(X-x)≺Q1" using CoCardinal_def by auto
  with assms have "x∈Pow(X)" "x=0∨(X-x)≺Q2" using lesspoll_trans2 by auto
  then show "x∈CoCardinal(X,Q2)" using CoCardinal_def by auto
qed

corollary cocardinal_is_T1:
  fixes X K
  assumes "InfCard(K)"
  shows "CoCardinal(X,K) {is T⇩1}"
proof-
  have "nat≤K" using InfCard_def assms by auto
  then have "nat⊆K" using le_imp_subset by auto
  then have "nat≲K" "K≠0"using subset_imp_lepoll by auto
  then have "CoCardinal(X,nat) ⊆ CoCardinal(X,K)" "⋃CoCardinal(X,K)=X" using order_cocardinal_top 
    union_cocardinal by auto
  then show ?thesis using topology0.T1_cocardinal_coarser topology0_CoCardinal assms Cofinite_def
    by auto
qed

text‹In $T_2$-spaces, filters and nets have at most one limit point.›

lemma (in topology0) T2_imp_unique_limit_filter:
  assumes "T {is T⇩2}" "𝔉 {is a filter on}⋃T" "𝔉 →⇩F x" "𝔉 →⇩F y"
  shows "x=y"
proof-
  {
    assume "x≠y"
    from assms(3,4) have "x∈⋃T" "y∈⋃T" using FilterConverges_def assms(2)
      by auto
    with ‹x≠y› have "∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0" using assms(1) isT2_def by auto
    then obtain U V where "x∈U" "y∈V" "U∩V=0" "U∈T" "V∈T" by auto
    then have "U∈{A∈Pow(⋃T). x∈Interior(A,T)}" "V∈{A∈Pow(⋃T). y∈Interior(A,T)}" using Top_2_L3 by auto
    then have "U∈𝔉" "V∈𝔉" using FilterConverges_def assms(2) assms(3,4)
      by auto
    then have "U∩V∈𝔉" using IsFilter_def assms(2) by auto
    with ‹U∩V=0› have "0∈𝔉" by auto
    then have "False" using IsFilter_def assms(2) by auto
  }
  then show ?thesis by auto
qed

lemma (in topology0) T2_imp_unique_limit_net:
  assumes "T {is T⇩2}" "N {is a net on}⋃T" "N →⇩N x" "N →⇩N y"
  shows "x=y"
proof-
  have "(Filter N..(⋃T)) {is a filter on} (⋃T)" "(Filter N..(⋃T)) →⇩F x" "(Filter N..(⋃T)) →⇩F y"
    using filter_of_net_is_filter(1) net_conver_filter_of_net_conver assms(2)
    assms(3,4) by auto
  with assms(1) show ?thesis using T2_imp_unique_limit_filter by auto
qed
    
text‹In fact, $T_2$-spaces are characterized by this property. For this proof we build
a filter containing the union of two filters.›

lemma (in topology0) unique_limit_filter_imp_T2:
  assumes "∀x∈⋃T. ∀y∈⋃T. ∀𝔉. ((𝔉 {is a filter on}⋃T) ∧ (𝔉 →⇩F x) ∧ (𝔉 →⇩F y)) ⟶ x=y"
  shows "T {is T⇩2}"
proof-
  {
    fix x y
    assume "x∈⋃T" "y∈⋃T" "x≠y"
    {
      assume "∀U∈T. ∀V∈T. (x∈U ∧ y∈V) ⟶ U∩V≠0"
      let ?Ux="{A∈Pow(⋃T). x∈int(A)}"
      let ?Uy="{A∈Pow(⋃T). y∈int(A)}"
      let ?FF="?Ux ∪ ?Uy ∪ {A∩B. ⟨A,B⟩∈?Ux × ?Uy}"
      have sat:"?FF {satisfies the filter base condition}"
      proof-
        {
          fix A B
          assume "A∈?FF" "B∈?FF"
          {
            assume "A∈?Ux" 
            {
              assume "B∈?Ux"
              with ‹x∈⋃T› ‹A∈?Ux› have "A∩B∈?Ux" using neigh_filter(1) IsFilter_def by auto
              then have "A∩B∈?FF" by auto
            }
            moreover
            {
              assume "B∈?Uy"
              with ‹A∈?Ux› have "A∩B∈?FF" by auto
            }
            moreover
            {
              assume "B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}"
              then obtain AA BB where "B=AA∩BB" "AA∈?Ux" "BB∈?Uy" by auto
              with ‹x∈⋃T› ‹A∈?Ux› have "A∩B=(A∩AA)∩BB" "A∩AA∈?Ux" using neigh_filter(1) IsFilter_def by auto
              with ‹BB∈?Uy› have "A∩B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}" by auto
              then have "A∩B∈?FF" by auto
            }
            ultimately have "A∩B∈?FF" using ‹B∈?FF› by auto
          }
          moreover
          {
            assume "A∈?Uy" 
            {
              assume "B∈?Uy"
              with ‹y∈⋃T› ‹A∈?Uy› have "A∩B∈?Uy" using neigh_filter(1) IsFilter_def by auto
              then have "A∩B∈?FF" by auto
            }
            moreover
            {
              assume "B∈?Ux"
              with ‹A∈?Uy› have "B∩A∈?FF" by auto
              moreover have "A∩B=B∩A" by auto
              ultimately have "A∩B∈?FF" by auto
            }
            moreover
            {
              assume "B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}"
              then obtain AA BB where "B=AA∩BB" "AA∈?Ux" "BB∈?Uy" by auto
              with ‹y∈⋃T› ‹A∈?Uy› have "A∩B=AA∩(A∩BB)" "A∩BB∈?Uy" using neigh_filter(1) IsFilter_def by auto
              with ‹AA∈?Ux› have "A∩B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}" by auto
              then have "A∩B∈?FF" by auto
            }
            ultimately have "A∩B∈?FF" using ‹B∈?FF› by auto
          }
          moreover
          {
            assume "A∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}"
            then obtain AA BB where "A=AA∩BB" "AA∈?Ux" "BB∈?Uy" by auto
            {
              assume "B∈?Uy"
              with ‹BB∈?Uy› ‹y∈⋃T› have "B∩BB∈?Uy" using neigh_filter(1) IsFilter_def by auto
              moreover from ‹A=AA∩BB› have "A∩B=AA∩(B∩BB)" by auto
              ultimately have "A∩B∈?FF" using ‹AA∈?Ux› ‹B∩BB∈?Uy› by auto
            }
            moreover
            {
              assume "B∈?Ux"
              with ‹AA∈?Ux› ‹x∈⋃T› have "B∩AA∈?Ux" using neigh_filter(1) IsFilter_def by auto
              moreover from ‹A=AA∩BB› have "A∩B=(B∩AA)∩BB" by auto
              ultimately have "A∩B∈?FF" using ‹B∩AA∈?Ux› ‹BB∈?Uy› by auto
            }
            moreover
            {
              assume "B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}"
              then obtain AA2 BB2 where "B=AA2∩BB2" "AA2∈?Ux" "BB2∈?Uy" by auto
              from ‹B=AA2∩BB2› ‹A=AA∩BB› have "A∩B=(AA∩AA2)∩(BB∩BB2)" by auto
              moreover
              from ‹AA∈?Ux›‹AA2∈?Ux›‹x∈⋃T› have "AA∩AA2∈?Ux" using neigh_filter(1) IsFilter_def by auto
              moreover
              from ‹BB∈?Uy›‹BB2∈?Uy›‹y∈⋃T› have "BB∩BB2∈?Uy" using neigh_filter(1) IsFilter_def by auto
              ultimately have "A∩B∈?FF" by auto
            }
            ultimately have "A∩B∈?FF" using ‹B∈?FF› by auto
          }
          ultimately have "A∩B∈?FF" using ‹A∈?FF› by auto
          then have "∃D∈?FF. D⊆A∩B" unfolding Bex_def by auto
        }
        then have "∀A∈?FF. ∀B∈?FF. ∃D∈?FF. D⊆A∩B" by force
        moreover
        have "⋃T∈?Ux" using ‹x∈⋃T› neigh_filter(1) IsFilter_def by auto
        then have "?FF≠0" by auto
        moreover
        {
          assume "0∈?FF"
          moreover
          have "0∉?Ux" using ‹x∈⋃T› neigh_filter(1) IsFilter_def by auto
          moreover
          have "0∉?Uy" using ‹y∈⋃T› neigh_filter(1) IsFilter_def by auto
          ultimately have "0∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}" by auto
          then obtain A B where "0=A∩B" "A∈?Ux""B∈?Uy" by auto
          then have "x∈int(A)""y∈int(B)" by auto
          moreover
          with ‹0=A∩B› have "int(A)∩int(B)=0" using Top_2_L1 by auto
          moreover
          have "int(A)∈T""int(B)∈T" using Top_2_L2 by auto
          ultimately have "False" using ‹∀U∈T. ∀V∈T. x∈U∧y∈V ⟶ U∩V≠0› by auto
        }
        then have "0∉?FF" by auto
        ultimately show ?thesis using SatisfiesFilterBase_def by auto
      qed
      moreover
      have "?FF⊆Pow(⋃T)" by auto
      ultimately have bas:"?FF {is a base filter} {A∈Pow(⋃T). ∃D∈?FF. D⊆A}" "⋃{A∈Pow(⋃T). ∃D∈?FF. D⊆A}=⋃T" 
        using base_unique_filter_set2[of "?FF"] by auto
      then have fil:"{A∈Pow(⋃T). ∃D∈?FF. D⊆A} {is a filter on} ⋃T" using basic_filter sat by auto
      have "∀U∈Pow(⋃T). x∈int(U) ⟶ (∃D∈?FF. D⊆U)" by auto
      then have "{A∈Pow(⋃T). ∃D∈?FF. D⊆A} →⇩F x" using convergence_filter_base2[OF fil bas(1) _ ‹x∈⋃T›] by auto
      moreover
      then have "∀U∈Pow(⋃T). y∈int(U) ⟶ (∃D∈?FF. D⊆U)" by auto
      then have "{A∈Pow(⋃T). ∃D∈?FF. D⊆A} →⇩F y" using convergence_filter_base2[OF fil bas(1) _ ‹y∈⋃T›] by auto
      ultimately have "x=y" using assms fil ‹x∈⋃T›‹y∈⋃T› by blast
      with ‹x≠y› have "False" by auto
    }
    then have "∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0" by blast
  }
  then show ?thesis using isT2_def by auto
qed

lemma (in topology0) unique_limit_net_imp_T2:
  assumes "∀x∈⋃T. ∀y∈⋃T. ∀N. ((N {is a net on}⋃T) ∧ (N →⇩N x) ∧ (N →⇩N y)) ⟶ x=y"
  shows "T {is T⇩2}"
proof-
  {
    fix x y 𝔉
    assume "x∈⋃T" "y∈⋃T""𝔉 {is a filter on}⋃T""𝔉 →⇩F x""𝔉 →⇩F y"
    then have "(Net(𝔉)) {is a net on} ⋃T""(Net 𝔉) →⇩N x""(Net 𝔉) →⇩N y"
      using filter_conver_net_of_filter_conver net_of_filter_is_net by auto
    with  ‹x∈⋃T› ‹y∈⋃T› have "x=y" using assms by blast
  }
  then have "∀x∈⋃T. ∀y∈⋃T. ∀𝔉. ((𝔉 {is a filter on}⋃T) ∧ (𝔉 →⇩F x) ∧ (𝔉 →⇩F y)) ⟶ x=y" by auto
  then show ?thesis using unique_limit_filter_imp_T2 by auto
qed

text‹This results make easy to check if a space is $T_2$.›

text‹The topology
which comes from a filter as in @{thm "top_of_filter"} is not $T_2$ generally.
  We will see in this file later on, that the exceptions are a consequence of the spectrum.›

corollary filter_T2_imp_card1:
  assumes "(𝔉∪{0}) {is T⇩2}" "𝔉 {is a filter on} ⋃𝔉" "x∈⋃𝔉"
  shows "⋃𝔉={x}"
proof-
  {
    fix y assume "y∈⋃𝔉"
    then have "𝔉 →⇩F y {in} (𝔉∪{0})" using lim_filter_top_of_filter assms(2) by auto
    moreover
    have "𝔉 →⇩F x {in} (𝔉∪{0})" using lim_filter_top_of_filter assms(2,3) by auto
    moreover
    have "⋃𝔉=⋃(𝔉∪{0})" by auto
    ultimately
    have "y=x" using topology0.T2_imp_unique_limit_filter[OF topology0_filter[OF assms(2)] assms(1)] assms(2)
      by auto
  }
  then have "⋃𝔉⊆{x}" by auto
  with assms(3) show ?thesis by auto
qed

text‹There are more separation axioms that just $T_0$, $T_1$ or $T_2$›

definition
  isT3 ("_{is T⇩3}" 90)
  where "T{is T⇩3} ≡ (T{is T⇩1}) ∧ (T{is regular})"

definition
  IsNormal ("_{is normal}" 90)
  where "T{is normal} ≡ ∀A. A{is closed in}T ⟶ (∀B. B{is closed in}T ∧ A∩B=0 ⟶
  (∃U∈T. ∃V∈T. A⊆U∧B⊆V∧U∩V=0))"

definition
  isT4 ("_{is T⇩4}" 90)
  where "T{is T⇩4} ≡ (T{is T⇩1}) ∧ (T{is normal})"

lemma (in topology0) T4_is_T3:
  assumes "T{is T⇩4}" shows "T{is T⇩3}"
proof-
  from assms have nor:"T{is normal}" using isT4_def by auto
  from assms have "T{is T⇩1}" using isT4_def by auto
  then have "Cofinite (⋃T)⊆T" using T1_cocardinal_coarser by auto
  {
    fix A
    assume AS:"A{is closed in}T"
    {
      fix x
      assume "x∈⋃T-A"
      have "Finite({x})" by auto
      then obtain n where "{x}≈n" "n∈nat" unfolding Finite_def by auto
      then have "{x}≲n" "n∈nat" using eqpoll_imp_lepoll by auto
      then have "{x}≺nat" using n_lesspoll_nat lesspoll_trans1 by auto
      with ‹x∈⋃T-A› have "{x} {is closed in} (Cofinite (⋃T))" using Cofinite_def 
        closed_sets_cocardinal by auto
      then have "⋃T-{x}∈Cofinite(⋃T)" unfolding IsClosed_def using union_cocardinal Cofinite_def
        by auto
      with ‹Cofinite (⋃T)⊆T› have "⋃T-{x}∈T" by auto
      with ‹x∈⋃T-A› have "{x}{is closed in}T" "A∩{x}=0" using IsClosed_def by auto
      with nor AS have "∃U∈T. ∃V∈T. A⊆U∧{x}⊆V∧U∩V=0" unfolding IsNormal_def by blast
      then have "∃U∈T. ∃V∈T. A⊆U∧ x∈V∧U∩V=0" by auto
    }
    then have "∀x∈⋃T-A. ∃U∈T. ∃V∈T. A⊆U∧ x∈V∧U∩V=0" by auto
  }
  then have "T{is regular}" using IsRegular_def by blast
  with ‹T{is T⇩1}› show ?thesis using isT3_def by auto
qed

lemma (in topology0) T3_is_T2:
  assumes "T{is T⇩3}" shows "T{is T⇩2}"
proof-
  from assms have "T{is regular}" using isT3_def by auto
  from assms have "T{is T⇩1}" using isT3_def by auto
  then have "Cofinite (⋃T)⊆T" using T1_cocardinal_coarser by auto
  {
    fix x y
    assume "x∈⋃T""y∈⋃T""x≠y"
    have "Finite({x})" by auto
    then obtain n where "{x}≈n" "n∈nat" unfolding Finite_def by auto
    then have "{x}≲n" "n∈nat" using eqpoll_imp_lepoll by auto
    then have "{x}≺nat" using n_lesspoll_nat lesspoll_trans1 by auto
    with ‹x∈⋃T› have "{x} {is closed in} (Cofinite (⋃T))" using Cofinite_def 
      closed_sets_cocardinal by auto
    then have "⋃T-{x}∈Cofinite(⋃T)" unfolding IsClosed_def using union_cocardinal Cofinite_def
       by auto
    with ‹Cofinite (⋃T)⊆T› have "⋃T-{x}∈T" by auto
    with ‹x∈⋃T›‹y∈⋃T›‹x≠y› have "{x}{is closed in}T" "y∈⋃T-{x}" using IsClosed_def by auto
    with ‹T{is regular}› have "∃U∈T. ∃V∈T. {x}⊆U∧y∈V∧U∩V=0" unfolding IsRegular_def by force
    then have "∃U∈T. ∃V∈T. x∈U∧y∈V∧U∩V=0" by auto
  }
  then show ?thesis using isT2_def by auto
qed

text‹Regularity can be rewritten in terms of existence of certain neighboorhoods.›

lemma (in topology0) regular_imp_exist_clos_neig:
  assumes "T{is regular}" and "U∈T" and "x∈U"
  shows "∃V∈T. x∈V ∧ cl(V)⊆U"
proof-
  from assms(2) have "(⋃T-U){is closed in}T" using Top_3_L9 by auto moreover
  from assms(2,3) have "x∈⋃T" by auto moreover
  note assms(1,3) ultimately obtain A B where "A∈T" and "B∈T" and "A∩B=0" and "(⋃T-U)⊆A" and "x∈B"
    unfolding IsRegular_def by blast
  from ‹A∩B=0› ‹B∈T› have "B⊆⋃T-A" by auto
  with ‹A∈T› have "cl(B)⊆⋃T-A" using Top_3_L9 Top_3_L13 by auto
  moreover from ‹(⋃T-U)⊆A› assms(3) have "⋃T-A⊆U" by auto
  moreover note ‹x∈B› ‹B∈T›
  ultimately have "B∈T ∧ x∈B ∧ cl(B)⊆U" by auto
  then show ?thesis by auto
qed

lemma (in topology0) exist_clos_neig_imp_regular:
  assumes "∀x∈⋃T. ∀U∈T. x∈U ⟶ (∃V∈T. x∈V∧ cl(V)⊆U)"
  shows "T{is regular}"
proof-
  {
    fix F
    assume "F{is closed in}T" 
    {
      fix x assume "x∈⋃T-F"
      with ‹F{is closed in}T› have "x∈⋃T" "⋃T-F∈T" "F⊆⋃T" unfolding IsClosed_def by auto
      with assms ‹x∈⋃T-F› have "∃V∈T. x∈V ∧ cl(V)⊆⋃T-F" by auto
      then obtain V where "V∈T" "x∈V" "cl(V)⊆⋃T-F" by auto
      from ‹cl(V)⊆⋃T-F› ‹F⊆⋃T› have "F⊆⋃T-cl(V)" by auto
      moreover from ‹V∈T› have "⋃T-(⋃T-V)=V" by auto
      then have "cl(V)=⋃T-int(⋃T-V)" using Top_3_L11(2)[of "⋃T-V"] by auto
      ultimately have "F⊆int(⋃T-V)" by auto moreover
      have "int(⋃T-V)⊆⋃T-V" using Top_2_L1 by auto
      then have "V∩(int(⋃T-V))=0" by auto moreover
      note ‹x∈V›‹V∈T› ultimately
      have "V∈T" "int(⋃T-V)∈T" "F⊆int(⋃T-V) ∧ x∈V ∧ (int(⋃T-V))∩V=0" using Top_2_L2
        by auto
      then have "∃U∈T. ∃V∈T. F⊆U ∧ x∈V ∧ U∩V=0" by auto
    }
    then have "∀x∈⋃T-F. ∃U∈T. ∃V∈T. F⊆U ∧ x∈V ∧ U∩V=0" by auto
  }
  then show ?thesis using IsRegular_def by blast
qed

lemma (in topology0) regular_eq:
  shows "T{is regular} ⟷ (∀x∈⋃T. ∀U∈T. x∈U ⟶ (∃V∈T. x∈V∧ cl(V)⊆U))"
  using regular_imp_exist_clos_neig exist_clos_neig_imp_regular by force

text‹A Hausdorff space separates compact spaces from points.›

theorem (in topology0) T2_compact_point:
  assumes "T{is T⇩2}" "A{is compact in}T" "x∈⋃T" "x∉A"
  shows "∃U∈T. ∃V∈T. A⊆U ∧ x∈V ∧ U∩V=0"
proof-
  {
    assume "A=0"
    then have "A⊆0∧x∈⋃T∧(0∩(⋃T)=0)" using assms(3) by auto 
    then have ?thesis using empty_open topSpaceAssum unfolding IsATopology_def by auto
  }
  moreover
  {
    assume noEmpty:"A≠0"
    let ?U="{⟨U,V⟩∈T×T. x∈U∧U∩V=0}"
    {
      fix y assume "y∈A"
      with ‹x∉A› assms(4) have "x≠y" by auto
      moreover from ‹y∈A› have "x∈⋃T""y∈⋃T" using assms(2,3) unfolding IsCompact_def by auto
      ultimately obtain U V where "U∈T""V∈T""U∩V=0""x∈U""y∈V" using assms(1) unfolding isT2_def by blast
      then have "∃⟨U,V⟩∈?U. y∈V" by auto
    }
    then have "∀y∈A. ∃⟨U,V⟩∈?U. y∈V" by auto
    then have "A⊆⋃{snd(B). B∈?U}" by auto
    moreover have "{snd(B). B∈?U}∈Pow(T)" by auto
    ultimately have "∃N∈FinPow({snd(B). B∈?U}). A⊆⋃N" using assms(2) unfolding IsCompact_def by auto
    then obtain N where ss:"N∈FinPow({snd(B). B∈?U})" "A⊆⋃N" by auto
    with ‹{snd(B). B∈?U}∈Pow(T)› have "A⊆⋃N" "N∈Pow(T)" unfolding FinPow_def by auto
    then have NN:"A⊆⋃N" "⋃N∈T" using topSpaceAssum unfolding IsATopology_def by auto
    from ss have "Finite(N)""N⊆{snd(B). B∈?U}" unfolding FinPow_def by auto
    then obtain n where "n∈nat" "N≈n" unfolding Finite_def by auto
    then have "N≲n" using eqpoll_imp_lepoll by auto
    from noEmpty ‹A⊆⋃N› have NnoEmpty:"N≠0" by auto
    let ?QQ="{⟨n,{fst(B). B∈{A∈?U. snd(A)=n}}⟩. n∈N}"
    have QQPi:"?QQ:N→{{fst(B). B∈{A∈?U. snd(A)=n}}. n∈N}" unfolding Pi_def function_def domain_def by auto
    {
      fix n assume "n∈N"
      with ‹N⊆{snd(B). B∈?U}› obtain B where "n=snd(B)" "B∈?U" by auto
      then have "fst(B)∈{fst(B). B∈{A∈?U. snd(A)=n}}" by auto
      then have "{fst(B). B∈{A∈?U. snd(A)=n}}≠0" by auto moreover
      from ‹n∈N› have "⟨n,{fst(B). B∈{A∈?U. snd(A)=n}}⟩∈?QQ" by auto
      with QQPi have "?QQ`n={fst(B). B∈{A∈?U. snd(A)=n}}" using apply_equality by auto
      ultimately have "?QQ`n≠0" by auto
    }
    then have "∀n∈N. ?QQ`n≠0" by auto
    with ‹n∈nat› ‹N≲n› have "∃f. f∈Pi(N,λt. ?QQ`t) ∧ (∀t∈N. f`t∈?QQ`t)" using finite_choice unfolding AxiomCardinalChoiceGen_def
      by auto
    then obtain f where fPI:"f∈Pi(N,λt. ?QQ`t)" "(∀t∈N. f`t∈?QQ`t)" by auto
    from fPI(1) NnoEmpty have "range(f)≠0" unfolding Pi_def range_def domain_def converse_def by (safe,blast)
    {
      fix t assume "t∈N"
      then have "f`t∈?QQ`t" using fPI(2) by auto
      with ‹t∈N› have "f`t∈⋃(?QQ``N)" "?QQ`t⊆⋃(?QQ``N)" using func_imagedef QQPi by auto
    }
    then have reg:"∀t∈N. f`t∈⋃(?QQ``N)"  "∀t∈N. ?QQ`t⊆⋃(?QQ``N)" by auto
    {
      fix tt assume "tt∈f"
      with fPI(1) have "tt∈Sigma(N, (`)(?QQ))" unfolding Pi_def by auto
      then have "tt∈(⋃xa∈N. ⋃y∈?QQ`xa. {⟨xa,y⟩})" unfolding Sigma_def by auto
      then obtain xa y where "xa∈N" "y∈?QQ`xa" "tt=⟨xa,y⟩" by auto
      with reg(2) have "y∈⋃(?QQ``N)" by blast
      with ‹tt=⟨xa,y⟩› ‹xa∈N› have "tt∈(⋃xa∈N. ⋃y∈⋃(?QQ``N). {⟨xa,y⟩})" by auto
      then have "tt∈N×(⋃(?QQ``N))" unfolding Sigma_def by auto
    }
    then have ffun:"f:N→⋃(?QQ``N)"  using fPI(1) unfolding Pi_def by auto
    then have "f∈surj(N,range(f))" using fun_is_surj by auto
    with ‹N≲n› ‹n∈nat› have "range(f)≲N" using surj_fun_inv_2 nat_into_Ord by auto
    with ‹N≲n› have "range(f)≲n" using lepoll_trans by blast
    with ‹n∈nat› have "Finite(range(f))" using n_lesspoll_nat lesspoll_nat_is_Finite lesspoll_trans1 by auto
    moreover from ffun have rr:"range(f)⊆⋃(?QQ``N)" unfolding Pi_def by auto
    then have "range(f)⊆T" by auto
    ultimately have "range(f)∈FinPow(T)" unfolding FinPow_def by auto
    then have "⋂range(f)∈T" using fin_inter_open_open ‹range(f)≠0› by auto moreover
    {
      fix S assume "S∈range(f)"
      with rr have "S∈⋃(?QQ``N)" by blast
      then have "∃B∈(?QQ``N). S ∈ B" using Union_iff by auto
      then obtain B where "B∈(?QQ``N)" "S∈B" by auto
      then have "∃rr∈N. ⟨rr,B⟩∈?QQ" unfolding image_def by auto
      then have "∃rr∈N. B={fst(B). B∈{A∈?U. snd(A)=rr}}" by auto
      with ‹S∈B› obtain rr where "⟨S,rr⟩∈?U" by auto
      then have "x∈S" by auto
    }
    then have "x∈⋂range(f)" using ‹range(f)≠0› by auto moreover
    {
      fix y assume "y∈(⋃N)∩(⋂range(f))"
      then have reg:"(∀S∈range(f). y∈S)∧(∃t∈N. y∈t)" by auto
      then obtain t where "t∈N" "y∈t" by auto
      then have "⟨t, {fst(B). B∈{A∈?U. snd(A)=t}}⟩∈?QQ" by auto
      then have "f`t∈range(f)" using apply_rangeI ffun by auto
      with reg have yft:"y∈f`t" by auto
      with ‹t∈N› fPI(2) have "f`t∈?QQ`t" by auto
      with ‹t∈N› have "f`t∈{fst(B). B∈{A∈?U. snd(A)=t}}" using apply_equality QQPi by auto
      then have "⟨f`t,t⟩∈?U" by auto
      then have "f`t∩t=0" by auto
      with ‹y∈t› yft have "False" by auto
    }
    then have "(⋃N)∩(⋂range(f))=0" by blast moreover
    note NN
    ultimately have ?thesis by auto
  }
  ultimately show ?thesis by auto
qed

text‹A Hausdorff space separates compact spaces from other compact spaces.›

theorem (in topology0) T2_compact_compact:
  assumes "T{is T⇩2}" "A{is compact in}T" "B{is compact in}T" "A∩B=0"
  shows "∃U∈T. ∃V∈T. A⊆U ∧ B⊆V ∧ U∩V=0"
proof-
 {
    assume "B=0"
    then have "A⊆⋃T∧B⊆0∧((⋃T)∩0=0)" using assms(2) unfolding IsCompact_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 ?thesis by auto
  }
  moreover
  {
    assume noEmpty:"B≠0"
    let ?U="{⟨U,V⟩∈T×T. A⊆U ∧ U∩V=0}"
    {
      fix y assume "y∈B"
      then have "y∈⋃T" using assms(3) unfolding IsCompact_def by auto
      with ‹y∈B› have "∃U∈T. ∃V∈T. A⊆U ∧ y∈V ∧ U∩V=0" using T2_compact_point assms(1,2,4) by auto
      then have "∃⟨U,V⟩∈?U. y∈V" by auto
    }
    then have "∀y∈B. ∃⟨U,V⟩∈?U. y∈V" by auto
    then have "B⊆⋃{snd(B). B∈?U}" by auto
    moreover have "{snd(B). B∈?U}∈Pow(T)" by auto
    ultimately have "∃N∈FinPow({snd(B). B∈?U}). B⊆⋃N" using assms(3) unfolding IsCompact_def by auto
    then obtain N where ss:"N∈FinPow({snd(B). B∈?U})" "B⊆⋃N" by auto
    with ‹{snd(B). B∈?U}∈Pow(T)› have "B⊆⋃N" "N∈Pow(T)" unfolding FinPow_def by auto
    then have NN:"B⊆⋃N" "⋃N∈T" using topSpaceAssum unfolding IsATopology_def by auto
    from ss have "Finite(N)""N⊆{snd(B). B∈?U}" unfolding FinPow_def by auto
    then obtain n where "n∈nat" "N≈n" unfolding Finite_def by auto
    then have "N≲n" using eqpoll_imp_lepoll by auto
    from noEmpty ‹B⊆⋃N› have NnoEmpty:"N≠0" by auto
    let ?QQ="{⟨n,{fst(B). B∈{A∈?U. snd(A)=n}}⟩. n∈N}"
    have QQPi:"?QQ:N→{{fst(B). B∈{A∈?U. snd(A)=n}}. n∈N}" unfolding Pi_def function_def domain_def by auto
    {
      fix n assume "n∈N"
      with ‹N⊆{snd(B). B∈?U}› obtain B where "n=snd(B)" "B∈?U" by auto
      then have "fst(B)∈{fst(B). B∈{A∈?U. snd(A)=n}}" by auto
      then have "{fst(B). B∈{A∈?U. snd(A)=n}}≠0" by auto moreover
      from ‹n∈N› have "⟨n,{fst(B). B∈{A∈?U. snd(A)=n}}⟩∈?QQ" by auto
      with QQPi have "?QQ`n={fst(B). B∈{A∈?U. snd(A)=n}}" using apply_equality by auto
      ultimately have "?QQ`n≠0" by auto
    }
    then have "∀n∈N. ?QQ`n≠0" by auto
    with ‹n∈nat› ‹N≲n› have "∃f. f∈Pi(N,λt. ?QQ`t) ∧ (∀t∈N. f`t∈?QQ`t)" using finite_choice unfolding AxiomCardinalChoiceGen_def
      by auto
    then obtain f where fPI:"f∈Pi(N,λt. ?QQ`t)" "(∀t∈N. f`t∈?QQ`t)" by auto
    from fPI(1) NnoEmpty have "range(f)≠0" unfolding Pi_def range_def domain_def converse_def by (safe,blast)
    {
      fix t assume "t∈N"
      then have "f`t∈?QQ`t" using fPI(2) by auto
      with ‹t∈N› have "f`t∈⋃(?QQ``N)" "?QQ`t⊆⋃(?QQ``N)" using func_imagedef QQPi by auto
    }
    then have reg:"∀t∈N. f`t∈⋃(?QQ``N)"  "∀t∈N. ?QQ`t⊆⋃(?QQ``N)" by auto
    {
      fix tt assume "tt∈f"
      with fPI(1) have "tt∈Sigma(N, (`)(?QQ))" unfolding Pi_def by auto
      then have "tt∈(⋃xa∈N. ⋃y∈?QQ`xa. {⟨xa,y⟩})" unfolding Sigma_def by auto
      then obtain xa y where "xa∈N" "y∈?QQ`xa" "tt=⟨xa,y⟩" by auto
      with reg(2) have "y∈⋃(?QQ``N)" by blast
      with ‹tt=⟨xa,y⟩› ‹xa∈N› have "tt∈(⋃xa∈N. ⋃y∈⋃(?QQ``N). {⟨xa,y⟩})" by auto
      then have "tt∈N×(⋃(?QQ``N))" unfolding Sigma_def by auto
    }
    then have ffun:"f:N→⋃(?QQ``N)"  using fPI(1) unfolding Pi_def by auto
    then have "f∈surj(N,range(f))" using fun_is_surj by auto
    with ‹N≲n› ‹n∈nat› have "range(f)≲N" using surj_fun_inv_2 nat_into_Ord by auto
    with ‹N≲n› have "range(f)≲n" using lepoll_trans by blast
    with ‹n∈nat› have "Finite(range(f))" using n_lesspoll_nat lesspoll_nat_is_Finite lesspoll_trans1 by auto
    moreover from ffun have rr:"range(f)⊆⋃(?QQ``N)" unfolding Pi_def by auto
    then have "range(f)⊆T" by auto
    ultimately have "range(f)∈FinPow(T)" unfolding FinPow_def by auto
    then have "⋂range(f)∈T" using fin_inter_open_open ‹range(f)≠0› by auto moreover
    {
      fix S assume "S∈range(f)"
      with rr have "S∈⋃(?QQ``N)" by blast
      then have "∃B∈(?QQ``N). S ∈ B" using Union_iff by auto
      then obtain B where "B∈(?QQ``N)" "S∈B" by auto
      then have "∃rr∈N. ⟨rr,B⟩∈?QQ" unfolding image_def by auto
      then have "∃rr∈N. B={fst(B). B∈{A∈?U. snd(A)=rr}}" by auto
      with ‹S∈B› obtain rr where "⟨S,rr⟩∈?U" by auto
      then have "A⊆S" by auto
    }
    then have "A⊆⋂range(f)" using ‹range(f)≠0› by auto moreover
    {
      fix y assume "y∈(⋃N)∩(⋂range(f))"
      then have reg:"(∀S∈range(f). y∈S)∧(∃t∈N. y∈t)" by auto
      then obtain t where "t∈N" "y∈t" by auto
      then have "⟨t, {fst(B). B∈{A∈?U. snd(A)=t}}⟩∈?QQ" by auto
      then have "f`t∈range(f)" using apply_rangeI ffun by auto
      with reg have yft:"y∈f`t" by auto
      with ‹t∈N› fPI(2) have "f`t∈?QQ`t" by auto
      with ‹t∈N› have "f`t∈{fst(B). B∈{A∈?U. snd(A)=t}}" using apply_equality QQPi by auto
      then have "⟨f`t,t⟩∈?U" by auto
      then have "f`t∩t=0" by auto
      with ‹y∈t› yft have "False" by auto
    }
    then have "(⋂range(f))∩(⋃N)=0" by blast moreover
    note NN
    ultimately have ?thesis by auto
  }
  ultimately show ?thesis by auto
qed

text‹A compact Hausdorff space is normal.›

corollary (in topology0) T2_compact_is_normal:
  assumes "T{is T⇩2}" "(⋃T){is compact in}T"
  shows "T{is normal}" unfolding IsNormal_def
proof-
  from assms(2) have car_nat:"(⋃T){is compact of cardinal}nat{in}T" using Compact_is_card_nat by auto
  {
    fix A B assume "A{is closed in}T" "B{is closed in}T""A∩B=0"
    then have com:"((⋃T)∩A){is compact of cardinal}nat{in}T" "((⋃T)∩B){is compact of cardinal}nat{in}T" using compact_closed[OF car_nat] 
      by auto
    from ‹A{is closed in}T›‹B{is closed in}T› have "(⋃T)∩A=A""(⋃T)∩B=B" unfolding IsClosed_def by auto
    with com have "A{is compact of cardinal}nat{in}T" "B{is compact of cardinal}nat{in}T" by auto
    then have "A{is compact in}T""B{is compact in}T" using Compact_is_card_nat by auto
    with ‹A∩B=0› have "∃U∈T. ∃V∈T. A⊆U ∧ B⊆V ∧ U∩V=0" using T2_compact_compact assms(1) by auto
  }
  then show " ∀A. A {is closed in} T ⟶ (∀B. B {is closed in} T ∧ A ∩ B = 0 ⟶ (∃U∈T. ∃V∈T. A ⊆ U ∧ B ⊆ V ∧ U ∩ V = 0))"
    by auto
qed

subsection‹Hereditability›

text‹A topological property is hereditary if whenever a space has it, 
every subspace also has it.›

definition IsHer ("_{is hereditary}" 90)
  where "P {is hereditary} ≡ ∀T. T{is a topology} ∧ P(T) ⟶ (∀A∈Pow(⋃T). P(T{restricted to}A))"

lemma subspace_of_subspace:
  assumes "A⊆B""B⊆⋃T"
  shows "T{restricted to}A=(T{restricted to}B){restricted to}A"
proof
  from assms have S:"∀S∈T. A∩(B∩S)=A∩S" by auto
  then show "T {restricted to} A ⊆ T {restricted to} B {restricted to} A" unfolding RestrictedTo_def
    by auto
  from S show "T {restricted to} B {restricted to} A ⊆ T {restricted to} A" unfolding RestrictedTo_def
    by auto
qed
 
text‹The separation properties $T_0$, $T_1$, $T_2$ y $T_3$ are hereditary.›

theorem regular_here:
  assumes "T{is regular}" "A∈Pow(⋃T)" shows "(T{restricted to}A){is regular}"
proof-
  {
    fix C
    assume A:"C{is closed in}(T{restricted to}A)"
    {fix y assume "y∈⋃(T{restricted to}A)""y∉C"
    with A have "(⋃(T{restricted to}A))-C∈(T{restricted to}A)""C⊆⋃(T{restricted to}A)" "y∈⋃(T{restricted to}A)""y∉C" unfolding IsClosed_def
      by auto
    moreover
    with assms(2) have "⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
    ultimately have "A-C∈T{restricted to}A" "y∈A""y∉C""C∈Pow(A)" by auto
    then obtain S where "S∈T" "A∩S=A-C" "y∈A""y∉C" unfolding RestrictedTo_def by auto
    then have "y∈A-C""A∩S=A-C" by auto
    with ‹C∈Pow(A)› have "y∈A∩S""C=A-A∩S" by auto
    then have "y∈S" "C=A-S" by auto
    with assms(2) have "y∈S" "C⊆⋃T-S" by auto
    moreover
    from ‹S∈T› have "⋃T-(⋃T-S)=S" by auto
    moreover
    with ‹S∈T› have "(⋃T-S) {is closed in}T" using IsClosed_def by auto
    ultimately have "y∈⋃T-(⋃T-S)" "(⋃T-S) {is closed in}T" by auto
    with assms(1) have "∀y∈⋃T-(⋃T-S). ∃U∈T. ∃V∈T. (⋃T-S)⊆U∧y∈V∧U∩V=0" unfolding IsRegular_def by auto
    with ‹y∈⋃T-(⋃T-S)› have "∃U∈T. ∃V∈T. (⋃T-S)⊆U∧y∈V∧U∩V=0" by auto
    then obtain U V where "U∈T""V∈T" "⋃T-S⊆U""y∈V""U∩V=0" by auto
    then have "A∩U∈(T{restricted to}A)""A∩V∈(T{restricted to}A)" "C⊆U""y∈V""(A∩U)∩(A∩V)=0"
      unfolding RestrictedTo_def  using ‹C⊆⋃T-S› by auto
    moreover
    with ‹C∈Pow(A)›‹y∈A› have "C⊆A∩U""y∈A∩V" by auto
    ultimately have "∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). C⊆U∧y∈V∧U∩V=0" by auto
  }
    then have "∀x∈⋃(T{restricted to}A)-C. ∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). C⊆U∧x∈V∧U∩V=0" by auto
  }
  then have "∀C. C{is closed in}(T{restricted to}A) ⟶ (∀x∈⋃(T{restricted to}A)-C. ∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). C⊆U∧x∈V∧U∩V=0)"
   by blast
  then show ?thesis using IsRegular_def by auto
qed

corollary here_regular:
  shows "IsRegular {is hereditary}" using regular_here IsHer_def by auto

theorem T1_here:
  assumes "T{is T⇩1}" "A∈Pow(⋃T)" shows "(T{restricted to}A){is T⇩1}"
proof-
  from assms(2) have un:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
  {
    fix x y
    assume "x∈A""y∈A""x≠y"
    with ‹A∈Pow(⋃T)› have "x∈⋃T""y∈⋃T""x≠y" by auto
    then have "∃U∈T. x∈U∧y∉U" using assms(1) isT1_def by auto
    then obtain U where "U∈T""x∈U""y∉U" by auto
    with ‹x∈A› have "A∩U∈(T{restricted to}A)" "x∈A∩U" "y∉A∩U" unfolding RestrictedTo_def by auto
    then have "∃U∈(T{restricted to}A). x∈U∧y∉U" by blast
  }
  with un have "∀x y. x∈⋃(T{restricted to}A) ∧ y∈⋃(T{restricted to}A) ∧ x≠y ⟶ (∃U∈(T{restricted to}A). x∈U∧y∉U)"
    by auto
  then show ?thesis using isT1_def by auto
qed

corollary here_T1:
  shows "isT1 {is hereditary}" using T1_here IsHer_def by auto

lemma here_and:
  assumes "P {is hereditary}" "Q {is hereditary}"
  shows "(λT. P(T) ∧ Q(T)) {is hereditary}" using assms unfolding IsHer_def by auto

corollary here_T3:
  shows "isT3 {is hereditary}" using here_and[OF here_T1 here_regular] unfolding IsHer_def isT3_def.

lemma T2_here:
  assumes "T{is T⇩2}" "A∈Pow(⋃T)" shows "(T{restricted to}A){is T⇩2}"
proof-
  from assms(2) have un:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
  {
    fix x y
    assume "x∈A""y∈A""x≠y"
    with ‹A∈Pow(⋃T)› have "x∈⋃T""y∈⋃T""x≠y" by auto
    then have "∃U∈T. ∃V∈T. x∈U∧y∈V∧U∩V=0" using assms(1) isT2_def by auto
    then obtain U V where "U∈T" "V∈T""x∈U""y∈V""U∩V=0" by auto
    with ‹x∈A›‹y∈A› have "A∩U∈(T{restricted to}A)""A∩V∈(T{restricted to}A)" "x∈A∩U" "y∈A∩V" "(A∩U)∩(A∩V)=0"unfolding RestrictedTo_def by auto
    then have "∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). x∈U∧y∈V∧U∩V=0" unfolding Bex_def by auto
  }
  with un have "∀x y. x∈⋃(T{restricted to}A) ∧ y∈⋃(T{restricted to}A) ∧ x≠y ⟶ (∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). x∈U∧y∈V∧U∩V=0)"
    by auto
  then show ?thesis using isT2_def by auto
qed

corollary here_T2:
  shows "isT2 {is hereditary}" using T2_here IsHer_def by auto

lemma T0_here:
  assumes "T{is T⇩0}" "A∈Pow(⋃T)" shows "(T{restricted to}A){is T⇩0}"
proof-
  from assms(2) have un:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
  {
    fix x y
    assume "x∈A""y∈A""x≠y"
    with ‹A∈Pow(⋃T)› have "x∈⋃T""y∈⋃T""x≠y" by auto
    then have "∃U∈T. (x∈U∧y∉U)∨(y∈U∧x∉U)" using assms(1) isT0_def by auto
    then obtain U where "U∈T" "(x∈U∧y∉U)∨(y∈U∧x∉U)" by auto
    with ‹x∈A›‹y∈A› have "A∩U∈(T{restricted to}A)" "(x∈A∩U∧y∉A∩U)∨(y∈A∩U∧x∉A∩U)" unfolding RestrictedTo_def by auto
    then have "∃U∈(T{restricted to}A). (x∈U∧y∉U)∨(y∈U∧x∉U)" unfolding Bex_def by auto
  }
  with un have "∀x y. x∈⋃(T{restricted to}A) ∧ y∈⋃(T{restricted to}A) ∧ x≠y ⟶ (∃U∈(T{restricted to}A). (x∈U∧y∉U)∨(y∈U∧x∉U))"
    by auto
  then show ?thesis using isT0_def by auto
qed

corollary here_T0:
  shows "isT0 {is hereditary}" using T0_here IsHer_def by auto

subsection‹Spectrum and anti-properties›

text‹The spectrum of a topological property is a class of
sets such that all topologies defined over that set have that property.›

text‹The spectrum of a property gives us the list of sets for which the property doesn't give
any topological information. Being in the spectrum of a topological property is an invariant
in the category of sets and function; mening that equipollent sets are in the same
spectra.›
      
definition Spec ("_ {is in the spectrum of} _" 99)
  where "Spec(K,P) ≡ ∀T. ((T{is a topology} ∧ ⋃T≈K) ⟶ P(T))"

lemma equipollent_spect:
  assumes "A≈B" "B {is in the spectrum of} P"
  shows  "A {is in the spectrum of} P"
proof-
  from assms(2) have "∀T. ((T{is a topology} ∧ ⋃T≈B) ⟶ P(T))" using Spec_def by auto
  then have "∀T. ((T{is a topology} ∧ ⋃T≈A) ⟶ P(T))" using eqpoll_trans[OF _ assms(1)] by auto
  then show ?thesis using Spec_def by auto
qed

theorem eqpoll_iff_spec:
  assumes "A≈B"
  shows "(B {is in the spectrum of} P) ⟷ (A {is in the spectrum of} P)"
proof
  assume "B {is in the spectrum of} P"
  with assms equipollent_spect show "A {is in the spectrum of} P" by auto
next
  assume "A {is in the spectrum of} P"
  moreover
  from assms have "B≈A" using eqpoll_sym by auto
  ultimately show "B {is in the spectrum of} P" using equipollent_spect by auto
qed

text‹From the previous statement, we see that the spectrum could be formed only by
representative of clases of sets. If \emph{AC} holds, this means that the spectrum
can be taken as a set or class of cardinal numbers.›

text‹Here is an example of the spectrum. The proof lies in the indiscrite filter ‹{A}›
that can be build for any set. In this proof, we see that without choice,
there is no way to define the sepctrum of a property with cardinals because if a set is not 
comparable with any ordinal, its cardinal is defined as ‹0› without the set being
empty.›

theorem T4_spectrum:
  shows "(A {is in the spectrum of} isT4) ⟷ A ≲ 1"
proof
  assume "A {is in the spectrum of} isT4"
  then have reg:"∀T. ((T{is a topology} ∧ ⋃T≈A) ⟶ (T {is T⇩4}))" using Spec_def by auto
  {
    assume "A≠0"
    then obtain x where "x∈A" by auto
    then have "x∈⋃{A}" by auto
    moreover
    then have "{A} {is a filter on}⋃{A}" using IsFilter_def by auto
    moreover
    then have "({A}∪{0}) {is a topology} ∧ ⋃({A}∪{0})=A" using top_of_filter by auto
    then have top:"({A}∪{0}) {is a topology}" "⋃({A}∪{0})≈A" using eqpoll_refl by auto
    then have "({A}∪{0}) {is T⇩4}" using reg by auto
    then have "({A}∪{0}) {is T⇩2}" using topology0.T3_is_T2 topology0.T4_is_T3 topology0_def top by auto
    ultimately have "⋃{A}={x}" using filter_T2_imp_card1[of "{A}""x"] by auto
    then have "A={x}" by auto
    then have "A≈1" using singleton_eqpoll_1 by auto
  }
  moreover
  have "A=0 ⟶ A≈0" by auto
  ultimately have "A≈1∨A≈0" by blast
  then show "A≲1" using empty_lepollI eqpoll_imp_lepoll eq_lepoll_trans by auto
next
  assume "A≲1"
  have "A=0∨A≠0" by auto
  then obtain E where "A=0∨E∈A" by auto
  then have "A≈0∨E∈A" by auto
  with ‹A≲1› have "A≈0∨A={E}" using lepoll_1_is_sing by auto
  then have "A≈0∨A≈1" using singleton_eqpoll_1 by auto
  {
    fix T
    assume AS:"T{is a topology}""⋃T≈A"
    {
      assume "A≈0"
      with AS have "T{is a topology}" and empty:"⋃T=0" using eqpoll_trans eqpoll_0_is_0 by auto
      then have "T{is T⇩2}" using isT2_def by auto
      then have "T{is T⇩1}" using T2_is_T1 by auto
      moreover
      from empty have "T⊆{0}" by auto
      with AS(1) have "T={0}" using empty_open by auto
      from empty have rr:"∀A. A{is closed in}T ⟶ A=0" using IsClosed_def by auto
      have "∃U∈T. ∃V∈T. 0⊆U∧0⊆V∧U∩V=0" using empty_open AS(1) by auto
      with rr have "∀A. A{is closed in}T ⟶ (∀B. B{is closed in}T ∧ A∩B=0 ⟶ (∃U∈T. ∃V∈T. A⊆U∧B⊆V∧U∩V=0))"
        by blast
      then have "T{is normal}" using IsNormal_def by auto
      with ‹T{is T⇩1}› have "T{is T⇩4}" using isT4_def by auto
    }
    moreover
    {
      assume "A≈1"
      with AS have "T{is a topology}" and NONempty:"⋃T≈1" using eqpoll_trans[of "⋃T""A""1"] by auto
      then have "⋃T≲1" using eqpoll_imp_lepoll by auto
      moreover
      {
        assume "⋃T=0"
        then have "0≈⋃T" by auto
        with NONempty have "0≈1" using eqpoll_trans by blast
        then have "0=1" using eqpoll_0_is_0 eqpoll_sym by auto
        then have "False" by auto
      }
      then have "⋃T≠0" by auto
      then obtain R where "R∈⋃T" by blast
      ultimately have "⋃T={R}" using lepoll_1_is_sing by auto
      {
        fix x y
        assume "x{is closed in}T""y{is closed in}T" "x∩y=0"
        then have "x⊆⋃T""y⊆⋃T" using IsClosed_def by auto
        then have "x=0∨y=0" using ‹x∩y=0› ‹⋃T={R}› by force
        {
          assume "x=0"
          then have "x⊆0""y⊆⋃T" using ‹y⊆⋃T› by auto
          moreover
          have "0∈T""⋃T∈T" using AS(1) IsATopology_def empty_open by auto
          ultimately have "∃U∈T. ∃V∈T. x⊆U∧y⊆V∧U∩V=0" by auto
        }
        moreover
        {
          assume "x≠0"
          with ‹x=0∨y=0› have "y=0" by auto
          then have "x⊆⋃T""y⊆0" using ‹x⊆⋃T› by auto
          moreover
          have "0∈T""⋃T∈T" using AS(1) IsATopology_def empty_open by auto
          ultimately have "∃U∈T. ∃V∈T. x⊆U∧y⊆V∧U∩V=0" by auto
        }
        ultimately
        have "(∃U∈T. ∃V∈T. x ⊆ U ∧ y ⊆ V ∧ U ∩ V = 0)" by blast
      }
      then have "T{is normal}" using IsNormal_def by auto
      moreover
      {
        fix x y
        assume "x∈⋃T""y∈⋃T""x≠y"
        with ‹⋃T={R}› have "False" by auto
        then have "∃U∈T. x∈U∧y∉U" by auto
      }
      then have "T{is T⇩1}" using isT1_def by auto
      ultimately have "T{is T⇩4}" using isT4_def by auto
    }
    ultimately have "T{is T⇩4}" using ‹A≈0∨A≈1› by auto
  }
  then have "∀T. (T{is a topology} ∧ ⋃T ≈ A) ⟶ (T{is T⇩4})" by auto
  then show "A {is in the spectrum of} isT4" using Spec_def by auto
qed

text‹If the topological properties are related, then so are the spectra.›
    
lemma P_imp_Q_spec_inv:
  assumes "∀T. T{is a topology} ⟶ (Q(T) ⟶ P(T))"  "A {is in the spectrum of} Q"
  shows "A {is in the spectrum of} P"
proof-
  from assms(2) have "∀T. T{is a topology} ∧ ⋃T ≈ A ⟶ Q(T)" using Spec_def by auto
  with assms(1) have "∀T. T{is a topology} ∧ ⋃T ≈ A ⟶ P(T)" by auto
  then show ?thesis using Spec_def by auto
qed

text‹Since we already now the spectrum of $T_4$; if we now the spectrum of $T_0$,
it should be easier to compute the spectrum of $T_1$, $T_2$ and $T_3$.›

theorem T0_spectrum:
  shows "(A {is in the spectrum of} isT0) ⟷ A ≲ 1"
proof
  assume "A {is in the spectrum of} isT0"
  then have reg:"∀T. ((T{is a topology} ∧ ⋃T≈A) ⟶ (T {is T⇩0}))" using Spec_def by auto
  {
    assume "A≠0"
    then obtain x where "x∈A" by auto
    then have "x∈⋃{A}" by auto
    moreover
    then have "{A} {is a filter on}⋃{A}" using IsFilter_def by auto
    moreover
    then have "({A}∪{0}) {is a topology} ∧ ⋃({A}∪{0})=A" using top_of_filter by auto
    then have "({A}∪{0}) {is a topology} ∧ ⋃({A}∪{0})≈A" using eqpoll_refl by auto
    then have "({A}∪{0}) {is T⇩0}" using reg by auto
    {
      fix y
      assume "y∈A""x≠y"
      with ‹({A}∪{0}) {is T⇩0}› obtain U where "U∈({A}∪{0})" and dis:"(x ∈ U ∧ y ∉ U) ∨ (y ∈ U ∧ x ∉ U)" using isT0_def by auto
      then have "U=A" by auto
      with dis ‹y∈A› ‹x∈⋃{A}› have "False" by auto
    }
    then have "∀y∈A. y=x" by auto
    with ‹x∈⋃{A}› have "A={x}" by blast
    then have "A≈1" using