Theory Topology_ZF_properties_2
section ‹Properties in topology 2›
theory Topology_ZF_properties_2 imports Topology_ZF_7 Topology_ZF_1b
Finite_ZF_1 Topology_ZF_11
begin
subsection‹Local properties.›
text‹This theory file deals with local topological properties; and applies local compactness
to the one point compactification.›
text‹We will say that a topological space is locally @term{"P"} iff every point has a neighbourhood basis
of subsets that have the property @term{"P"} as subspaces.›
definition
IsLocally ("_{is locally}_" 90)
where "T{is a topology} ⟹ T{is locally}P ≡ (∀x∈⋃T. ∀b∈T. x∈b ⟶ (∃c∈Pow(b). x∈Interior(c,T) ∧ P(c,T)))"
subsection‹First examples›
text‹Our first examples deal with the locally finite property. Finiteness is a property of sets,
and hence it is preserved by homeomorphisms; which are in particular bijective.›
text‹The discrete topology is locally finite.›
lemma discrete_locally_finite:
shows "Pow(A){is locally}(λA.(λB. Finite(A)))"
proof-
have "∀b∈Pow(A). ⋃(Pow(A){restricted to}b)=b" unfolding RestrictedTo_def by blast
then have "∀b∈{{x}. x∈A}. Finite(b)" by auto moreover
have reg:"∀S∈Pow(A). Interior(S,Pow(A))=S" unfolding Interior_def by auto
{
fix x b assume "x∈⋃Pow(A)" "b∈Pow(A)" "x∈b"
then have "{x}⊆b" "x∈Interior({x},Pow(A))" "Finite({x})" using reg by auto
then have "∃c∈Pow(b). x∈Interior(c,Pow(A))∧Finite(c)" by blast
}
then have "∀x∈⋃Pow(A). ∀b∈Pow(A). x∈b ⟶ (∃c∈Pow(b). x∈Interior(c,Pow(A)) ∧ Finite(c))" by auto
then show ?thesis using IsLocally_def[OF Pow_is_top] by auto
qed
text‹The included set topology is locally finite when the set is finite.›
lemma included_finite_locally_finite:
assumes "Finite(A)" and "A⊆X"
shows "(IncludedSet(X,A)){is locally}(λA.(λB. Finite(A)))"
proof-
have "∀b∈Pow(X). b∩A⊆b" by auto moreover
note assms(1)
ultimately have rr:"∀b∈{A∪{x}. x∈X}. Finite(b)" by force
{
fix x b assume "x∈⋃(IncludedSet(X,A))" "b∈(IncludedSet(X,A))" "x∈b"
then have "A∪{x}⊆b" "A∪{x}∈{A∪{x}. x∈X}" and sub: "b⊆X" unfolding IncludedSet_def by auto
moreover have "A ∪ {x} ⊆ X" using assms(2) sub ‹x∈b› by auto
then have "x∈Interior(A∪{x},IncludedSet(X,A))" using interior_set_includedset[of "A∪{x}""X""A"] by auto
ultimately have "∃c∈Pow(b). x∈Interior(c,IncludedSet(X,A))∧ Finite(c)" using rr by blast
}
then have "∀x∈⋃(IncludedSet(X,A)). ∀b∈(IncludedSet(X,A)). x∈b ⟶ (∃c∈Pow(b). x∈Interior(c,IncludedSet(X,A))∧ Finite(c))" by auto
then show ?thesis using IsLocally_def includedset_is_topology by auto
qed
subsection‹Local compactness›
definition
IsLocallyComp ("_{is locally-compact}" 70)
where "T{is locally-compact}≡T{is locally}(λB. λT. B{is compact in}T)"
text‹We center ourselves in local compactness, because it is a very important tool in topological groups
and compactifications.›
text‹If a subset is compact of some cardinal for a topological space, it is compact of the same cardinal
in the subspace topology.›
lemma compact_imp_compact_subspace:
assumes "A{is compact of cardinal}K{in}T" "A⊆B"
shows "A{is compact of cardinal}K{in}(T{restricted to}B)" unfolding IsCompactOfCard_def
proof
from assms show C:"Card(K)" unfolding IsCompactOfCard_def by auto
from assms have "A⊆⋃T" unfolding IsCompactOfCard_def by auto
then have AA:"A⊆⋃(T{restricted to}B)" using assms(2) unfolding RestrictedTo_def by auto moreover
{
fix M assume "M∈Pow(T{restricted to}B)" "A⊆⋃M"
let ?M="{S∈T. B∩S∈M}"
from ‹M∈Pow(T{restricted to}B)› have "⋃M⊆⋃?M" unfolding RestrictedTo_def by auto
with ‹A⊆⋃M› have "A⊆⋃?M""?M∈Pow(T)" by auto
with assms have "∃N∈Pow(?M). A⊆⋃N∧N≺K" unfolding IsCompactOfCard_def by auto
then obtain N where "N∈Pow(?M)" "A⊆⋃N" "N≺K" by auto
then have "N{restricted to}B⊆M" unfolding RestrictedTo_def FinPow_def by auto
moreover
let ?f="{⟨𝔅,B∩𝔅⟩. 𝔅∈N}"
have "?f:N→(N{restricted to}B)" unfolding Pi_def function_def domain_def RestrictedTo_def by auto
then have "?f∈surj(N,N{restricted to}B)" unfolding surj_def RestrictedTo_def using apply_equality
by auto
from ‹N≺K› have "N≲K" unfolding lesspoll_def by auto
with ‹?f∈surj(N,N{restricted to}B)› have "N{restricted to}B≲N" using surj_fun_inv_2 Card_is_Ord C by auto
with ‹N≺K› have "N{restricted to}B≺K" using lesspoll_trans1 by auto
moreover from ‹A⊆⋃N› have "A⊆⋃(N{restricted to}B)" using assms(2) unfolding RestrictedTo_def by auto
ultimately have "∃N∈Pow(M). A⊆⋃N ∧ N≺K" by auto
}
with AA show "A ⊆ ⋃(T {restricted to} B) ∧ (∀M∈Pow(T {restricted to} B). A ⊆ ⋃M ⟶ (∃N∈Pow(M). A ⊆ ⋃N ∧ N≺K))" by auto
qed
text‹The converse of the previous result is not always true. For compactness, it holds because the axiom of finite choice
always holds.›
lemma compact_subspace_imp_compact:
assumes "A{is compact in}(T{restricted to}B)" "A⊆B"
shows "A{is compact in}T" unfolding IsCompact_def
proof
from assms show "A⊆⋃T" unfolding IsCompact_def RestrictedTo_def by auto
next
{
fix M assume "M∈Pow(T)" "A⊆⋃M"
let ?M="M{restricted to}B"
from ‹M∈Pow(T)› have "?M∈Pow(T{restricted to}B)" unfolding RestrictedTo_def by auto
from ‹A⊆⋃M› have "A⊆⋃?M" unfolding RestrictedTo_def using assms(2) by auto
with assms ‹?M∈Pow(T{restricted to}B)› obtain N where "N∈FinPow(?M)" "A⊆⋃N" unfolding IsCompact_def by blast
from ‹N∈FinPow(?M)› have "N≺nat" unfolding FinPow_def Finite_def using n_lesspoll_nat eq_lesspoll_trans
by auto
then have "Finite(N)" using lesspoll_nat_is_Finite by auto
then obtain n where "n∈nat" "N≈n" unfolding Finite_def by auto
then have "N≲n" using eqpoll_imp_lepoll by auto
moreover
{
fix BB assume "BB∈N"
with ‹N∈FinPow(?M)› have "BB∈?M" unfolding FinPow_def by auto
then obtain S where "S∈M" and "BB=B∩S" unfolding RestrictedTo_def by auto
then have "S∈{S∈M. B∩S=BB}" by auto
then obtain "{S∈M. B∩S=BB}≠0" by auto
}
then have "∀BB∈N. ((λW∈N. {S∈M. B∩S=W})`BB)≠0" by auto moreover
from ‹n∈nat› have " (N ≲ n ∧ (∀t∈N. (λW∈N. {S∈M. B∩S=W}) ` t ≠ 0) ⟶ (∃f. f ∈ Pi(N,λt. (λW∈N. {S∈M. B∩S=W}) ` t) ∧ (∀t∈N. f ` t ∈ (λW∈N. {S∈M. B∩S=W}) ` t)))" using finite_choice unfolding AxiomCardinalChoiceGen_def by blast
ultimately
obtain f where AA:"f∈Pi(N,λt. (λW∈N. {S∈M. B∩S=W}) ` t)" "∀t∈N. f`t∈(λW∈N. {S∈M. B∩S=W}) ` t" by blast
from AA(2) have ss:"∀t∈N. f`t∈{S∈M. B∩S=t}" using beta_if by auto
then have "{f`t. t∈N}⊆M" by auto
{
fix t assume "t∈N"
with ss have "f`t∈{S∈M. B∩S∈N}" by auto
}
with AA(1) have FF:"f:N→{S∈M. B∩S∈N}" unfolding Pi_def Sigma_def using beta_if by auto moreover
{
fix aa bb assume AAA:"aa∈N" "bb∈N" "f`aa=f`bb"
from AAA(1) ss have "B∩ (f`aa) =aa" by auto
with AAA(3) have "B∩(f`bb)=aa" by auto
with ss AAA(2) have "aa=bb" by auto
}
ultimately have "f∈inj(N,{S∈M. B∩S∈N})" unfolding inj_def by auto
then have "f∈bij(N,range(f))" using inj_bij_range by auto
then have "f∈bij(N,f``N)" using range_image_domain FF by auto
then have "f∈bij(N,{f`t. t∈N})" using func_imagedef FF by auto
then have "N≈{f`t. t∈N}" unfolding eqpoll_def by auto
with ‹N≈n› have "{f`t. t∈N}≈n" using eqpoll_sym eqpoll_trans by blast
with ‹n∈nat› have "Finite({f`t. t∈N})" unfolding Finite_def by auto
with ss have "{f`t. t∈N}∈FinPow(M)" unfolding FinPow_def by auto moreover
{
fix aa assume "aa∈A"
with ‹A⊆⋃N› obtain b where "b∈N" and "aa∈b" by auto
with ss have "B∩(f`b)=b" by auto
with ‹aa∈b› have "aa∈B∩(f`b)" by auto
then have "aa∈ f`b" by auto
with ‹b∈N› have "aa∈⋃{f`t. t∈N}" by auto
}
then have "A⊆⋃{f`t. t∈N}" by auto ultimately
have "∃R∈FinPow(M). A⊆⋃R" by auto
}
then show "∀M∈Pow(T). A ⊆ ⋃M ⟶ (∃N∈FinPow(M). A ⊆ ⋃N)" by auto
qed
text‹If the axiom of choice holds for some cardinal,
then we can drop the compact sets of that cardial are compact of the same cardinal
as subspaces of every superspace.›
lemma Kcompact_subspace_imp_Kcompact:
assumes "A{is compact of cardinal}Q{in}(T{restricted to}B)" "A⊆B" "({the axiom of} Q {choice holds})"
shows "A{is compact of cardinal}Q{in}T"
proof -
from assms(1) have a1:"Card(Q)" unfolding IsCompactOfCard_def RestrictedTo_def by auto
from assms(1) have a2:"A⊆⋃T" unfolding IsCompactOfCard_def RestrictedTo_def by auto
{
fix M assume "M∈Pow(T)" "A⊆⋃M"
let ?M="M{restricted to}B"
from ‹M∈Pow(T)› have "?M∈Pow(T{restricted to}B)" unfolding RestrictedTo_def by auto
from ‹A⊆⋃M› have "A⊆⋃?M" unfolding RestrictedTo_def using assms(2) by auto
with assms ‹?M∈Pow(T{restricted to}B)› obtain N where N:"N∈Pow(?M)" "A⊆⋃N" "N ≺ Q" unfolding IsCompactOfCard_def by blast
from N(3) have "N≲Q" using lesspoll_imp_lepoll by auto moreover
{
fix BB assume "BB∈N"
with ‹N∈Pow(?M)› have "BB∈?M" unfolding FinPow_def by auto
then obtain S where "S∈M" and "BB=B∩S" unfolding RestrictedTo_def by auto
then have "S∈{S∈M. B∩S=BB}" by auto
then obtain "{S∈M. B∩S=BB}≠0" by auto
}
then have "∀BB∈N. ((λW∈N. {S∈M. B∩S=W})`BB)≠0" by auto moreover
have " (N ≲ Q ∧ (∀t∈N. (λW∈N. {S∈M. B∩S=W}) ` t ≠ 0) ⟶ (∃f. f ∈ Pi(N,λt. (λW∈N. {S∈M. B∩S=W}) ` t) ∧ (∀t∈N. f ` t ∈ (λW∈N. {S∈M. B∩S=W}) ` t)))"
using assms(3) unfolding AxiomCardinalChoiceGen_def by blast
ultimately
obtain f where AA:"f∈Pi(N,λt. (λW∈N. {S∈M. B∩S=W}) ` t)" "∀t∈N. f`t∈(λW∈N. {S∈M. B∩S=W}) ` t" by blast
from AA(2) have ss:"∀t∈N. f`t∈{S∈M. B∩S=t}" using beta_if by auto
then have "{f`t. t∈N}⊆M" by auto
{
fix t assume "t∈N"
with ss have "f`t∈{S∈M. B∩S∈N}" by auto
}
with AA(1) have FF:"f:N→{S∈M. B∩S∈N}" unfolding Pi_def Sigma_def using beta_if by auto moreover
{
fix aa bb assume AAA:"aa∈N" "bb∈N" "f`aa=f`bb"
from AAA(1) ss have "B∩ (f`aa) =aa" by auto
with AAA(3) have "B∩(f`bb)=aa" by auto
with ss AAA(2) have "aa=bb" by auto
}
ultimately have "f∈inj(N,{S∈M. B∩S∈N})" unfolding inj_def by auto
then have "f∈bij(N,range(f))" using inj_bij_range by auto
then have "f∈bij(N,f``N)" using range_image_domain FF by auto
then have "f∈bij(N,{f`t. t∈N})" using func_imagedef FF by auto
then have "N≈{f`t. t∈N}" unfolding eqpoll_def by auto
with ‹N≺Q› have "{f`t. t∈N}≺Q" using eqpoll_sym eq_lesspoll_trans by blast moreover
with ss have "{f`t. t∈N}∈Pow(M)" unfolding FinPow_def by auto moreover
{
fix aa assume "aa∈A"
with ‹A⊆⋃N› obtain b where "b∈N" and "aa∈b" by auto
with ss have "B∩(f`b)=b" by auto
with ‹aa∈b› have "aa∈B∩(f`b)" by auto
then have "aa∈ f`b" by auto
with ‹b∈N› have "aa∈⋃{f`t. t∈N}" by auto
}
then have "A⊆⋃{f`t. t∈N}" by auto ultimately
have "∃R∈Pow(M). A⊆⋃R ∧ R≺Q" by auto
}
then show ?thesis using a1 a2 unfolding IsCompactOfCard_def by auto
qed
text‹Every set, with the cofinite topology is compact.›
lemma cofinite_compact:
shows "X {is compact in}(CoFinite X)" unfolding IsCompact_def
proof
show "X⊆⋃(CoFinite X)" using union_cocardinal unfolding Cofinite_def by auto
next
{
fix M assume "M∈Pow(CoFinite X)" "X⊆⋃M"
{
assume "M=0∨M={0}"
then have "M∈FinPow(M)" unfolding FinPow_def by auto
with ‹X⊆⋃M› have "∃N∈FinPow(M). X⊆⋃N" by auto
}
moreover
{
assume "M≠0""M≠{0}"
then obtain U where "U∈M""U≠0" by auto
with ‹M∈Pow(CoFinite X)› have "U∈CoFinite X" by auto
with ‹U≠0› have "U⊆X" "(X-U)≺nat" unfolding Cofinite_def CoCardinal_def by auto
then have "Finite(X-U)" using lesspoll_nat_is_Finite by auto
then have "(X-U){is in the spectrum of}(λT. (⋃T){is compact in}T)" using compact_spectrum
by auto
then have "((⋃(CoFinite (X-U)))≈X-U) ⟶ ((⋃(CoFinite (X-U))){is compact in}(CoFinite (X-U)))" unfolding Spec_def
using InfCard_nat CoCar_is_topology unfolding Cofinite_def by auto
then have com:"(X-U){is compact in}(CoFinite (X-U))" using union_cocardinal unfolding Cofinite_def by auto
have "(X-U)∩X=X-U" by auto
then have "(CoFinite X){restricted to}(X-U)=(CoFinite (X-U))" using subspace_cocardinal unfolding Cofinite_def by auto
with com have "(X-U){is compact in}(CoFinite X)" using compact_subspace_imp_compact[of "X-U""CoFinite X""X-U"] by auto
moreover have "X-U⊆⋃M" using ‹X⊆⋃M› by auto
moreover note ‹M∈Pow(CoFinite X)›
ultimately have "∃N∈FinPow(M). X-U⊆⋃N" unfolding IsCompact_def by auto
then obtain N where "N⊆M" "Finite(N)" "X-U⊆⋃N" unfolding FinPow_def by auto
with ‹U∈M› have "N ∪{U}⊆M" "Finite(N ∪{U})" "X⊆⋃(N ∪{U})" by auto
then have "∃N∈FinPow(M). X⊆⋃N" unfolding FinPow_def by blast
}
ultimately
have "∃N∈FinPow(M). X⊆⋃N" by auto
}
then show "∀M∈Pow(CoFinite X). X ⊆ ⋃M ⟶ (∃N∈FinPow(M). X ⊆ ⋃N)" by auto
qed
text‹A corollary is then that the cofinite topology is locally compact; since every subspace
of a cofinite space is cofinite.›
corollary cofinite_locally_compact:
shows "(CoFinite X){is locally-compact}"
proof-
have cof:"topology0(CoFinite X)" and cof1:"(CoFinite X){is a topology}"
using CoCar_is_topology InfCard_nat Cofinite_def unfolding topology0_def by auto
{
fix x B assume "x∈⋃(CoFinite X)" "B∈(CoFinite X)" "x∈B"
then have "x∈Interior(B,CoFinite X)" using topology0.Top_2_L3[OF cof] by auto moreover
from ‹B∈(CoFinite X)› have "B⊆X" unfolding Cofinite_def CoCardinal_def by auto
then have "B∩X=B" by auto
then have "(CoFinite X){restricted to}B=CoFinite B" using subspace_cocardinal unfolding Cofinite_def by auto
then have "B{is compact in}((CoFinite X){restricted to}B)" using cofinite_compact
union_cocardinal unfolding Cofinite_def by auto
then have "B{is compact in}(CoFinite X)" using compact_subspace_imp_compact by auto
ultimately have "∃c∈Pow(B). x∈Interior(c,CoFinite X)∧ c{is compact in}(CoFinite X)" by auto
}
then have "(∀x∈⋃(CoFinite X). ∀b∈(CoFinite X). x∈b ⟶ (∃c∈Pow(b). x∈Interior(c,CoFinite X) ∧ c{is compact in}(CoFinite X)))"
by auto
then show ?thesis unfolding IsLocallyComp_def IsLocally_def[OF cof1] by auto
qed
text‹In every locally compact space, by definition, every point has a compact neighbourhood.›
theorem (in topology0) locally_compact_exist_compact_neig:
assumes "T{is locally-compact}"
shows "∀x∈⋃T. ∃A∈Pow(⋃T). A{is compact in}T ∧ x∈int(A)"
proof-
{
fix x assume "x∈⋃T" moreover
then have "⋃T≠0" by auto
have "⋃T∈T" using union_open topSpaceAssum by auto
ultimately have "∃c∈Pow(⋃T). x∈int(c)∧ c{is compact in}T" using assms
IsLocally_def topSpaceAssum unfolding IsLocallyComp_def by auto
then have "∃c∈Pow(⋃T). c{is compact in}T ∧ x∈int(c)" by auto
}
then show ?thesis by auto
qed
text‹In Hausdorff spaces, the previous result is an equivalence.›
theorem (in topology0) exist_compact_neig_T2_imp_locally_compact:
assumes "∀x∈⋃T. ∃A∈Pow(⋃T). x∈int(A) ∧ A{is compact in}T" "T{is T⇩2}"
shows "T{is locally-compact}"
proof-
{
fix x assume "x∈⋃T"
with assms(1) obtain A where "A∈Pow(⋃T)" "x∈int(A)" and Acom:"A{is compact in}T" by blast
then have Acl:"A{is closed in}T" using in_t2_compact_is_cl assms(2) by auto
then have sub:"A⊆⋃T" unfolding IsClosed_def by auto
{
fix U assume "U∈T" "x∈U"
let ?V="int(A∩U)"
from ‹x∈U› ‹x∈int(A)› have "x∈U∩(int (A))" by auto
moreover from ‹U∈T› have "U∩(int(A))∈T" using Top_2_L2 topSpaceAssum unfolding IsATopology_def
by auto moreover
have "U∩(int(A))⊆A∩U" using Top_2_L1 by auto
ultimately have "x∈?V" using Top_2_L5 by blast
have "?V⊆A" using Top_2_L1 by auto
then have "cl(?V)⊆A" using Acl Top_3_L13 by auto
then have "A∩cl(?V)=cl(?V)" by auto moreover
have clcl:"cl(?V){is closed in}T" using cl_is_closed(1) ‹?V⊆A› ‹A⊆⋃T› by auto
ultimately have comp:"cl(?V){is compact in}T" using Acom compact_closed[of "A""nat""T""cl(?V)"] Compact_is_card_nat
by auto
{
then have "cl(?V){is compact in}(T{restricted to}cl(?V))" using compact_imp_compact_subspace[of "cl(?V)""nat""T"] Compact_is_card_nat
by auto moreover
have "⋃(T{restricted to}cl(?V))=cl(?V)" unfolding RestrictedTo_def using clcl unfolding IsClosed_def by auto moreover
ultimately have "(⋃(T{restricted to}cl(?V))){is compact in}(T{restricted to}cl(?V))" by auto
}
then have "(⋃(T{restricted to}cl(?V))){is compact in}(T{restricted to}cl(?V))" by auto moreover
have "(T{restricted to}cl(?V)){is T⇩2}" using assms(2) T2_here clcl unfolding IsClosed_def by auto
ultimately have "(T{restricted to}cl(?V)){is T⇩4}" using topology0.T2_compact_is_normal unfolding topology0_def
using Top_1_L4 unfolding isT4_def using T2_is_T1 by auto
then have clvreg:"(T{restricted to}cl(?V)){is regular}" using topology0.T4_is_T3 unfolding topology0_def isT3_def using Top_1_L4
by auto
have "?V⊆cl(?V)" using cl_contains_set ‹?V⊆A› ‹A⊆⋃T› by auto
then have "?V∈(T{restricted to}cl(?V))" unfolding RestrictedTo_def using Top_2_L2 by auto
with ‹x∈?V› obtain W where Wop:"W∈(T{restricted to}cl(?V))" and clcont:"Closure(W,(T{restricted to}cl(?V)))⊆?V" and cinW:"x∈W"
using topology0.regular_imp_exist_clos_neig unfolding topology0_def using Top_1_L4 clvreg
by blast
from clcont Wop have "W⊆?V" using topology0.cl_contains_set unfolding topology0_def using Top_1_L4 by auto
with Wop have "W∈(T{restricted to}cl(?V)){restricted to}?V" unfolding RestrictedTo_def by auto
moreover from ‹?V⊆A› ‹A⊆⋃T› have "?V⊆⋃T" by auto
then have "?V⊆cl(?V)""cl(?V)⊆⋃T" using ‹?V⊆cl(?V)› Top_3_L11(1) by auto
then have "(T{restricted to}cl(?V)){restricted to}?V=(T{restricted to}?V)" using subspace_of_subspace by auto
ultimately have "W∈(T{restricted to}?V)" by auto
then obtain UU where "UU∈T" "W=UU∩?V" unfolding RestrictedTo_def by auto
then have "W∈T" using Top_2_L2 topSpaceAssum unfolding IsATopology_def by auto moreover
have "W⊆Closure(W,(T{restricted to}cl(?V)))" using topology0.cl_contains_set unfolding topology0_def
using Top_1_L4 Wop by auto
ultimately have A1:"x∈int(Closure(W,(T{restricted to}cl(?V))))" using Top_2_L6 cinW by auto
from clcont have A2:"Closure(W,(T{restricted to}cl(?V)))⊆U" using Top_2_L1 by auto
have clwcl:"Closure(W,(T{restricted to}cl(?V))) {is closed in}(T{restricted to}cl(?V))"
using topology0.cl_is_closed(1) Top_1_L4 Wop unfolding topology0_def by auto
from comp have "cl(?V){is compact in}(T{restricted to}cl(?V))" using compact_imp_compact_subspace[of "cl(?V)""nat""T"] Compact_is_card_nat
by auto
with clwcl have "((cl(?V)∩(Closure(W,(T{restricted to}cl(?V)))))){is compact in}(T{restricted to}cl(?V))"
using compact_closed Compact_is_card_nat by auto moreover
from clcont have cont:"(Closure(W,(T{restricted to}cl(?V))))⊆cl(?V)" using cl_contains_set ‹?V⊆A›‹A⊆⋃T›
by blast
then have "((cl(?V)∩(Closure(W,(T{restricted to}cl(?V))))))=Closure(W,(T{restricted to}cl(?V)))" by auto
ultimately have "Closure(W,(T{restricted to}cl(?V))){is compact in}(T{restricted to}cl(?V))" by auto
then have "Closure(W,(T{restricted to}cl(?V))){is compact in}T" using compact_subspace_imp_compact[of "Closure(W,T{restricted to}cl(?V))"]
cont by auto
with A1 A2 have "∃c∈Pow(U). x∈int(c)∧c{is compact in}T" by auto
}
then have "∀U∈T. x∈U ⟶ (∃c∈Pow(U). x∈int(c)∧c{is compact in}T)" by auto
}
then show ?thesis unfolding IsLocally_def[OF topSpaceAssum] IsLocallyComp_def by auto
qed
subsection‹Compactification by one point›
text‹Given a topological space, we can always add one point to the space and get a new compact topology; as we
will check in this section.›
definition
OPCompactification ("{one-point compactification of}_" 90)
where "{one-point compactification of}T≡T∪{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}"
text‹Firstly, we check that what we defined is indeed a topology.›
theorem (in topology0) op_comp_is_top:
shows "({one-point compactification of}T){is a topology}" unfolding IsATopology_def
proof(safe)
fix M assume "M⊆{one-point compactification of}T"
then have disj:"M⊆T∪{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}" unfolding OPCompactification_def by auto
let ?MT="{A∈M. A∈T}"
have "?MT⊆T" by auto
then have c1:"⋃?MT∈T" using topSpaceAssum unfolding IsATopology_def by auto
let ?MK="{A∈M. A∉T}"
have "⋃M=⋃?MK ∪ ⋃?MT" by auto
from disj have "?MK⊆{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}" by auto
moreover have N:"⋃T∉(⋃T)" using mem_not_refl by auto
{
fix B assume "B∈M" "B∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}"
then obtain K where "K∈Pow(⋃T)" "B={⋃T}∪((⋃T)-K)" by auto
with N have "⋃T∈B" by auto
with N have "B∉T" by auto
with ‹B∈M› have "B∈?MK" by auto
}
then have "{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}⊆?MK" by auto
ultimately have MK_def:"?MK={A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}" by auto
let ?KK="{K∈Pow(⋃T). {⋃T}∪((⋃T)-K)∈?MK}"
{
assume "?MK=0"
then have "⋃M=⋃?MT" by auto
then have "⋃M∈T" using c1 by auto
then have "⋃M∈{one-point compactification of}T" unfolding OPCompactification_def by auto
}
moreover
{
assume "?MK≠0"
then obtain A where "A∈?MK" by auto
then obtain K1 where "A={⋃T}∪((⋃T)-K1)" "K1∈Pow(⋃T)" "K1{is closed in}T" "K1{is compact in}T" using MK_def by auto
with ‹A∈?MK› have "⋂?KK⊆K1" by auto
from ‹A∈?MK› ‹A={⋃T}∪((⋃T)-K1)› ‹K1∈Pow(⋃T)› have "?KK≠0" by blast
{
fix K assume "K∈?KK"
then have "{⋃T}∪((⋃T)-K)∈?MK" "K⊆⋃T" by auto
then obtain KK where A:"{⋃T}∪((⋃T)-K)={⋃T}∪((⋃T)-KK)" "KK⊆⋃T" "KK{is compact in}T" "KK{is closed in}T" using MK_def by auto
note A(1) moreover
have "(⋃T)-K⊆{⋃T}∪((⋃T)-K)" "(⋃T)-KK⊆{⋃T}∪((⋃T)-KK)" by auto
ultimately have "(⋃T)-K⊆{⋃T}∪((⋃T)-KK)" "(⋃T)-KK⊆{⋃T}∪((⋃T)-K)" by auto moreover
from N have "⋃T∉(⋃T)-K" "⋃T∉(⋃T)-KK" by auto ultimately
have "(⋃T)-K⊆((⋃T)-KK)" "(⋃T)-KK⊆((⋃T)-K)" by auto
then have "(⋃T)-K=(⋃T)-KK" by auto moreover
from ‹K⊆⋃T› have "K=(⋃T)-((⋃T)-K)" by auto ultimately
have "K=(⋃T)-((⋃T)-KK)" by auto
with ‹KK⊆⋃T› have "K=KK" by auto
with A(4) have "K{is closed in}T" by auto
}
then have "∀K∈?KK. K{is closed in}T" by auto
with ‹?KK≠0› have "(⋂?KK){is closed in}T" using Top_3_L4 by auto
with ‹K1{is compact in}T› have "(K1∩(⋂?KK)){is compact in}T" using Compact_is_card_nat
compact_closed[of "K1""nat""T""⋂?KK"] by auto moreover
from ‹⋂?KK⊆K1› have "K1∩(⋂?KK)=(⋂?KK)" by auto ultimately
have "(⋂?KK){is compact in}T" by auto
with ‹(⋂?KK){is closed in}T› ‹⋂?KK⊆K1› ‹K1∈Pow(⋃T)› have "({⋃T}∪((⋃T)-(⋂?KK)))∈({one-point compactification of}T)"
unfolding OPCompactification_def by blast
have t:"⋃?MK=⋃{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}"
using MK_def by auto
{
fix x assume "x∈⋃?MK"
with t have "x∈⋃{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}" by auto
then have "∃AA∈{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}. x∈AA"
using Union_iff by auto
then obtain AA where AAp:"AA∈{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}" "x∈AA" by auto
then obtain K2 where "AA={⋃T}∪((⋃T)-K2)" "K2∈Pow(⋃T)""K2{is compact in}T" "K2{is closed in}T" by auto
with ‹x∈AA› have "x=⋃T ∨ (x∈(⋃T) ∧ x∉K2)" by auto
from ‹K2∈Pow(⋃T)› ‹AA={⋃T}∪((⋃T)-K2)› AAp(1) MK_def have "K2∈?KK" by auto
then have "⋂?KK⊆K2" by auto
with ‹x=⋃T ∨ (x∈(⋃T) ∧ x∉K2)› have "x=⋃T∨(x∈⋃T ∧ x∉⋂?KK)" by auto
then have "x∈{⋃T}∪((⋃T)-(⋂?KK))" by auto
}
then have "⋃?MK⊆{⋃T}∪((⋃T)-(⋂?KK))" by auto
moreover
{
fix x assume "x∈{⋃T}∪((⋃T)-(⋂?KK))"
then have "x=⋃T∨(x∈(⋃T)∧ x∉⋂?KK)" by auto
with ‹?KK≠0› obtain K2 where "K2∈?KK" "x=⋃T∨(x∈⋃T∧ x∉K2)" by auto
then have "{⋃T}∪((⋃T)-K2)∈?MK" by auto
with ‹x=⋃T∨(x∈⋃T∧ x∉K2)› have "x∈⋃?MK" by auto
}
then have "{⋃T}∪((⋃T)-(⋂?KK))⊆⋃?MK" by (safe,auto)
ultimately have "⋃?MK={⋃T}∪((⋃T)-(⋂?KK))" by blast
from ‹⋃?MT∈T› have "⋃T-(⋃T-⋃?MT)=⋃?MT" by auto
with ‹⋃?MT∈T› have "(⋃T-⋃?MT){is closed in}T" unfolding IsClosed_def by auto
have "((⋃T)-(⋂?KK))∪(⋃T-(⋃T-⋃?MT))=(⋃T)-((⋂?KK)∩(⋃T-⋃?MT))" by auto
then have "({⋃T}∪((⋃T)-(⋂?KK)))∪(⋃T-(⋃T-⋃?MT))={⋃T}∪((⋃T)-((⋂?KK)∩(⋃T-⋃?MT)))" by auto
with ‹⋃?MK={⋃T}∪((⋃T)-(⋂?KK))›‹⋃T-(⋃T-⋃?MT)=⋃?MT› have "⋃?MK∪⋃?MT={⋃T}∪((⋃T)-((⋂?KK)∩(⋃T-⋃?MT)))"
by auto
with ‹⋃M=⋃?MK ∪⋃?MT› have unM:"⋃M={⋃T}∪((⋃T)-((⋂?KK)∩(⋃T-⋃?MT)))" by auto
have "((⋂?KK)∩(⋃T-⋃?MT)) {is closed in}T" using ‹(⋂?KK){is closed in}T›‹(⋃T-(⋃?MT)){is closed in}T›
Top_3_L5 by auto
moreover
note ‹(⋃T-(⋃?MT)){is closed in}T› ‹(⋂?KK){is compact in}T›
then have "((⋂?KK)∩(⋃T-⋃?MT)){is compact of cardinal}nat{in}T" using compact_closed[of "⋂?KK""nat""T""(⋃T-⋃?MT)"] Compact_is_card_nat
by auto
then have "((⋂?KK)∩(⋃T-⋃?MT)){is compact in}T" using Compact_is_card_nat by auto
ultimately have "{⋃T}∪(⋃T-((⋂?KK)∩(⋃T-⋃?MT)))∈{one-point compactification of}T"
unfolding OPCompactification_def IsClosed_def by auto
with unM have "⋃M∈{one-point compactification of}T" by auto
}
ultimately show "⋃M∈{one-point compactification of}T" by auto
next
fix U V assume "U∈{one-point compactification of}T" and "V∈{one-point compactification of}T"
then have A:"U∈T∨(∃KU∈Pow(⋃T). U={⋃T}∪(⋃T-KU)∧KU{is closed in}T∧KU{is compact in}T)"
"V∈T∨(∃KV∈Pow(⋃T). V={⋃T}∪(⋃T-KV)∧KV{is closed in}T∧KV{is compact in}T)" unfolding OPCompactification_def
by auto
have N:"⋃T∉(⋃T)" using mem_not_refl by auto
{
assume "U∈T""V∈T"
then have "U∩V∈T" using topSpaceAssum unfolding IsATopology_def by auto
then have "U∩V∈{one-point compactification of}T" unfolding OPCompactification_def
by auto
}
moreover
{
assume "U∈T""V∉T"
then obtain KV where V:"KV{is closed in}T""KV{is compact in}T""V={⋃T}∪(⋃T-KV)"
using A(2) by auto
with N ‹U∈T› have "⋃T∉U" by auto
then have "⋃T∉U∩V" by auto
then have "U∩V=U∩(⋃T-KV)" using V(3) by auto
moreover have "⋃T-KV∈T" using V(1) unfolding IsClosed_def by auto
with ‹U∈T› have "U∩(⋃T-KV)∈T" using topSpaceAssum unfolding IsATopology_def by auto
with ‹U∩V=U∩(⋃T-KV)› have "U∩V∈T" by auto
then have "U∩V∈{one-point compactification of}T" unfolding OPCompactification_def by auto
}
moreover
{
assume "U∉T""V∈T"
then obtain KV where V:"KV{is closed in}T""KV{is compact in}T""U={⋃T}∪(⋃T-KV)"
using A(1) by auto
with N ‹V∈T› have "⋃T∉V" by auto
then have "⋃T∉U∩V" by auto
then have "U∩V=(⋃T-KV)∩V" using V(3) by auto
moreover have "⋃T-KV∈T" using V(1) unfolding IsClosed_def by auto
with ‹V∈T› have "(⋃T-KV)∩V∈T" using topSpaceAssum unfolding IsATopology_def by auto
with ‹U∩V=(⋃T-KV)∩V› have "U∩V∈T" by auto
then have "U∩V∈{one-point compactification of}T" unfolding OPCompactification_def by auto
}
moreover
{
assume "U∉T""V∉T"
then obtain KV KU where V:"KV{is closed in}T""KV{is compact in}T""V={⋃T}∪(⋃T-KV)"
and U:"KU{is closed in}T""KU{is compact in}T""U={⋃T}∪(⋃T-KU)"
using A by auto
with V(3) U(3) have "⋃T∈U∩V" by auto
then have "U∩V={⋃T}∪((⋃T-KV)∩(⋃T-KU))" using V(3) U(3) by auto
moreover have "⋃T-KV∈T""⋃T-KU∈T" using V(1) U(1) unfolding IsClosed_def by auto
then have "(⋃T-KV)∩(⋃T-KU)∈T" using topSpaceAssum unfolding IsATopology_def by auto
then have "(⋃T-KV)∩(⋃T-KU)=⋃T-(⋃T-((⋃T-KV)∩(⋃T-KU)))" by auto moreover
with ‹(⋃T-KV)∩(⋃T-KU)∈T› have "(⋃T-(⋃T-KV)∩(⋃T-KU)){is closed in}T" unfolding IsClosed_def
by auto moreover
from V(1) U(1) have "(⋃T-(⋃T-KV)∩(⋃T-KU))=KV∪KU" unfolding IsClosed_def by auto
with V(2) U(2) have "(⋃T-(⋃T-KV)∩(⋃T-KU)){is compact in}T" using union_compact[of "KV""nat""T""KU"] Compact_is_card_nat
InfCard_nat by auto ultimately
have "U∩V∈{one-point compactification of}T" unfolding OPCompactification_def by auto
}
ultimately show "U∩V∈{one-point compactification of}T" by auto
qed
text‹The original topology is an open subspace of the new topology.›
theorem (in topology0) open_subspace:
shows "⋃T∈{one-point compactification of}T" and "({one-point compactification of}T){restricted to}⋃T=T"
proof-
show "⋃T∈{one-point compactification of}T"
unfolding OPCompactification_def using topSpaceAssum unfolding IsATopology_def by auto
have "T⊆({one-point compactification of}T){restricted to}⋃T" unfolding OPCompactification_def RestrictedTo_def by auto
moreover
{
fix A assume "A∈({one-point compactification of}T){restricted to}⋃T"
then obtain R where "R∈({one-point compactification of}T)" "A=⋃T∩R" unfolding RestrictedTo_def by auto
then obtain K where K:"R∈T ∨ (R={⋃T}∪(⋃T-K) ∧ K{is closed in}T)" unfolding OPCompactification_def by auto
with ‹A=⋃T∩R› have "(A=R∧R∈T)∨(A=⋃T-K ∧ K{is closed in}T)" using mem_not_refl unfolding IsClosed_def by auto
with K have "A∈T" unfolding IsClosed_def by auto
}
ultimately
show "({one-point compactification of}T){restricted to}⋃T=T" by auto
qed
text‹We added only one new point to the space.›
lemma (in topology0) op_compact_total:
shows "⋃({one-point compactification of}T)={⋃T}∪(⋃T)"
proof-
have "0{is compact in}T" unfolding IsCompact_def FinPow_def by auto
moreover note Top_3_L2 ultimately have TT:"0∈{A∈Pow(⋃T). A{is compact in}T ∧A{is closed in}T}" by auto
have "⋃({one-point compactification of}T)=(⋃T)∪(⋃{{⋃T}∪(⋃T-K). K∈{B∈Pow(⋃T). B{is compact in}T∧B{is closed in}T}})" unfolding OPCompactification_def
by blast
also have "…=(⋃T)∪{⋃T}∪(⋃{(⋃T-K). K∈{B∈Pow(⋃T). B{is compact in}T∧B{is closed in}T}})" using TT by auto
ultimately show "⋃({one-point compactification of}T)={⋃T}∪(⋃T)" by auto
qed
text‹The one point compactification, gives indeed a compact topological space.›
theorem (in topology0) compact_op:
shows "({⋃T}∪(⋃T)){is compact in}({one-point compactification of}T)" unfolding IsCompact_def
proof(safe)
have "0{is compact in}T" unfolding IsCompact_def FinPow_def by auto
moreover note Top_3_L2 ultimately have "0∈{A∈Pow(⋃T). A{is compact in}T ∧A{is closed in}T}" by auto
then have "{⋃T}∪(⋃T)∈{one-point compactification of}T" unfolding OPCompactification_def by auto
then show "⋃T ∈ ⋃{one-point compactification of}T" by auto
next
fix x B assume "x∈B""B∈T"
then show "x∈⋃({one-point compactification of}T)" using open_subspace by auto
next
fix M assume A:"M⊆({one-point compactification of}T)" "{⋃T} ∪ ⋃T ⊆ ⋃M"
then obtain R where "R∈M""⋃T∈R" by auto
have "⋃T∉⋃T" using mem_not_refl by auto
with ‹R∈M› ‹⋃T∈R› A(1) obtain K where K:"R={⋃T}∪(⋃T-K)" "K{is compact in}T""K{is closed in}T"
unfolding OPCompactification_def by auto
from K(1,2) have B:"{⋃T} ∪ (⋃T) = R ∪ K" unfolding IsCompact_def by auto
with A(2) have "K⊆⋃M" by auto
from K(2) have "K{is compact in}(({one-point compactification of}T){restricted to}⋃T)" using open_subspace(2)
by auto
then have "K{is compact in}({one-point compactification of}T)" using compact_subspace_imp_compact
‹K{is closed in}T› unfolding IsClosed_def by auto
with ‹K⊆⋃M› A(1) have "(∃N∈FinPow(M). K ⊆ ⋃N)" unfolding IsCompact_def by auto
then obtain N where "N∈FinPow(M)" "K⊆⋃N" by auto
with ‹R∈M› have "(N ∪{R})∈FinPow(M)""R∪K⊆⋃(N∪{R})" unfolding FinPow_def by auto
with B show "∃N∈FinPow(M). {⋃T} ∪ (⋃T)⊆⋃N" by auto
qed
text‹The one point compactification is Hausdorff iff the original space is also
Hausdorff and locally compact.›
lemma (in topology0) op_compact_T2_1:
assumes "({one-point compactification of}T){is T⇩2}"
shows "T{is T⇩2}"
using T2_here[OF assms, of "⋃T"] open_subspace by auto
lemma (in topology0) op_compact_T2_2:
assumes "({one-point compactification of}T){is T⇩2}"
shows "T{is locally-compact}"
proof-
{
fix x assume "x∈⋃T"
then have "x∈{⋃T}∪(⋃T)" by auto
moreover have "⋃T∈{⋃T}∪(⋃T)" by auto moreover
from ‹x∈⋃T› have "x≠⋃T" using mem_not_refl by auto
ultimately have "∃U∈{one-point compactification of}T. ∃V∈{one-point compactification of}T. x ∈ U ∧ (⋃T) ∈ V ∧ U ∩ V = 0"
using assms op_compact_total unfolding isT2_def by auto
then obtain U V where UV:"U∈{one-point compactification of}T""V∈{one-point compactification of}T"
"x∈U""⋃T∈V""U∩V=0" by auto
from ‹V∈{one-point compactification of}T› ‹⋃T∈V› mem_not_refl obtain K where K:"V={⋃T}∪(⋃T-K)""K{is closed in}T""K{is compact in}T"
unfolding OPCompactification_def by auto
from ‹U∈{one-point compactification of}T› have "U⊆{⋃T}∪(⋃T)" unfolding OPCompactification_def
using op_compact_total by auto
with ‹U∩V=0› K have "U⊆K""K⊆⋃T" unfolding IsClosed_def by auto
then have "(⋃T)∩U=U" by auto moreover
from UV(1) have "((⋃T)∩U)∈({one-point compactification of}T){restricted to}⋃T"
unfolding RestrictedTo_def by auto
ultimately have "U∈T" using open_subspace(2) by auto
with ‹x∈U›‹U⊆K› have "x∈int(K)" using Top_2_L6 by auto
with ‹K⊆⋃T› ‹K{is compact in}T› have "∃A∈Pow(⋃T). x∈int(A)∧ A{is compact in}T" by auto
}
then have "∀x∈⋃T. ∃A∈Pow(⋃T). x∈int(A)∧ A{is compact in}T" by auto
then show ?thesis using op_compact_T2_1[OF assms] exist_compact_neig_T2_imp_locally_compact
by auto
qed
lemma (in topology0) op_compact_T2_3:
assumes "T{is locally-compact}" "T{is T⇩2}"
shows "({one-point compactification of}T){is T⇩2}"
proof-
{
fix x y assume "x≠y""x∈⋃({one-point compactification of}T)""y∈⋃({one-point compactification of}T)"
then have S:"x∈{⋃T}∪(⋃T)""y∈{⋃T}∪(⋃T)" using op_compact_total by auto
{
assume "x∈⋃T""y∈⋃T"
with ‹x≠y› have "∃U∈T. ∃V∈T. x∈U∧y∈V∧U∩V=0" using assms(2) unfolding isT2_def by auto
then have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0"
unfolding OPCompactification_def by auto
}
moreover
{
assume "x∉⋃T∨y∉⋃T"
with S have "x=⋃T∨y=⋃T" by auto
with ‹x≠y› have "(x=⋃T∧y≠⋃T)∨(y=⋃T∧x≠⋃T)" by auto
with S have "(x=⋃T∧y∈⋃T)∨(y=⋃T∧x∈⋃T)" by auto
then obtain Ky Kx where "(x=⋃T∧ Ky{is compact in}T∧y∈int(Ky))∨(y=⋃T∧ Kx{is compact in}T∧x∈int(Kx))"
using assms(1) locally_compact_exist_compact_neig by blast
then have "(x=⋃T∧ Ky{is compact in}T∧ Ky{is closed in}T∧y∈int(Ky))∨(y=⋃T∧ Kx{is compact in}T∧ Kx{is closed in}T∧x∈int(Kx))"
using in_t2_compact_is_cl assms(2) by auto
then have "(x∈{⋃T}∪(⋃T-Ky)∧y∈int(Ky)∧ Ky{is compact in}T∧ Ky{is closed in}T)∨(y∈{⋃T}∪(⋃T-Kx)∧x∈int(Kx)∧ Kx{is compact in}T∧ Kx{is closed in}T)"
by auto moreover
{
fix K
assume A:"K{is closed in}T""K{is compact in}T"
then have "K⊆⋃T" unfolding IsClosed_def by auto
moreover have "⋃T∉⋃T" using mem_not_refl by auto
ultimately have "({⋃T}∪(⋃T-K))∩K=0" by auto
then have "({⋃T}∪(⋃T-K))∩int(K)=0" using Top_2_L1 by auto moreover
from A have "{⋃T}∪(⋃T-K)∈({one-point compactification of}T)" unfolding OPCompactification_def
IsClosed_def by auto moreover
have "int(K)∈({one-point compactification of}T)" using Top_2_L2 unfolding OPCompactification_def
by auto ultimately
have "int(K)∈({one-point compactification of}T)∧{⋃T}∪(⋃T-K)∈({one-point compactification of}T)∧({⋃T}∪(⋃T-K))∩int(K)=0"
by auto
}
ultimately have "({⋃T} ∪ (⋃T - Ky)∈({one-point compactification of}T)∧int(Ky)∈({one-point compactification of}T)∧x ∈ {⋃T} ∪ (⋃T - Ky) ∧ y ∈ int(Ky) ∧ ({⋃T}∪(⋃T-Ky))∩int(Ky)=0) ∨
({⋃T} ∪ (⋃T - Kx)∈({one-point compactification of}T)∧int(Kx)∈({one-point compactification of}T)∧y ∈ {⋃T} ∪ (⋃T - Kx) ∧ x ∈ int(Kx) ∧ ({⋃T}∪(⋃T-Kx))∩int(Kx)=0)" by auto
moreover
{
assume "({⋃T} ∪ (⋃T - Ky)∈({one-point compactification of}T)∧int(Ky)∈({one-point compactification of}T)∧x ∈ {⋃T} ∪ (⋃T - Ky) ∧ y ∈ int(Ky) ∧ ({⋃T}∪(⋃T-Ky))∩int(Ky)=0)"
then have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0" using exI[OF exI[of _ "int(Ky)"],of "λU V. U∈({one-point compactification of}T)∧V∈({one-point compactification of}T) ∧ x∈U∧y∈V∧U∩V=0" "{⋃T}∪(⋃T-Ky)"]
by auto
} moreover
{
assume "({⋃T} ∪ (⋃T - Kx)∈({one-point compactification of}T)∧int(Kx)∈({one-point compactification of}T)∧y ∈ {⋃T} ∪ (⋃T - Kx) ∧ x ∈ int(Kx) ∧ ({⋃T}∪(⋃T-Kx))∩int(Kx)=0)"
then have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0" using exI[OF exI[of _ "{⋃T}∪(⋃T-Kx)"],of "λU V. U∈({one-point compactification of}T)∧V∈({one-point compactification of}T) ∧ x∈U∧y∈V∧U∩V=0""int(Kx)" ]
by blast
}
ultimately have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0" by auto
}
ultimately have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0" by auto
}
then show ?thesis unfolding isT2_def by auto
qed
text‹In conclusion, every locally compact Hausdorff topological space is regular; since this property is hereditary.›
corollary (in topology0) locally_compact_T2_imp_regular:
assumes "T{is locally-compact}" "T{is T⇩2}"
shows "T{is regular}"
proof-
from assms have "( {one-point compactification of}T) {is T⇩2}" using op_compact_T2_3 by auto
then have "({one-point compactification of}T) {is T⇩4}" unfolding isT4_def using T2_is_T1 topology0.T2_compact_is_normal
op_comp_is_top unfolding topology0_def using op_compact_total compact_op by auto
then have "({one-point compactification of}T) {is T⇩3}" using topology0.T4_is_T3 op_comp_is_top unfolding topology0_def
by auto
then have "({one-point compactification of}T) {is regular}" using isT3_def by auto moreover
have "⋃T⊆⋃({one-point compactification of}T)" using op_compact_total by auto
ultimately have "(({one-point compactification of}T){restricted to}⋃T) {is regular}" using regular_here by auto
then show "T{is regular}" using open_subspace(2) by auto
qed
text‹This last corollary has an explanation: In Hausdorff spaces, compact sets are closed
and regular spaces are exactly the "locally closed spaces"(those which have a neighbourhood basis of closed sets).
So the neighbourhood basis of compact sets also works as the neighbourhood basis of closed sets we needed to find.›
definition
IsLocallyClosed ("_{is locally-closed}")
where "T{is locally-closed} ≡ T{is locally}(λB TT. B{is closed in}TT)"
lemma (in topology0) regular_locally_closed:
shows "T{is regular} ⟷ (T{is locally-closed})"
proof
assume "T{is regular}"
then have a:"∀x∈⋃T. ∀U∈T. (x∈U) ⟶ (∃V∈T. x ∈ V ∧ cl(V) ⊆ U)" using regular_imp_exist_clos_neig by auto
{
fix x b assume "x∈⋃T""b∈T""x∈b"
with a obtain V where "V∈T""x∈V""cl(V)⊆b" by blast
note ‹cl(V)⊆b› moreover
from ‹V∈T› have "V⊆⋃T" by auto
then have "V⊆cl(V)" using cl_contains_set by auto
with ‹x∈V›‹V∈T› have "x∈int(cl(V))" using Top_2_L6 by auto moreover
from ‹V⊆⋃T› have "cl(V){is closed in}T" using cl_is_closed by auto
ultimately have "x∈int(cl(V))""cl(V)⊆b""cl(V){is closed in}T" by auto
then have "∃K∈Pow(b). x∈int(K)∧K{is closed in}T" by auto
}
then show "T{is locally-closed}" unfolding IsLocally_def[OF topSpaceAssum] IsLocallyClosed_def
by auto
next
assume "T{is locally-closed}"
then have a:"∀x∈⋃T. ∀b∈T. x∈b ⟶ (∃K∈Pow(b). x∈int(K)∧K{is closed in}T)" unfolding IsLocally_def[OF topSpaceAssum]
IsLocallyClosed_def by auto
{
fix x b assume "x∈⋃T""b∈T""x∈b"
with a obtain K where K:"K⊆b""x∈int(K)""K{is closed in}T" by blast
have "int(K)⊆K" using Top_2_L1 by auto
with K(3) have "cl(int(K))⊆K" using Top_3_L13 by auto
with K(1) have "cl(int(K))⊆b" by auto moreover
have "int(K)∈T" using Top_2_L2 by auto moreover
note ‹x∈int(K)› ultimately have "∃V∈T. x∈V∧ cl(V)⊆b" by auto
}
then have "∀x∈⋃T. ∀b∈T. x∈b ⟶ (∃V∈T. x∈V∧ cl(V)⊆b)" by auto
then show "T{is regular}" using exist_clos_neig_imp_regular by auto
qed
subsection‹Hereditary properties and local properties›
text‹In this section, we prove a relation between a property and its local property
for hereditary properties. Then we apply it to locally-Hausdorff or locally-$T_2$.
We also prove the relation between locally-$T_2$ and
another property that appeared when considering anti-properties, the
anti-hyperconnectness.›
text‹If a property is hereditary in open sets, then local properties are equivalent
to find just one open neighbourhood with that property instead of a whole local basis.›
lemma (in topology0) her_P_is_loc_P:
assumes "∀TT. ∀B∈Pow(⋃TT). ∀A∈TT. TT{is a topology}∧P(B,TT) ⟶ P(B∩A,TT)"
shows "(T{is locally}P) ⟷ (∀x∈⋃T. ∃A∈T. x∈A∧P(A,T))"
proof
assume A:"T{is locally}P"
{
fix x assume x:"x∈⋃T"
with A have "∀b∈T. x∈b ⟶ (∃c∈Pow(b). x∈int(c)∧P(c,T))" unfolding IsLocally_def[OF topSpaceAssum]
by auto moreover
note x moreover
have "⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto
ultimately have "∃c∈Pow(⋃T). x∈int(c)∧ P(c,T)" by auto
then obtain c where c:"c⊆⋃T""x∈int(c)""P(c,T)" by auto
have P:"int(c)∈T" using Top_2_L2 by auto moreover
from c(1,3) topSpaceAssum assms have "∀A∈T. P(c∩A,T)" by auto
ultimately have "P(c∩int(c),T)" by auto moreover
from Top_2_L1[of "c"] have "int(c)⊆c" by auto
then have "c∩int(c)=int(c)" by auto
ultimately have "P(int(c),T)" by auto
with P c(2) have "∃V∈T. x∈V∧P(V,T)" by auto
}
then show "∀x∈⋃T. ∃V∈T. x∈V∧P(V,T)" by auto
next
assume A:"∀x∈⋃T. ∃A∈T. x ∈ A ∧ P(A, T)"
{
fix x assume x:"x∈⋃T"
{
fix b assume b:"x∈b""b∈T"
from x A obtain A where A_def:"A∈T""x∈A""P(A,T)" by auto
from A_def(1,3) assms topSpaceAssum have "∀G∈T. P(A∩G,T)" by auto
with b(2) have "P(A∩b,T)" by auto
moreover from b(1) A_def(2) have "x∈A∩b" by auto moreover
have "A∩b∈T" using b(2) A_def(1) topSpaceAssum IsATopology_def by auto
then have "int(A∩b)=A∩b" using Top_2_L3 by auto
ultimately have "x∈int(A∩b)∧P(A∩b,T)" by auto
then have "∃c∈Pow(b). x∈int(c)∧P(c,T)" by auto
}
then have "∀b∈T. x∈b⟶(∃c∈Pow(b). x∈int(c)∧P(c,T))" by auto
}
then show "T{is locally}P" unfolding IsLocally_def[OF topSpaceAssum] by auto
qed
definition
IsLocallyT2 ("_{is locally-T⇩2}" 70)
where "T{is locally-T⇩2}≡T{is locally}(λB. λT. (T{restricted to}B){is T⇩2})"
text‹Since $T_2$ is an hereditary property, we can apply the previous lemma.›
corollary (in topology0) loc_T2:
shows "(T{is locally-T⇩2}) ⟷ (∀x∈⋃T. ∃A∈T. x∈A∧(T{restricted to}A){is T⇩2})"
proof-
{
fix TT B A assume TT:"TT{is a topology}" "(TT{restricted to}B){is T⇩2}" "A∈TT""B∈Pow(⋃TT)"
then have s:"B∩A⊆B""B⊆⋃TT" by auto
then have "(TT{restricted to}(B∩A))=(TT{restricted to}B){restricted to}(B∩A)" using subspace_of_subspace
by auto moreover
have "⋃(TT{restricted to}B)=B" unfolding RestrictedTo_def using s(2) by auto
then have "B∩A⊆⋃(TT{restricted to}B)" using s(1) by auto moreover
note TT(2) ultimately have "(TT{restricted to}(B∩A)){is T⇩2}" using T2_here
by auto
}
then have "∀TT. ∀B∈Pow(⋃TT). ∀A∈TT. TT{is a topology}∧(TT{restricted to}B){is T⇩2} ⟶ (TT{restricted to}(B∩A)){is T⇩2}"
by auto
with her_P_is_loc_P[where P="λA. λTT. (TT{restricted to}A){is T⇩2}"] show ?thesis unfolding IsLocallyT2_def by auto
qed
text‹First, we prove that a locally-$T_2$ space is anti-hyperconnected.›
text‹Before starting, let's prove that an open subspace of an hyperconnected
space is hyperconnected.›
lemma(in topology0) open_subspace_hyperconn:
assumes "T{is hyperconnected}" "U∈T"
shows "(T{restricted to}U){is hyperconnected}"
proof-
{
fix A B assume "A∈(T{restricted to}U)""B∈(T{restricted to}U)""A∩B=0"
then obtain AU BU where "A=U∩AU""B=U∩BU" "AU∈T""BU∈T" unfolding RestrictedTo_def by auto
then have "A∈T""B∈T" using topSpaceAssum assms(2) unfolding IsATopology_def by auto
with ‹A∩B=0› have "A=0∨B=0" using assms(1) unfolding IsHConnected_def by auto
}
then show ?thesis unfolding IsHConnected_def by auto
qed
lemma(in topology0) locally_T2_is_antiHConn:
assumes "T{is locally-T⇩2}"
shows "T{is anti-}IsHConnected"
proof-
{
fix A assume A:"A∈Pow(⋃T)""(T{restricted to}A){is hyperconnected}"
{
fix x assume "x∈A"
with A(1) have "x∈⋃T" by auto moreover
have "⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto ultimately
have "∃c∈Pow(⋃T). x ∈ int(c) ∧ (T {restricted to} c) {is T⇩2}" using