section ‹ Topology and neighborhoods ›
theory Topology_ZF_4a imports Topology_ZF_4
begin
text‹ This theory considers the relations between topology and systems of neighborhood filters. ›
subsection‹ Neighborhood systems ›
text‹ The standard way of defining a topological space is by specifying a collection
of sets that we consider "open" (see the ‹Topology_ZF› theory).
An alternative of this approach is to define a collection of neighborhoods for each point of
the space. ›
text‹ We define a neighborhood system as a function that takes each point $x\in X$ and assigns it
a collection of subsets of $X$ which is called the neighborhoods of $x$.
The neighborhoods of a point $x$ form a filter that satisfies an additional
axiom that for every neighborhood $N$ of $x$ we can find another one $U$ such that $N$
is a neighborhood of every point of $U$. ›
definition
IsNeighSystem ("_ {is a neighborhood system on} _" 90)
where "ℳ {is a neighborhood system on} X ≡ (ℳ : X→Pow(Pow(X))) ∧
(∀x∈X. (ℳ`(x) {is a filter on} X) ∧ (∀N∈ℳ`(x). x∈N ∧ (∃U∈ℳ`(x).∀y∈U.(N∈ℳ`(y)) ) ))"
text‹ A neighborhood system on $X$ consists of collections of subsets of $X$. ›
lemma neighborhood_subset:
assumes "ℳ {is a neighborhood system on} X" and "x∈X" and "N∈ℳ`(x)"
shows "N⊆X" and "x∈N"
proof -
from ‹ℳ {is a neighborhood system on} X› have "ℳ : X→Pow(Pow(X))"
unfolding IsNeighSystem_def by simp
with ‹x∈X› have "ℳ`(x) ∈ Pow(Pow(X))" using apply_funtype by blast
with ‹N∈ℳ`(x)› show "N⊆X" by blast
from assms show "x∈N" using IsNeighSystem_def by simp
qed
text‹Some sources (like Wikipedia) use a bit different definition of neighborhood systems
where the $U$ is required to be contained in $N$. The next lemma shows that this stronger version
can be recovered from our definition. ›
lemma neigh_def_stronger:
assumes "ℳ {is a neighborhood system on} X" and "x∈X" and "N∈ℳ`(x)"
shows "∃U∈ℳ`(x).U⊆N ∧ (∀y∈U.(N∈ℳ`(y)))"
proof -
from assms obtain W where "W∈ℳ`(x)" and areNeigh:"∀y∈W.(N∈ℳ`(y))"
using IsNeighSystem_def by blast
let ?U = "N∩W"
from assms ‹W∈ℳ`(x)› have "?U ∈ ℳ`(x)"
unfolding IsNeighSystem_def IsFilter_def by blast
moreover have "?U⊆N" by blast
moreover from areNeigh have "∀y∈?U.(N∈ℳ`(y))" by auto
ultimately show ?thesis by auto
qed
subsection‹ Topology from neighborhood systems ›
text‹Given a neighborhood system $\{\mathcal{M}_x\}_{x\in X}$ we can define a topology on $X$.
Namely, we consider a subset of $X$ open if $U \in \mathcal{M}_x$ for every element $x$ of $U$. ›
text‹ The collection of sets defined as above is indeed a topology. ›
theorem topology_from_neighs:
assumes "ℳ {is a neighborhood system on} X"
defines Tdef: "T ≡ {U∈Pow(X). ∀x∈U. U ∈ ℳ`(x)}"
shows "T {is a topology}" and "⋃T = X"
proof -
{ fix 𝔘 assume "𝔘 ∈ Pow(T)"
have "⋃𝔘 ∈ T"
proof -
from ‹𝔘 ∈ Pow(T)› Tdef have "⋃𝔘 ∈ Pow(X)" by blast
moreover
{ fix x assume "x ∈ ⋃𝔘"
then obtain U where "U∈𝔘" and "x∈U" by blast
with assms ‹𝔘 ∈ Pow(T)›
have "U ∈ ℳ`(x)" and "U ⊆ ⋃𝔘" and "ℳ`(x) {is a filter on} X"
unfolding IsNeighSystem_def by auto
with ‹⋃𝔘 ∈ Pow(X)› have "⋃𝔘 ∈ ℳ`(x)" unfolding IsFilter_def
by simp
}
ultimately show "⋃𝔘 ∈ T" using Tdef by blast
qed
}
moreover
{ fix U V assume "U∈T" and "V∈T"
have "U∩V ∈ T"
proof -
from Tdef ‹U∈T› ‹U∈T› have "U∩V ∈ Pow(X)" by auto
moreover
{ fix x assume "x ∈ U∩V"
with assms ‹U∈T› ‹V∈T› Tdef have "U ∈ ℳ`(x)" "V ∈ ℳ`(x)" and "ℳ`(x) {is a filter on} X"
unfolding IsNeighSystem_def by auto
then have "U∩V ∈ ℳ`(x)" unfolding IsFilter_def by simp
}
ultimately show "U∩V ∈T" using Tdef by simp
qed
}
ultimately show "T {is a topology}" unfolding IsATopology_def by blast
from assms show "⋃T = X" unfolding IsNeighSystem_def IsFilter_def by blast
qed
text‹ Some sources (like Wikipedia) define the open sets generated by a neighborhood system
"as those sets containing a neighborhood of each of their points". The next lemma shows that
this definition is equivalent to the one we are using.›
lemma topology_from_neighs1:
assumes "ℳ {is a neighborhood system on} X"
shows "{U∈Pow(X). ∀x∈U. U ∈ ℳ`(x)} = {U∈Pow(X). ∀x∈U. ∃V ∈ ℳ`(x). V⊆U}"
proof
let ?T = "{U∈Pow(X). ∀x∈U. U ∈ ℳ`(x)}"
let ?S = "{U∈Pow(X). ∀x∈U. ∃V ∈ ℳ`(x). V⊆U}"
show "?S⊆?T"
proof -
{ fix U assume "U∈?S"
then have "U∈Pow(X)" by simp
moreover
from assms ‹U∈?S› ‹U∈Pow(X)› have "∀x∈U. U ∈ ℳ`(x)"
unfolding IsNeighSystem_def IsFilter_def by blast
ultimately have "U∈?T" by auto
} thus ?thesis by auto
qed
show "?T⊆?S" by auto
qed
subsection‹ Neighborhood system from topology ›
text‹ Once we have a topology $T$ we can define a natural neighborhood system on $X=\bigcup T$.
In this section we define such neighborhood system and prove its basic properties. ›
text‹For a topology $T$ we define a neighborhood system of $T$ as a function that takes an $x\in X=\bigcup T$
and assigns it a collection supersets of open sets containing $x$.
We call that the "neighborhood system of $T$"›
definition
NeighSystem ("{neighborhood system of} _" 91)
where "{neighborhood system of} T ≡ { ⟨x,{V∈Pow(⋃T).∃U∈T.(x∈U ∧ U⊆V)}⟩. x ∈ ⋃T }"
text‹ The next lemma shows that open sets are members of (what we will prove later to be) the natural
neighborhood system on $X=\bigcup T$. ›
lemma open_are_neighs:
assumes "U∈T" "x∈U"
shows "x ∈ ⋃T" and "U ∈ {V∈Pow(⋃T).∃U∈T.(x∈U ∧ U⊆V)}"
using assms by auto
text‹ Another fact we will need is that for every $x\in X=\bigcup T$ the neighborhoods of $x$
form a filter ›
lemma neighs_is_filter:
assumes "T {is a topology}" and "x ∈ ⋃T"
defines Mdef: "ℳ ≡ {neighborhood system of} T"
shows "ℳ`(x) {is a filter on} (⋃T)"
proof -
let ?X = "⋃T"
let ?𝔉 = "{V∈Pow(?X).∃U∈T.(x∈U ∧ U⊆V)}"
have "0∉?𝔉" by blast
moreover have "?X∈?𝔉"
proof -
from assms ‹x∈?X› have "?X ∈ Pow(?X)" "?X∈T" and "x∈?X ∧ ?X⊆?X" using carr_open
by auto
hence "∃U∈T.(x∈U ∧ U⊆?X)" by auto
thus ?thesis by auto
qed
moreover have "∀A∈?𝔉. ∀B∈?𝔉. A∩B ∈ ?𝔉"
proof -
{ fix A B assume "A∈?𝔉" "B∈?𝔉"
then obtain U⇩A U⇩B where "U⇩A∈T" "x∈U⇩A" "U⇩A⊆A" "U⇩B∈T" "x∈U⇩B" "U⇩B⊆B"
by auto
with ‹T {is a topology}› ‹A∈?𝔉› ‹B∈?𝔉› have "A∩B ∈ Pow(?X)" and
"U⇩A∩U⇩B ∈ T" "x ∈ U⇩A∩U⇩B" "U⇩A∩U⇩B ⊆ A∩B" using IsATopology_def
by auto
hence "A∩B ∈ ?𝔉" by blast
} thus ?thesis by blast
qed
moreover have "∀B∈?𝔉. ∀C∈Pow(?X). B⊆C ⟶ C∈?𝔉"
proof -
{ fix B C assume "B∈?𝔉" "C ∈ Pow(?X)" "B⊆C"
then obtain U where "U∈T" and "x∈U" "U⊆B" by blast
with ‹C ∈ Pow(?X)› ‹B⊆C› have "C∈?𝔉" by blast
} thus ?thesis by auto
qed
ultimately have "?𝔉 {is a filter on} ?X" unfolding IsFilter_def by blast
with Mdef ‹x∈?X› show "ℳ`(x) {is a filter on} ?X" using ZF_fun_from_tot_val1 NeighSystem_def
by simp
qed
text‹ The next theorem states that the the natural
neighborhood system on $X=\bigcup T$ indeed is a neighborhood system. ›
theorem neigh_from_topology:
assumes "T {is a topology}"
shows "({neighborhood system of} T) {is a neighborhood system on} (⋃T)"
proof -
let ?X = "⋃T"
let ?ℳ = "{neighborhood system of} T"
have "?ℳ : ?X→Pow(Pow(?X))"
proof -
{ fix x assume "x∈?X"
hence "{V∈Pow(⋃T).∃U∈T.(x∈U ∧ U⊆V)} ∈ Pow(Pow(?X))" by auto
} hence "∀x∈?X. {V∈Pow(⋃T).∃U∈T.(x∈U ∧ U⊆V)} ∈ Pow(Pow(?X))" by auto
then show ?thesis using ZF_fun_from_total NeighSystem_def by simp
qed
moreover from assms have "∀x∈?X. (?ℳ`(x) {is a filter on} ?X)"
using neighs_is_filter NeighSystem_def by auto
moreover have "∀x∈?X. ∀N∈?ℳ`(x). x∈N ∧ (∃U∈?ℳ`(x).∀y∈U.(N∈?ℳ`(y)))"
proof -
{ fix x N assume "x∈?X" "N ∈ ?ℳ`(x)"
let ?𝔉 = "{V∈Pow(?X).∃U∈T.(x∈U ∧ U⊆V)}"
from ‹x∈?X› have "?ℳ`(x) = ?𝔉" using ZF_fun_from_tot_val1 NeighSystem_def
by simp
with ‹N ∈ ?ℳ`(x)› have "N∈?𝔉" by simp
hence "x∈N" by blast
from ‹N∈?𝔉› obtain U where "U∈T" "x∈U" and "U⊆N" by blast
with ‹N∈?𝔉› ‹?ℳ`(x) = ?𝔉› have "U ∈ ?ℳ`(x)" by auto
moreover from assms ‹U∈T› ‹U⊆N› ‹N∈?𝔉› have "∀y∈U.(N ∈ ?ℳ`(y))"
using ZF_fun_from_tot_val1 open_are_neighs neighs_is_filter
NeighSystem_def IsFilter_def by auto
ultimately have "∃U∈?ℳ`(x).∀y∈U.(N∈?ℳ`(y))" by blast
with ‹x∈N› have "x∈N ∧ (∃U∈?ℳ`(x).∀y∈U.(N∈?ℳ`(y)))" by simp
} thus ?thesis by auto
qed
ultimately show ?thesis unfolding IsNeighSystem_def by blast
qed
end