Theory Topology_ZF_5
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