Theory Topology_ZF_properties_3
section ‹Properties in Topology 3›
theory Topology_ZF_properties_3 imports Topology_ZF_7 Finite_ZF_1 Topology_ZF_1b Topology_ZF_9
Topology_ZF_properties_2 FinOrd_ZF
begin
text‹This theory file deals with more topological properties and the
relation with the previous ones in other theory files.›
subsection‹More anti-properties›
text‹In this section we study more anti-properties.›
subsection‹First examples›
text‹A first example of an anti-compact space is the discrete space.›
lemma pow_compact_imp_finite:
assumes "B{is compact in}Pow(A)"
shows "Finite(B)"
proof-
from assms have B:"B⊆A" "∀M∈Pow(Pow(A)). B⊆⋃M ⟶(∃N∈FinPow(M). B⊆⋃N)"
unfolding IsCompact_def by auto
from B(1) have "{{x}. x∈B}∈Pow(Pow(A))" "B⊆⋃{{x}. x∈B}" by auto
with B(2) have "∃N∈FinPow({{x}. x∈B}). B⊆⋃N" by auto
then obtain N where "N∈FinPow({{x}. x∈B})" "B⊆⋃N" by auto
then have "Finite(N)" "N⊆{{x}. x∈B}" "B⊆⋃N" unfolding FinPow_def by auto
then have "Finite(N)" "∀b∈N. Finite(b)" "B⊆⋃N" by auto
then have "B⊆⋃N" "Finite(⋃N)" using Finite_Union[of "N"] by auto
then show "Finite(B)" using subset_Finite by auto
qed
theorem pow_anti_compact:
shows "Pow(A){is anti-compact}"
proof-
{
fix B assume as:"B⊆⋃Pow(A)" "(⋃(Pow(A){restricted to}B)){is compact in}(Pow(A){restricted to}B)"
then have sub:"B⊆A" by auto
then have "Pow(B)=Pow(A){restricted to}B" unfolding RestrictedTo_def by blast
with as(2) have "(⋃Pow(B)){is compact in}Pow(B)" by auto
then have "B{is compact in}Pow(B)" by auto
then have "Finite(B)" using pow_compact_imp_finite by auto
then have "B{is in the spectrum of}(λT. (⋃T){is compact in}T)" using compact_spectrum by auto
}
then show ?thesis unfolding IsAntiComp_def antiProperty_def by auto
qed
text‹In a previous file, @{file "Topology_ZF_5.thy"}, we proved that
the spectrum of the lindelöf property depends on the axiom of countable choice
on subsets of the power set of the natural number.›
text‹In this context, the examples depend on wether this choice principle holds or not.
This is the reason that the examples of anti-lindeloef topologies are left for the next
section.›
subsection‹Structural results›
text‹We first differenciate the spectrum of the lindeloef property depending
on some axiom of choice.›
lemma lindeloef_spec1:
assumes "{the axiom of} nat {choice holds for subsets}(Pow(nat))"
shows "(A {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))) ⟷ (A≲nat)"
using compactK_spectrum[OF assms Card_nat] unfolding IsLindeloef_def.
lemma lindeloef_spec2:
assumes "¬({the axiom of} nat {choice holds for subsets}(Pow(nat)))"
shows "(A {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))) ⟷ Finite(A)"
proof
assume "Finite(A)"
then have A:"A{is in the spectrum of} (λT. ((⋃T){is compact in}T))" using compact_spectrum by auto
have s:"nat≲csucc(nat)" using le_imp_lesspoll[OF Card_csucc[OF Ord_nat]] lt_csucc[OF Ord_nat] le_iff by auto
{
fix T assume "T{is a topology}" "(⋃T){is compact in}T"
then have "(⋃T){is compact of cardinal}nat{in}T" using Compact_is_card_nat by auto
then have "(⋃T){is compact of cardinal}csucc(nat){in}T" using s compact_greater_card Card_csucc[OF Ord_nat] by auto
then have "(⋃T){is lindeloef in}T" unfolding IsLindeloef_def by auto
}
then have "∀T. T{is a topology} ⟶ ((⋃T){is compact in}T) ⟶ ((⋃T){is lindeloef in}T)" by auto
with A show "A {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))" using P_imp_Q_spec_inv[
where Q="λT. ((⋃T){is compact in}T)" and P="λT. ((⋃T){is lindeloef in}T)"] by auto
next
assume A:"A {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))"
then have reg:"∀T. T{is a topology}∧⋃T≈A ⟶ ((⋃T){is compact of cardinal} csucc(nat){in}T)" using Spec_def
unfolding IsLindeloef_def by auto
then have "A{is compact of cardinal} csucc(nat) {in} Pow(A)" using Pow_is_top[of "A"] by auto
then have "∀M∈Pow(Pow(A)). A⊆⋃M ⟶ (∃N∈Pow(M). A⊆⋃N ∧ N≺csucc(nat))" unfolding IsCompactOfCard_def by auto
moreover
have "{{x}. x∈A}∈Pow(Pow(A))" by auto
moreover
have "A=⋃{{x}. x∈A}" by auto
ultimately have "∃N∈Pow({{x}. x∈A}). A⊆⋃N ∧ N≺csucc(nat)" by auto
then obtain N where "N∈Pow({{x}. x∈A})" "A⊆⋃N" "N≺csucc(nat)" by auto
then have "N⊆{{x}. x∈A}" "N≺csucc(nat)" "A⊆⋃N" using FinPow_def by auto
{
fix t
assume "t∈{{x}. x∈A}"
then obtain x where "x∈A""t={x}" by auto
with ‹A⊆⋃N› have "x∈⋃N" by auto
then obtain B where "B∈N""x∈B" by auto
with ‹N⊆{{x}. x∈A}› have "B={x}" by auto
with ‹t={x}›‹B∈N› have "t∈N" by auto
}
with ‹N⊆{{x}. x∈A}› have "N={{x}. x∈A}" by auto
let ?B="{⟨x,{x}⟩. x∈A}"
from ‹N={{x}. x∈A}› have "?B:A→ N" unfolding Pi_def function_def by auto
with ‹N={{x}. x∈A}› have "?B:inj(A,N)" unfolding inj_def using apply_equality by auto
then have "A≲N" using lepoll_def by auto
with ‹N≺csucc(nat)› have "A≺csucc(nat)" using lesspoll_trans1 by auto
then have "A≲nat" using Card_less_csucc_eq_le Card_nat by auto
then have "A≺nat∨A≈nat" using lepoll_iff_leqpoll by auto moreover
{
assume "A≈nat"
then have "nat≈A" using eqpoll_sym by auto
with A have "nat {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))" using equipollent_spect[
where P="(λT. ((⋃T){is lindeloef in}T))"] by auto
moreover
have "Pow(nat){is a topology}" using Pow_is_top by auto
moreover
have "⋃Pow(nat)=nat" by auto
then have "⋃Pow(nat)≈nat" using eqpoll_refl by auto
ultimately
have "nat {is compact of cardinal} csucc(nat){in}Pow(nat)" using Spec_def unfolding IsLindeloef_def by auto
then have "False" using Q_disc_comp_csuccQ_eq_Q_choice_csuccQ[OF InfCard_nat] assms by auto
}
ultimately have "A≺nat" by auto
then show "Finite(A)" using lesspoll_nat_is_Finite by auto
qed
text‹If the axiom of countable choice on subsets of the pow of the natural numbers
doesn't hold, then anti-lindeloef spaces are anti-compact.›
theorem(in topology0) no_choice_imp_anti_lindeloef_is_anti_comp:
assumes "¬({the axiom of} nat {choice holds for subsets}(Pow(nat)) )" "T{is anti-lindeloef}"
shows "T{is anti-compact}"
proof-
have s:"nat≲csucc(nat)" using le_imp_lesspoll[OF Card_csucc[OF Ord_nat]] lt_csucc[OF Ord_nat] le_iff by auto
{
fix T assume "T{is a topology}" "(⋃T){is compact in}T"
then have "(⋃T){is compact of cardinal}nat{in}T" using Compact_is_card_nat by auto
then have "(⋃T){is compact of cardinal}csucc(nat){in}T" using s compact_greater_card Card_csucc[OF Ord_nat] by auto
then have "(⋃T){is lindeloef in}T" unfolding IsLindeloef_def by auto
}
then have "∀T. T{is a topology} ⟶ ((⋃T){is compact in}T) ⟶ ((⋃T){is lindeloef in}T)" by auto
from eq_spect_rev_imp_anti[OF this] lindeloef_spec2[OF assms(1)] compact_spectrum
show ?thesis using assms(2) unfolding IsAntiLin_def IsAntiComp_def by auto
qed
text‹If the axiom of countable choice holds for subsets of the power set of the
natural numbers, then there exists a topological space that is anti-lindeloef
but no anti-compact.›
theorem no_choice_imp_anti_lindeloef_is_anti_comp:
assumes "({the axiom of} nat {choice holds for subsets}(Pow(nat)))"
shows "({one-point compactification of}Pow(nat)){is anti-lindeloef}"
proof-
have t:"⋃({one-point compactification of}Pow(nat))={nat}∪nat" using topology0.op_compact_total
unfolding topology0_def using Pow_is_top by auto
have "{nat}≈1" using singleton_eqpoll_1 by auto
then have "{nat}≺nat" using n_lesspoll_nat eq_lesspoll_trans by auto moreover
have s:"nat≺csucc(nat)" using lt_Card_imp_lesspoll[OF Card_csucc] lt_csucc[OF Ord_nat] by auto
ultimately have "{nat}≺csucc(nat)" using lesspoll_trans by blast
with s have "{nat}∪nat≺csucc(nat)" using less_less_imp_un_less[OF _ _ InfCard_csucc[OF InfCard_nat]]
by auto
then have "{nat}∪nat≲nat" using Card_less_csucc_eq_le[OF Card_nat] by auto
with t have r:"⋃({one-point compactification of}Pow(nat))≲nat" by auto
{
fix A assume A:"A∈Pow(⋃({one-point compactification of}Pow(nat)))" "(⋃(({one-point compactification of}Pow(nat)){restricted to}A)){is lindeloef in}(({one-point compactification of}Pow(nat)){restricted to}A)"
from A(1) have "A⊆⋃({one-point compactification of}Pow(nat))" by auto
with r have "A≲nat" using subset_imp_lepoll lepoll_trans by blast
then have "A{is in the spectrum of}(λT. ((⋃T){is lindeloef in}T))" using assms
lindeloef_spec1 by auto
}
then show ?thesis unfolding IsAntiLin_def antiProperty_def by auto
qed
theorem op_comp_pow_nat_no_anti_comp:
shows "¬(({one-point compactification of}Pow(nat)){is anti-compact})"
proof
let ?T="({one-point compactification of}Pow(nat)){restricted to}({nat} ∪ nat)"
assume antiComp:"({one-point compactification of}Pow(nat)){is anti-compact}"
have "({nat} ∪ nat){is compact in}({one-point compactification of}Pow(nat))"
using topology0.compact_op[of "Pow(nat)"] Pow_is_top[of "nat"] unfolding topology0_def
by auto
then have "({nat} ∪ nat){is compact in}?T" using compact_imp_compact_subspace Compact_is_card_nat by auto
moreover have "⋃?T=(⋃({one-point compactification of}Pow(nat)))∩({nat} ∪ nat)" unfolding RestrictedTo_def by auto
then have "⋃?T={nat} ∪ nat" using topology0.op_compact_total unfolding topology0_def
using Pow_is_top by auto
ultimately have "(⋃?T){is compact in}?T" by auto
with antiComp have "({nat} ∪ nat){is in the spectrum of}(λT. (⋃T){is compact in}T)" unfolding IsAntiComp_def
antiProperty_def using topology0.op_compact_total unfolding topology0_def using Pow_is_top by auto
then have "Finite({nat} ∪ nat)" using compact_spectrum by auto
then have "Finite(nat)" using subset_Finite by auto
then show "False" using nat_not_Finite by auto
qed
text‹In coclusion, we reached another equivalence of this choice principle.›
text‹The axiom of countable choice holds for subsets of the power set of the
natural numbers if and only if there exists a topological space which is anti-lindeloef
but not anti-compact; this space can be chosen as the one-point compactification
of the discrete topology on $\mathbb{N}$.›
theorem acc_pow_nat_equiv1:
shows "({the axiom of} nat {choice holds for subsets}(Pow(nat))) ⟷ (({one-point compactification of}Pow(nat)){is anti-lindeloef})"
using op_comp_pow_nat_no_anti_comp no_choice_imp_anti_lindeloef_is_anti_comp
topology0.no_choice_imp_anti_lindeloef_is_anti_comp topology0.op_comp_is_top
Pow_is_top[of "nat"] unfolding topology0_def by auto
theorem acc_pow_nat_equiv2:
shows "({the axiom of} nat {choice holds for subsets}(Pow(nat))) ⟷ (∃T. T{is a topology}
∧ (T{is anti-lindeloef}) ∧ ¬(T{is anti-compact}))"
using op_comp_pow_nat_no_anti_comp no_choice_imp_anti_lindeloef_is_anti_comp
topology0.no_choice_imp_anti_lindeloef_is_anti_comp topology0.op_comp_is_top
Pow_is_top[of "nat"] unfolding topology0_def by auto
text‹In the file @{file "Topology_ZF_properties.thy"}, it is proven that $\mathbb{N}$ is
lindeloef if and only if the axiom of countable choice holds for subsets of $Pow(\mathbb{N})$.
Now we check that, in ZF, this space is always anti-lindeloef.›
theorem nat_anti_lindeloef:
shows "Pow(nat){is anti-lindeloef}"
proof-
{
fix A assume A:"A∈Pow(⋃Pow(nat))" "(⋃(Pow(nat){restricted to}A)){is lindeloef in}(Pow(nat){restricted to}A)"
from A(1) have "A⊆nat" by auto
then have "Pow(nat){restricted to}A=Pow(A)" unfolding RestrictedTo_def by blast
with A(2) have lin:"A{is lindeloef in}Pow(A)" using subset_imp_lepoll by auto
{
fix T assume T:"T{is a topology}" "⋃T≈A"
then have "A≈⋃T" using eqpoll_sym by auto
then obtain f where f:"f∈bij(A,⋃T)" unfolding eqpoll_def by auto
then have "f∈surj(A,⋃T)" unfolding bij_def by auto
moreover then have "IsContinuous(Pow(A),T,f)" unfolding IsContinuous_def
surj_def using func1_1_L3 by blast
moreover have "two_top_spaces0(Pow(A),T,f)" unfolding two_top_spaces0_def
using f T(1) Pow_is_top unfolding bij_def inj_def by auto
ultimately have "(⋃T){is lindeloef in}T" using two_top_spaces0.cont_image_com
lin unfolding IsLindeloef_def by auto
}
then have "A{is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))" unfolding Spec_def by auto
}
then show ?thesis unfolding IsAntiLin_def antiProperty_def by auto
qed
text‹This result is interesting because depending on the different axioms we add
to ZF, it means two different things:
\begin{itemize}
\item Every subspace of $\mathbb{N}$ is Lindeloef.
\item Only the compact subspaces of $\mathbb{N}$ are Lindeloef.
\end{itemize}
›
text‹Now, we could wonder if the class of compact spaces and the class of lindeloef spaces being equal
is consistent in ZF. Let's find a topological space which is lindeloef and no compact
without assuming any axiom of choice or any negation of one. This will prove
that the class of lindeloef spaces and the class of compact spaces cannot be equal
in any model of ZF.›
theorem lord_nat:
shows "(LOrdTopology nat Le)={LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}"
proof-
{
fix U assume U:"U⊆{LeftRayX(nat,Le,n). n∈nat} ∪{nat}" "U≠0"
{
assume "nat∈U"
with U have "⋃U=nat" unfolding LeftRayX_def by auto
then have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat}∪{0}" by auto
}
moreover
{
assume "nat∉U"
with U have UU:"U⊆{LeftRayX(nat,Le,n). n∈nat}∪{0}" by auto
{
assume A:"∃i. i∈nat∧ ⋃U⊆ LeftRayX(nat,Le,i)"
let ?M="μ i. i∈nat ∧ ⋃U⊆ LeftRayX(nat,Le,i)"
from A have M:"?M∈nat" "⋃U⊆ LeftRayX(nat,Le,?M)" using LeastI[OF _ nat_into_Ord, where P="λi. i∈nat ∧ ⋃U⊆ LeftRayX(nat,Le,i)"]
by auto
{
fix y assume V:"y∈LeftRayX(nat,Le,?M)"
then have y:"y∈nat" unfolding LeftRayX_def by auto
{
assume "∀V∈U. y∉V"
then have "∀m∈{n∈nat. LeftRayX(nat,Le,n)∈U}. y∉LeftRayX(nat,Le,m)" using UU by auto
then have "∀m∈{n∈nat. LeftRayX(nat,Le,n)∈U}. ⟨y,m⟩∉Le∨y=m" unfolding LeftRayX_def using y
by auto
then have RR:"∀m∈{n∈nat. LeftRayX(nat,Le,n)∈U}. ⟨m,y⟩∈Le" using Le_directs_nat(1) y unfolding IsLinOrder_def IsTotal_def by blast
{
fix rr V assume "rr∈⋃U"
then obtain V where V:"V∈U" "rr∈V" by auto
with UU obtain m where m:"V=LeftRayX(nat,Le,m)" "m∈nat" by auto
with V(1) RR have a:"⟨m,y⟩∈Le" by auto
from V(2) m(1) have b:"⟨rr,m⟩∈Le" "rr∈nat-{m}" unfolding LeftRayX_def by auto
from a b(1) have "⟨rr,y⟩∈Le" using Le_directs_nat(1) unfolding IsLinOrder_def
trans_def by blast moreover
{
assume "rr=y"
with a b have "False" using Le_directs_nat(1) unfolding IsLinOrder_def antisym_def by blast
}
ultimately have "rr∈LeftRayX(nat,Le,y)" unfolding LeftRayX_def using b(2) by auto
}
then have "⋃U⊆LeftRayX(nat,Le,y)" by auto
with y M(1) have "⟨?M,y⟩∈Le" using Least_le by auto
with V have "False" unfolding LeftRayX_def using Le_directs_nat(1) unfolding IsLinOrder_def antisym_def by blast
}
then have "y∈⋃U" by auto
}
then have "LeftRayX(nat,Le,?M)⊆⋃U" by auto
with M(2) have "⋃U=LeftRayX(nat,Le,?M)" by auto
with M(1) have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat}" by auto
}
moreover
{
assume "¬(∃i. i ∈ nat ∧ ⋃U ⊆ LeftRayX(nat, Le, i))"
then have A:"∀i. i∈nat ⟶ ¬(⋃U ⊆ LeftRayX(nat, Le, i))" by auto
{
fix i assume i:"i∈nat"
with A have AA:"¬(⋃U ⊆ LeftRayX(nat, Le, i))" by auto
{
assume "i∉⋃U"
then have "∀V∈U. i∉V" by auto
then have "∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. i∉LeftRayX(nat, Le, m)" by auto
with i have "∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. ⟨i,m⟩∉Le∨i=m" unfolding LeftRayX_def by auto
with i have "∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. ¬(i≤m)∨i=m" unfolding Le_def by auto
then have "∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. m<i∨m=i" using not_le_iff_lt[OF nat_into_Ord[OF i]
nat_into_Ord] by auto
then have M:"∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. m≤i" using le_iff nat_into_Ord[OF i] by auto
{
fix s assume "s∈⋃U"
then obtain n where n:"n∈nat" "s∈LeftRayX(nat, Le, n)" "LeftRayX(nat, Le, n)∈U"
using UU by auto
with M have ni:"n≤i" by auto
from n(2) have sn:"s≤n" "s≠n" unfolding LeftRayX_def by auto
then have "s≤i" "s≠i" using le_trans[OF sn(1) ni] le_anti_sym[OF sn(1)] ni by auto
then have "s∈LeftRayX(nat, Le, i)" using i le_in_nat unfolding LeftRayX_def by auto
}
with AA have "False" by auto
}
then have "i∈⋃U" by auto
}
then have "nat⊆⋃U" by auto
then have "⋃U=nat" using UU unfolding LeftRayX_def by auto
then have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}" by auto
}
ultimately have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}" by auto
}
ultimately have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}" by auto
}
moreover
{
fix U assume "U=0"
then have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}" by auto
}
ultimately have "∀U. U⊆{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ⟶ ⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}"
by auto
then have "{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}={⋃U. U∈Pow({LeftRayX(nat,Le,n). n∈nat} ∪{nat})}" by blast
then show ?thesis using LOrdtopology_ROrdtopology_are_topologies(2)[OF Le_directs_nat(1)]
unfolding IsAbaseFor_def by auto
qed
lemma countable_lord_nat:
shows "{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}≺csucc(nat)"
proof-
{
fix e
have "{e}≈1" using singleton_eqpoll_1 by auto
then have "{e}≺nat" using n_lesspoll_nat eq_lesspoll_trans by auto moreover
have s:"nat≺csucc(nat)" using lt_Card_imp_lesspoll[OF Card_csucc] lt_csucc[OF Ord_nat] by auto
ultimately have "{e}≺csucc(nat)" using lesspoll_trans by blast
}
then have "{nat} ∪{0}≺csucc(nat)" using less_less_imp_un_less[OF _ _ InfCard_csucc[OF InfCard_nat], of "{nat}" "{0}"]
by auto moreover
let ?FF="{⟨n,LeftRayX(nat,Le,n)⟩. n∈nat}"
have ff:"?FF:nat→{LeftRayX(nat,Le,n). n∈nat}" unfolding Pi_def domain_def function_def by auto
then have su:"?FF∈surj(nat,{LeftRayX(nat,Le,n). n∈nat})" unfolding surj_def using apply_equality[
OF _ ff] by auto
then have "{LeftRayX(nat,Le,n). n∈nat}≲nat" using surj_fun_inv_2[OF su lepoll_refl[of "nat"]] Ord_nat
by auto
then have "{LeftRayX(nat,Le,n). n∈nat}≺csucc(nat)" using Card_less_csucc_eq_le[OF Card_nat] by auto
ultimately have "{LeftRayX(nat, Le, n) . n ∈ nat} ∪ ({nat} ∪ {0}) ≺ csucc(nat)" using less_less_imp_un_less[OF _ _ InfCard_csucc[OF InfCard_nat]] by auto
moreover have "{LeftRayX(nat, Le, n) . n ∈ nat} ∪ ({nat} ∪ {0})={LeftRayX(nat, Le, n) . n ∈ nat} ∪ {nat} ∪ {0}" by auto
ultimately show ?thesis by auto
qed
corollary lindelof_lord_nat:
shows "nat{is lindeloef in}(LOrdTopology nat Le)"
unfolding IsLindeloef_def using countable_lord_nat lord_nat card_top_comp[OF Card_csucc[OF Ord_nat]]
union_lordtopology_rordtopology(1)[OF Le_directs_nat(1)] by auto
theorem not_comp_lord_nat:
shows "¬(nat{is compact in}(LOrdTopology nat Le))"
proof
assume "nat{is compact in}(LOrdTopology nat Le)"
with lord_nat have "nat{is compact in}({LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0})" by auto
then have "∀M∈Pow({LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}). nat⊆⋃M ⟶ (∃N∈FinPow(M). nat⊆⋃N)"
unfolding IsCompact_def by auto moreover
{
fix n assume n:"n∈nat"
then have "n<succ(n)" by auto
then have "⟨n,succ(n)⟩∈Le" "n≠succ(n)" using n nat_succ_iff by auto
then have "n∈LeftRayX(nat,Le,succ(n))" unfolding LeftRayX_def using n by auto
then have "n∈⋃({LeftRayX(nat,Le,n). n∈nat})" using n nat_succ_iff by auto
}
ultimately have "∃N∈FinPow({LeftRayX(nat,Le,n). n∈nat}). nat⊆⋃N" by blast
then obtain N where "N∈FinPow({LeftRayX(nat,Le,n). n∈nat})" "nat⊆⋃N" by auto
then have N:"N⊆{LeftRayX(nat,Le,n). n∈nat}" "Finite(N)" "nat⊆⋃N" unfolding FinPow_def by auto
let ?F="{⟨n,LeftRayX(nat,Le,n)⟩. n∈{m∈nat. LeftRayX(nat,Le,m)∈N}}"
have ff:"?F:{m∈nat. LeftRayX(nat,Le,m)∈N} → N" unfolding Pi_def function_def by auto
then have "?F∈surj({m∈nat. LeftRayX(nat,Le,m)∈N}, N)" unfolding surj_def using N(1) apply_equality[
OF _ ff] by blast moreover
{
fix x y assume xyF:"x∈{m∈nat. LeftRayX(nat,Le,m)∈N}" "y∈{m∈nat. LeftRayX(nat,Le,m)∈N}" "?F`x=?F`y"
then have "?F`x=LeftRayX(nat,Le,x)" "?F`y=LeftRayX(nat,Le,y)" using apply_equality[
OF _ ff] by auto
with xyF(3) have lxy:"LeftRayX(nat,Le,x)=LeftRayX(nat,Le,y)" by auto
{
fix r assume "r<x"
then have "r≤x" "r≠x" using leI by auto
with xyF(1) have "r∈LeftRayX(nat,Le,x)" unfolding LeftRayX_def using le_in_nat by auto
then have "r∈LeftRayX(nat,Le,y)" using lxy by auto
then have "r≤y" "r≠y" unfolding LeftRayX_def by auto
then have "r<y" using le_iff by auto
}
then have "∀r. r<x ⟶ r<y" by auto
then have r:"¬(y<x)" by auto
{
fix r assume "r<y"
then have "r≤y" "r≠y" using leI by auto
with xyF(2) have "r∈LeftRayX(nat,Le,y)" unfolding LeftRayX_def using le_in_nat by auto
then have "r∈LeftRayX(nat,Le,x)" using lxy by auto
then have "r≤x" "r≠x" unfolding LeftRayX_def by auto
then have "r<x" using le_iff by auto
}
then have "¬(x<y)" by auto
with r have "x=y" using not_lt_iff_le[OF nat_into_Ord nat_into_Ord] xyF(1,2)
le_anti_sym by auto
}
then have "?F∈inj({m∈nat. LeftRayX(nat,Le,m)∈N}, N)" unfolding inj_def using ff by auto
ultimately have "?F∈bij({m∈nat. LeftRayX(nat,Le,m)∈N}, N)" unfolding bij_def by auto
then have "{m∈nat. LeftRayX(nat,Le,m)∈N}≈ N" unfolding eqpoll_def by auto
with N(2) have fin:"Finite({m∈nat. LeftRayX(nat,Le,m)∈N})" using lepoll_Finite eqpoll_imp_lepoll
by auto
from N(3) have "N≠0" by auto
then have nE:"{m∈nat. LeftRayX(nat,Le,m)∈N}≠0" using N(1) by auto
let ?M="Maximum(Le,{m∈nat. LeftRayX(nat,Le,m)∈N})"
have M:"?M∈nat" "LeftRayX(nat,Le,?M)∈N" "∀𝔵∈{m∈nat. LeftRayX(nat,Le,m)∈N}. ⟨𝔵,?M⟩∈Le" using fin linord_max_props(1,3)[OF Le_directs_nat(1) _ nE]
unfolding FinPow_def by auto
{
fix V 𝔵 assume V:"V∈N" "𝔵∈V"
then obtain m where m:"V=LeftRayX(nat,Le,m)" "LeftRayX(nat,Le,m)∈N" "m∈nat" using N(1) by auto
with V(2) have xx:"⟨𝔵,m⟩∈Le" "𝔵≠m" unfolding LeftRayX_def by auto
from m(2,3) have "m∈{m∈nat. LeftRayX(nat,Le,m)∈N}" by auto
then have mM:"⟨m,?M⟩∈Le" using M(3) by auto
with xx(1) have "⟨𝔵,?M⟩∈Le" using le_trans unfolding Le_def by auto
moreover
{
assume "𝔵=?M"
with xx mM have "False" using le_anti_sym by auto
}
ultimately have "𝔵∈LeftRayX(nat,Le,?M)" unfolding LeftRayX_def by auto
}
then have "⋃N⊆LeftRayX(nat,Le,?M)" by auto
with M(2) have "⋃N=LeftRayX(nat,Le,?M)" by auto
with N(3) have "nat⊆LeftRayX(nat,Le,?M)" by auto
moreover from M(1) have "succ(?M)∈nat" using nat_succI by auto
ultimately have "succ(?M)∈LeftRayX(nat,Le,?M)" by auto
then have "⟨succ(?M),?M⟩∈Le" unfolding LeftRayX_def by blast
then show "False" by auto
qed
subsection‹More Separation properties›
text‹In this section we study more separation properties.›
subsection‹Definitions›
text‹We start with a property that has already appeared in
@{file "Topology_ZF_1b.thy"}. A KC-space is a space where
compact sets are closed.›
definition
IsKC ("_ {is KC}") where
"T{is KC} ≡ ∀A∈Pow(⋃T). A{is compact in}T ⟶ A{is closed in}T"
text‹Another type of space is an US-space; those where sequences
have at most one limit.›
definition
IsUS ("_{is US}") where
"T{is US} ≡ ∀N x y. (N:nat→⋃T) ∧ NetConvTop(⟨N,Le⟩,x,T) ∧ NetConvTop(⟨N,Le⟩,y,T) ⟶ y=x"
subsection‹First results›
text‹The proof in @{file "Topology_ZF_1b.thy"} shows that a Hausdorff space
is KC.›
corollary(in topology0) T2_imp_KC:
assumes "T{is T⇩2}"
shows "T{is KC}"
proof-
{
fix A assume "A{is compact in}T"
then have "A{is closed in}T" using in_t2_compact_is_cl assms by auto
}
then show ?thesis unfolding IsKC_def by auto
qed
text‹From the spectrum of compactness, it follows that any KC-space
is $T_1$.›
lemma(in topology0) KC_imp_T1:
assumes "T{is KC}"
shows "T{is T⇩1}"
proof-
{
fix x assume A:"x∈⋃T"
have "Finite({x})" by auto
then have "{x}{is in the spectrum of}(λT. (⋃T){is compact in}T)"
using compact_spectrum by auto moreover
have "(T{restricted to}{x}){is a topology}" using Top_1_L4 by auto
moreover have "⋃(T{restricted to}{x})={x}" using A unfolding RestrictedTo_def by auto
ultimately have com:"{x}{is compact in}(T{restricted to}{x})" unfolding Spec_def
by auto
then have "{x}{is compact in}T" using compact_subspace_imp_compact A by auto
then have "{x}{is closed in}T" using assms unfolding IsKC_def using A by auto
}
then show ?thesis using T1_iff_singleton_closed by auto
qed
text‹Even more, if a space is KC, then it is US. We already know that
for $T_2$ spaces, any net or filter has at most one limit; and that
this property is equivalent with $T_2$. The US property is much weaker
because we don't know what happends with other nets that are not directed by
the order on the natural numbers.›
theorem(in topology0) KC_imp_US:
assumes "T{is KC}"
shows "T{is US}"
proof-
{
fix N x y assume A:"N:nat→⋃T" "⟨N,Le⟩→⇩N x" "⟨N,Le⟩→⇩N y" "x≠y"
have dir:"Le directs nat" using Le_directs_nat by auto moreover
from A(1) have dom:"domain(N)=nat" using func1_1_L1 by auto
moreover note A(1) ultimately have Net:"⟨N,Le⟩{is a net on}⋃T" unfolding IsNet_def
by auto
from A(3) have y:"y∈⋃T" unfolding NetConverges_def[OF Net] by auto
from A(2) have x:"x∈⋃T" unfolding NetConverges_def[OF Net] by auto
from A(2) have o1:"∀U∈Pow(⋃T). x∈int(U) ⟶ (∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)" unfolding NetConverges_def[OF Net]
using dom by auto
{
assume B:"∃n∈nat. ∀m∈nat. ⟨n,m⟩∈Le ⟶ N`m=y"
have "{y}{is closed in}T" using y T1_iff_singleton_closed KC_imp_T1 assms by auto
then have o2:"⋃T-{y}∈T" unfolding IsClosed_def by auto
then have "int(⋃T-{y})=⋃T-{y}" using Top_2_L3 by auto
with A(4) x have o3:"x∈int(⋃T-{y})" by auto
from o2 have "⋃T-{y}∈Pow(⋃T)" by auto
with o1 o3 obtain r where r:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈⋃T-{y}" by auto
from B obtain n where n:"n∈nat" "∀m∈nat. ⟨n,m⟩∈Le ⟶ N`m=y" by auto
from dir r(1) n(1) obtain z where "⟨r,z⟩∈Le""⟨n,z⟩∈Le""z∈nat" unfolding IsDirectedSet_def by auto
with r(2) n(2) have "N`z∈⋃T-{y}" "N`z=y" by auto
then have "False" by auto
}
then have reg:"∀n∈nat. ∃m∈nat. N`m≠y ∧ ⟨n,m⟩∈Le" by auto
let ?NN="{⟨n,N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)⟩. n∈nat}"
{
fix x z assume A1:"⟨x, z⟩ ∈ ?NN"
{
fix y' assume A2:"⟨x,y'⟩∈?NN"
with A1 have "z=y'" by auto
}
then have "∀y'. ⟨x,y'⟩∈?NN ⟶ z=y'" by auto
}
then have "∀x z. ⟨x, z⟩ ∈ ?NN ⟶ (∀y'. ⟨x,y'⟩∈?NN ⟶ z=y')" by auto
moreover
{
fix n assume as:"n∈nat"
with reg obtain m where "N`m≠y ∧ ⟨n,m⟩∈Le" "m∈nat" by auto
then have LI:"N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)≠y" "⟨n,μ i. N`i≠y ∧ ⟨n,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠y ∧ ⟨n,m⟩∈Le" "m"]
nat_into_Ord[of "m"] by auto
then have "(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)∈nat" by auto
then have "N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)∈⋃T" using apply_type[OF A(1)] by auto
with as have "⟨n,N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)⟩∈nat×⋃T" by auto
}
then have "?NN∈Pow(nat×⋃T)" by auto
ultimately have NFun:"?NN:nat→⋃T" unfolding Pi_def function_def domain_def by auto
{
fix n assume as:"n∈nat"
with reg obtain m where "N`m≠y ∧ ⟨n,m⟩∈Le" "m∈nat" by auto
then have LI:"N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)≠y" "⟨n,μ i. N`i≠y ∧ ⟨n,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠y ∧ ⟨n,m⟩∈Le" "m"]
nat_into_Ord[of "m"] by auto
then have "?NN`n≠y" using apply_equality[OF _ NFun] by auto
}
then have noy:"∀n∈nat. ?NN`n≠y" by auto
have dom2:"domain(?NN)=nat" by auto
then have net2:"⟨?NN,Le⟩{is a net on}⋃T" unfolding IsNet_def using NFun dir by auto
{
fix U assume "U∈Pow(⋃T)" "x∈int(U)"
then have "(∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)" using o1 by auto
then obtain r where r_def:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U" by auto
{
fix s assume AA:"⟨r,s⟩∈Le"
with reg obtain m where "N`m≠y" "⟨s,m⟩∈Le" by auto
then have "⟨s,μ i. N`i≠y ∧ ⟨s,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠y ∧ ⟨s,m⟩∈Le" "m"]
nat_into_Ord by auto
with AA have "⟨r,μ i. N`i≠y ∧ ⟨s,i⟩∈Le⟩∈Le" using le_trans by auto
with r_def(2) have "N`(μ i. N`i≠y ∧ ⟨s,i⟩∈Le)∈U" by blast
then have "?NN`s∈U" using apply_equality[OF _ NFun] AA by auto
}
then have "∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" by auto
with r_def(1) have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" by auto
}
then have conv2:"⟨?NN,Le⟩→⇩N x" unfolding NetConverges_def[OF net2] using x dom2 by auto
let ?A="{x}∪?NN``nat"
{
fix M assume Acov:"?A⊆⋃M" "M⊆T"
then have "x∈⋃M" by auto
then obtain U where U:"x∈U" "U∈M" by auto
with Acov(2) have UT:"U∈T" by auto
then have "U=int(U)" using Top_2_L3 by auto
with U(1) have "x∈int(U)" by auto
with conv2 obtain r where rr:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U"
unfolding NetConverges_def[OF net2] using dom2 UT by auto
have NresFun:"restrict(?NN,{n∈nat. ⟨n,r⟩∈Le}):{n∈nat. ⟨n,r⟩∈Le}→⋃T" using restrict_fun
[OF NFun, of "{n∈nat. ⟨n,r⟩∈Le}"] by auto
then have "restrict(?NN,{n∈nat. ⟨n,r⟩∈Le})∈surj({n∈nat. ⟨n,r⟩∈Le},range(restrict(?NN,{n∈nat. ⟨n,r⟩∈Le})))"
using fun_is_surj by auto moreover
have "{n∈nat. ⟨n,r⟩∈Le}⊆nat" by auto
then have "{n∈nat. ⟨n,r⟩∈Le}≲nat" using subset_imp_lepoll by auto
ultimately have "range(restrict(?NN,{n∈nat. ⟨n,r⟩∈Le}))≲{n∈nat. ⟨n,r⟩∈Le}" using surj_fun_inv_2 by auto
moreover
have "{n∈nat. ⟨n,0⟩∈Le}={0}" by auto
then have "Finite({n∈nat. ⟨n,0⟩∈Le})" by auto moreover
{
fix j assume as:"j∈nat" "Finite({n∈nat. ⟨n,j⟩∈Le})"
{
fix t assume "t∈{n∈nat. ⟨n,succ(j)⟩∈Le}"
then have "t∈nat" "⟨t,succ(j)⟩∈Le" by auto
then have "t≤succ(j)" by auto
then have "t⊆succ(j)" using le_imp_subset by auto
then have "t⊆j ∪{j}" using succ_explained by auto
then have "j∈t∨t⊆j" by auto
then have "j∈t∨t≤j" using subset_imp_le ‹t∈nat› ‹j∈nat› nat_into_Ord by auto
then have "j ∪{j}⊆t∨t≤j" using ‹t∈nat› ‹j∈nat› nat_into_Ord unfolding Ord_def
Transset_def by auto
then have "succ(j)⊆t∨t≤j" using succ_explained by auto
with ‹t⊆succ(j)› have "t=succ(j)∨t≤j" by auto
with ‹t∈nat› ‹j∈nat› have "t∈{n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)}" by auto
}
then have "{n∈nat. ⟨n,succ(j)⟩∈Le} ⊆{n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)}" by auto
moreover have "Finite({n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)})" using as(2) Finite_cons
by auto
ultimately have "Finite({n∈nat. ⟨n,succ(j)⟩∈Le})" using subset_Finite by auto
}
then have "∀j∈nat. Finite({n∈nat. ⟨n,j⟩∈Le}) ⟶ Finite({n∈nat. ⟨n,succ(j)⟩∈Le})"
by auto
ultimately have "Finite(range(restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le})))"
using lepoll_Finite[of "range(restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le}))"
"{n ∈ nat . ⟨n, r⟩ ∈ Le}"] ind_on_nat[OF ‹r∈nat›, where P="λt. Finite({n∈nat. ⟨n,t⟩∈Le})"] by auto
then have "Finite((restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le}))``{n ∈ nat . ⟨n, r⟩ ∈ Le})" using range_image_domain[OF NresFun]
by auto
then have "Finite(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})" using restrict_image by auto
then have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is in the spectrum of}(λT. (⋃T){is compact in}T)" using compact_spectrum by auto
moreover have "⋃(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})=⋃T∩?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}"
unfolding RestrictedTo_def by auto moreover
have "⋃T∩?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}=?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}"
using func1_1_L6(2)[OF NFun] by blast
moreover have "(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is a topology}"
using Top_1_L4 by auto
ultimately have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is compact in}(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})"
unfolding Spec_def by force
then have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is compact in}T" using compact_subspace_imp_compact by auto
moreover from Acov(1) have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})⊆⋃M" by auto
moreover note Acov(2) ultimately
obtain 𝔑 where 𝔑:"𝔑∈FinPow(M)" "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})⊆⋃𝔑"
unfolding IsCompact_def by blast
from 𝔑(1) have "𝔑 ∪{U}∈FinPow(M)" using U(2) unfolding FinPow_def by auto moreover
{
fix s assume s:"s∈?A" "s∉U"
with U(1) have "s∈?NN``nat" by auto
then have "s∈{?NN`n. n∈nat}" using func_imagedef[OF NFun] by auto
then obtain n where n:"n∈nat" "s=?NN`n" by auto
{
assume "⟨r,n⟩∈Le"
with rr have "?NN`n∈U" by auto
with n(2) s(2) have "False" by auto
}
then have "⟨r,n⟩∉Le" by auto
with rr(1) n(1) have "¬(r≤n)" by auto
then have "n≤r" using Ord_linear_le[where thesis="⟨n,r⟩∈Le"] nat_into_Ord[OF rr(1)]
nat_into_Ord[OF n(1)] by auto
with rr(1) n(1) have "⟨n,r⟩∈Le" by auto
with n(2) have "s∈{?NN`t. t∈{n∈nat. ⟨n,r⟩∈Le}}" by auto moreover
have "{n∈nat. ⟨n,r⟩∈Le}⊆nat" by auto
ultimately have "s∈?NN``{n∈nat. ⟨n,r⟩∈Le}" using func_imagedef[OF NFun]
by auto
with 𝔑(2) have "s∈⋃𝔑" by auto
}
then have "?A⊆⋃𝔑 ∪ U" by auto
then have "?A⊆⋃(𝔑 ∪ {U})" by auto ultimately
have "∃𝔑∈FinPow(M). ?A⊆⋃𝔑" by auto
}
then have "∀M∈Pow(T). ?A⊆⋃M ⟶ (∃𝔑∈FinPow(M). ?A⊆⋃𝔑)" by auto moreover
have "?A⊆⋃T" using func1_1_L6(2)[OF NFun] x by blast ultimately
have "?A{is compact in}T" unfolding IsCompact_def by auto
with assms have "?A{is closed in}T" unfolding IsKC_def IsCompact_def by auto
then have "⋃T-?A∈T" unfolding IsClosed_def by auto
then have "⋃T-?A=int(⋃T-?A)" using Top_2_L3 by auto moreover
{
assume "y∈?A"
with A(4) have "y∈?NN``nat" by auto
then have "y∈{?NN`n. n∈nat}" using func_imagedef[OF NFun] by auto
then obtain n where "n∈nat""?NN`n=y" by auto
with noy have "False" by auto
}
with y have "y∈⋃T-?A" by force ultimately
have "y∈int(⋃T-?A)" "⋃T-?A∈Pow(⋃T)" by auto moreover
have "(∀U∈Pow(⋃T). y ∈ int(U) ⟶ (∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ U))"
using A(3) dom unfolding NetConverges_def[OF Net] by auto
ultimately have "∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ ⋃T-?A" by blast
then obtain r where r_def:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈⋃T-?A" by auto
{
fix s assume AA:"⟨r,s⟩∈Le"
with reg obtain m where "N`m≠y" "⟨s,m⟩∈Le" by auto
then have "⟨s,μ i. N`i≠y ∧ ⟨s,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠y ∧ ⟨s,m⟩∈Le" "m"]
nat_into_Ord by auto
with AA have "⟨r,μ i. N`i≠y ∧ ⟨s,i⟩∈Le⟩∈Le" using le_trans by auto
with r_def(2) have "N`(μ i. N`i≠y ∧ ⟨s,i⟩∈Le)∈⋃T-?A" by force
then have "?NN`s∈⋃T-?A" using apply_equality[OF _ NFun] AA by auto
moreover have "?NN`s∈{?NN`t. t∈nat}" using AA by auto
then have "?NN`s∈?NN``nat" using func_imagedef[OF NFun] by auto
then have "?NN`s∈?A" by auto
ultimately have "False" by auto
}
moreover have "r⊆succ(r)" using succ_explained by auto
then have "r≤succ(r)" using subset_imp_le nat_into_Ord ‹r∈nat› nat_succI
by auto
then have "⟨r,succ(r)⟩∈Le" using ‹r∈nat› nat_succI by auto
ultimately have "False" by auto
}
then have "∀N x y. (N:nat→⋃T) ∧ (⟨N, Le⟩ →⇩N x {in} T) ∧ (⟨N, Le⟩ →⇩N y {in} T)
⟶ x=y" by auto
then show ?thesis unfolding IsUS_def by auto
qed
text‹US spaces are also $T_1$.›
theorem (in topology0) US_imp_T1:
assumes "T{is US}"
shows "T{is T⇩1}"
proof-
{
fix x assume x:"x∈⋃T"
then have "{x}⊆⋃T" by auto
{
fix y assume y:"y≠x" "y∈cl({x})"
then have r:"∀U∈T. y∈U ⟶ x∈U" using cl_inter_neigh[OF ‹{x}⊆⋃T›] by auto
let ?N="ConstantFunction(nat,x)"
have fun:"?N:nat→⋃T" using x func1_3_L1 by auto
then have dom:"domain(?N)=nat" using func1_1_L1 by auto
with fun have Net:"⟨?N,Le⟩{is a net on}⋃T" using Le_directs_nat unfolding IsNet_def
by auto
{
fix U assume "U∈Pow(⋃T)" "x∈int(U)"
then have "x∈U" using Top_2_L1 by auto
then have "∀n∈nat. ?N`n∈U" using func1_3_L2 by auto
then have "∀n∈nat. ⟨0,n⟩∈Le ⟶?N`n∈U" by auto
then have "∃r∈nat. ∀n∈nat. ⟨r,n⟩∈Le ⟶?N`n∈U" by auto
}
then have "⟨?N,Le⟩ →⇩N x" unfolding NetConverges_def[OF Net] using x dom by auto moreover
{
fix U assume "U∈Pow(⋃T)" "y∈int(U)"
then have "x∈int(U)" using r Top_2_L2 by auto
then have "x∈U" using Top_2_L1 by auto
then have "∀n∈nat. ?N`n∈U" using func1_3_L2 by auto
then have "∀n∈nat. ⟨0,n⟩∈Le ⟶?N`n∈U" by auto
then have "∃r∈nat. ∀n∈nat. ⟨r,n⟩∈Le ⟶?N`n∈U" by auto
}
then have "⟨?N,Le⟩ →⇩N y" unfolding NetConverges_def[OF Net] using y(2) dom
Top_3_L11(1)[OF ‹{x}⊆⋃T›] by auto
ultimately have "x=y" using assms unfolding IsUS_def using fun by auto
with y(1) have "False" by auto
}
then have "cl({x})⊆{x}" by auto
then have "cl({x})={x}" using cl_contains_set[OF ‹{x}⊆⋃T›] by auto
then have "{x}{is closed in}T" using Top_3_L8 x by auto
}
then show ?thesis using T1_iff_singleton_closed by auto
qed
subsection‹Counter-examples›
text‹We need to find counter-examples that prove that this properties
are new ones.›
text‹We know that $T_2\Rightarrow loc.T_2\Rightarrow$ anti-hyperconnected $\Rightarrow T_1$
and $T_2\Rightarrow KC\Rightarrow US\Rightarrow T_1$. The question is: What is the relation
between $KC$ or $US$ and, $loc.T_2$ or anti-hyperconnected?›
text‹In the file @{file "Topology_ZF_properties_2.thy"} we built a topological space
which is locally-$T_2$ but no $T_2$. It happends actually that this space is not even US
given the appropiate topology ‹T›.›
lemma (in topology0) locT2_not_US_1:
assumes "{m}∉T" "{m}{is closed in}T" "∃N∈nat→⋃T. (⟨N,Le⟩→⇩N m) ∧ m∉N``nat"
shows "∃N∈nat→⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). (⟨N,Le⟩→⇩N ⋃T {in} (T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))
∧ (⟨N,Le⟩→⇩N m {in} (T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))"
proof-
from assms(3) obtain N where N:"N:nat→⋃T" "⟨N,Le⟩→⇩N m" "m∉N``nat" by auto
have "⋃T⊆⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using assms(2) union_doublepoint_top
by auto
with N(1) have fun:"N:nat→⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using func1_1_L1B by auto
then have dom:"domain(N)=nat" using func1_1_L1 by auto
with fun have Net:"⟨N,Le⟩{is a net on}⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" unfolding
IsNet_def using Le_directs_nat by auto
from N(1) dom have Net2:"⟨N,Le⟩{is a net on}⋃T" unfolding IsNet_def using Le_directs_nat by auto
from N(2) have R:"∀U∈Pow(⋃T). m∈int(U) ⟶(∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)"
unfolding NetConverges_def[OF Net2] using dom by auto
{
fix U assume U:"U∈Pow(⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))" "m∈Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})"
let ?I="Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})"
have "?I∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" using topology0.Top_2_L2 assms(2) doble_point_top unfolding topology0_def by blast
then have "(⋃T)∩?I∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T" unfolding RestrictedTo_def by blast
then have "(⋃T)∩?I∈T" using open_subspace_double_point(1) assms(2) by auto moreover
then have "int((⋃T)∩?I)=(⋃T)∩?I" using Top_2_L3 by auto
with U(2) assms(2) have "m∈int((⋃T)∩?I)" unfolding IsClosed_def by auto
moreover note R ultimately have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈(⋃T)∩?I" by blast
then have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈?I" by blast
then have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U" using topology0.Top_2_L1[of "T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}""U"] doble_point_top assms(2)
unfolding topology0_def by auto
}
then have "∀U∈Pow(⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})). m∈Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}) ⟶(∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)" by auto
moreover have tt:"topology0(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using doble_point_top[OF assms(2)] unfolding topology0_def.
have "m∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using assms(2) union_doublepoint_top unfolding IsClosed_def by auto ultimately
have con1:"(⟨N,Le⟩→⇩N m {in} (T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))" unfolding topology0.NetConverges_def[OF tt Net]
using dom by auto
{
fix U assume U:"U∈Pow(⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))" "⋃T∈Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})"
let ?I="Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})"
have "?I∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" using topology0.Top_2_L2 assms(2) doble_point_top unfolding topology0_def by blast
with U(2) mem_not_refl have "?I∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
then obtain V W where VW:"?I=(V-{m})∪{⋃T}∪W" "W∈T" "V∈T" "m∈V" by auto
from VW(3,4) have "m∈int(V)" using Top_2_L3 by auto moreover
have "V∈Pow(⋃T)" using VW(3) by auto moreover
note R ultimately
have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈V" by blast moreover
from N(3) have "∀s∈nat. N`s≠m" using func_imagedef[OF N(1)] by auto ultimately
have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈V-{m}" by blast
then have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈?I" using VW(1) by auto
then have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U" using topology0.Top_2_L1 assms(2) doble_point_top unfolding topology0_def by blast
}
then have "∀U∈Pow(⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})). ⋃T∈Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}) ⟶ (∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)" by auto
moreover have "⋃T∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using assms(2) union_doublepoint_top by auto ultimately
have "(⟨N,Le⟩→⇩N ⋃T {in} (T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))" unfolding topology0.NetConverges_def[OF tt Net]
using dom by auto
with con1 fun show ?thesis by auto
qed
corollary (in topology0) locT2_not_US_2:
assumes "{m}∉T" "{m}{is closed in}T" "∃N∈nat→⋃T. (⟨N,Le⟩→⇩N m) ∧ m∉N``nat"
shows "¬((T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){is US})"
proof-
have "m≠⋃T" using assms(2) mem_not_refl unfolding IsClosed_def by auto
then show ?thesis using locT2_not_US_1 assms unfolding IsUS_def by blast
qed
text‹In particular, we also know that a locally-$T_2$ space doesn't need to be KC;
since KC$\Rightarrow$US. Also we know that anti-hyperconnected spaces don't need to be
KC or US, since locally-$T_2\Rightarrow$anti-hyperconnected.›
text‹Let's find a KC space that is not $T_2$, an US space which is not KC
and a $T_1$ space which is not US.›
text‹First, let's prove some lemmas about what relation
is there between this properties under the influence of other ones. This will
help us to find counter-examples.›
text‹Anti-compactness ereases the differences between several properties.›
lemma (in topology0) anticompact_KC_equiv_T1:
assumes "T{is anti-compact}"
shows "T{is KC}⟷T{is T⇩1}"
proof
assume "T{is KC}"
then show "T{is T⇩1}" using KC_imp_T1 by auto
next
assume AS:"T{is T⇩1}"
{
fix A assume A:"A{is compact in}T" "A∈Pow(⋃T)"
then have "A{is compact in}(T{restricted to}A)" "A∈Pow(⋃T)" using compact_imp_compact_subspace
Compact_is_card_nat by auto
moreover then have "⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
ultimately have "(⋃(T{restricted to}A)){is compact in}(T{restricted to}A)" "A∈Pow(⋃T)" by auto
with assms have "Finite(A)" unfolding IsAntiComp_def antiProperty_def using compact_spectrum by auto
then obtain n where "n∈nat" "A≈n" unfolding Finite_def by auto
then have "A≺nat" using eq_lesspoll_trans n_lesspoll_nat by auto moreover
have "⋃T-(⋃T-A)=A" using A(2) by auto
ultimately have "⋃T-(⋃T-A)≺nat" by auto
then have "⋃T-A∈CoFinite ⋃T" unfolding Cofinite_def CoCardinal_def by auto
then have "⋃T-A∈T" using AS T1_cocardinal_coarser by auto
with A(2) have "A{is closed in}T" unfolding IsClosed_def by auto
}
then show "T{is KC}" unfolding IsKC_def by auto
qed
text‹Then if we find an anti-compact and $T_1$ but no $T_2$ space,
there is a counter-example for $KC\Rightarrow T_2$. A counter-example for US doesn't
need to be KC mustn't be anti-compact.›
text‹The cocountable topology on ‹csucc(nat)› is such a topology.›
text‹The cocountable topology on $\mathbb{N}^+$ is hyperconnected.›
lemma cocountable_in_csucc_nat_HConn:
shows "(CoCountable csucc(nat)){is hyperconnected}"
proof-
{
fix U V assume as:"U∈(CoCountable csucc(nat))""V∈(CoCountable csucc(nat))""U∩V=0"
then have "csucc(nat)-U≺csucc(nat)∨U=0""csucc(nat)-V≺csucc(nat)∨V=0"
unfolding Cocountable_def CoCardinal_def by auto
then have "(csucc(nat)-U)∪(csucc(nat)-V)≺csucc(nat)∨U=0∨V=0" using less_less_imp_un_less[
OF _ _ InfCard_csucc[OF InfCard_nat]] by auto moreover
{
assume "(csucc(nat)-U)∪(csucc(nat)-V)≺csucc(nat)" moreover
have "(csucc(nat)-U)∪(csucc(nat)-V)=csucc(nat)-U∩V" by auto
with as(3) have "(csucc(nat)-U)∪(csucc(nat)-V)=csucc(nat)" by auto
ultimately have "csucc(nat)≺csucc(nat)" by auto
then have "False" by auto
}
ultimately have "U=0∨V=0" by auto
}
then show "(CoCountable csucc(nat)){is hyperconnected}" unfolding IsHConnected_def by auto
qed
text‹The cocountable topology on $\mathbb{N}^+$ is not anti-hyperconnected.›
corollary cocountable_in_csucc_nat_notAntiHConn:
shows "¬((CoCountable csucc(nat)){is anti-}IsHConnected)"
proof
assume as:"(CoCountable csucc(nat)){is anti-}IsHConnected"
have "(CoCountable csucc(nat)){is hyperconnected}" using cocountable_in_csucc_nat_HConn by auto moreover
have "csucc(nat)≠0" using Ord_0_lt_csucc[OF Ord_nat] by auto
then have uni:"⋃(CoCountable csucc(nat))=csucc(nat)" using union_cocardinal unfolding Cocountable_def by auto
have "∀A∈(CoCountable csucc(nat)). A⊆⋃(CoCountable csucc(nat))" by fast
with uni have "∀A∈(CoCountable csucc(nat)). A⊆csucc(nat)" by auto
then have "∀A∈(CoCountable csucc(nat)). csucc(nat)∩A=A" by auto
ultimately have "((CoCountable csucc(nat)){restricted to}csucc(nat)){is hyperconnected}"
unfolding RestrictedTo_def by auto
with as have "(csucc(nat)){is in the spectrum of}IsHConnected" unfolding antiProperty_def
using uni by auto
then have "csucc(nat)≲1" using HConn_spectrum by auto
then have "csucc(nat)≺nat" using n_lesspoll_nat lesspoll_trans1 by auto
then show "False" using lt_csucc[OF Ord_nat] lt_Card_imp_lesspoll[OF Card_csucc[OF Ord_nat]]
lesspoll_trans by auto
qed
text‹The cocountable topology on $\mathbb{N}^+$ is not $T_2$.›
theorem cocountable_in_csucc_nat_noT2:
shows "¬(CoCountable csucc(nat)){is T⇩2}"
proof
assume "(CoCountable csucc(nat)){is T⇩2}"
then have antiHC:"(CoCountable csucc(nat))