Theory Topology_ZF_4a
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‹ From a neighborhood system to topology ›
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‹From a topology to a neighborhood system›
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 the collection of 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,{N∈Pow(⋃T).∃U∈T.(x∈U ∧ U⊆N)}⟩. x ∈ ⋃T }"
text‹The way we defined the neighborhood system of $T$ means that
it is a function on $\bigcup T$. ›
lemma neigh_fun: shows "({neighborhood system of} T): ⋃T → Pow(Pow(⋃T))"
proof -
let ?X = "⋃T"
have "∀x∈?X. {N∈Pow(?X).∃U∈T.(x∈U ∧ U⊆N)} ∈ Pow(Pow(?X))"
by blast
then show ?thesis unfolding NeighSystem_def using ZF_fun_from_total
by simp
qed
text‹The value of the neighborhood system of $T$ at $x\in \bigcup T$
is the collection of supersets of open sets containing $x$.›
lemma neigh_val: assumes "x∈⋃T"
shows "({neighborhood system of} T)`(x) = {N∈Pow(⋃T).∃U∈T.(x∈U ∧ U⊆N)}"
using assms ZF_fun_from_tot_val1 unfolding NeighSystem_def
by simp
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
text‹Any neighborhood of an element of the closure of a subset intersects the subset.›
lemma neigh_inter_nempty:
assumes "T {is a topology}" "A⊆⋃T" "x ∈ Closure(A,T)" and
"N ∈ ({neighborhood system of} T)`(x)"
shows "N∩A ≠ 0"
proof -
let ?X = "⋃T"
from assms(1) have cntx: "topology0(T)"
unfolding topology0_def by simp
with assms(2,3) have "x∈?X"
using topology0.Top_3_L11(1) by blast
with assms(4) obtain U where "U∈T" "x∈U" and "U⊆N"
using neigh_val by auto
from assms(2,3) cntx ‹U∈T› ‹x∈U› have "A∩U ≠ 0"
using topology0.cl_inter_neigh by simp
with ‹U⊆N› show "N∩A ≠ 0" by blast
qed
subsection‹ Neighborhood systems are 1:1 with topologies ›
text‹We can create a topology from a neighborhood system and neighborhood system from topology.
The question is then if we start from a neighborhood system, create a topology from it
then create the topology's natural neighborhood system, do we get back the neighborhood system
we started from? Similarly, if we start from a topology, create its neighborhood system and then
create a topology from that, do we get the original topology? This section provides
the affirmative answer (for now only for the first question).
This means that there is a one-to-one correspondence between the set of topologies on a set
and the set of abstract neighborhood systems on the set. ›
text‹Each abstract neighborhood of $x$ contains an open neighborhood of $x$.›
lemma open_nei_in_nei:
assumes "ℳ {is a neighborhood system on} X" "x∈X" "N∈ℳ`(x)"
defines Tdef: "T ≡ {U∈Pow(X). ∀x∈U. U ∈ ℳ`(x)}"
shows "N∈Pow(X)" and "∃U∈T. (x∈U ∧ U⊆N)"
proof -
from assms(1) have "ℳ:X→Pow(Pow(X))" unfolding IsNeighSystem_def
by simp
with assms(2,3) show "N∈Pow(X)"using apply_funtype by blast
let ?U = "{y∈X. N ∈ ℳ`(y)}"
have "?U∈T"
proof -
have "?U ∈ Pow(X)" by auto
moreover have "∀y∈?U. ?U∈ℳ`(y)"
proof -
{ fix y assume "y∈?U"
then have "y∈X" and "N∈ℳ`(y)" by auto
with assms(1) obtain V where "V∈ℳ`(y)" and "∀z∈V. N ∈ ℳ`(z)"
unfolding IsNeighSystem_def by blast
with assms(1) ‹y∈X› ‹V∈ℳ`(y)› have "V⊆?U"
using neighborhood_subset(1) by blast
with assms(1) ‹y∈X› ‹V∈ℳ`(y)› ‹?U ∈ Pow(X)› have "?U∈ℳ`(y)"
unfolding IsNeighSystem_def using is_filter_def_split(5) by blast
} thus ?thesis by simp
qed
ultimately have "?U ∈ {U∈Pow(X). ∀x∈U. U ∈ ℳ`(x)}" by simp
with assms(4) show "?U∈T" by simp
qed
moreover from assms(1,2) ‹N∈ℳ`(x)› have "x∈?U ∧ ?U ⊆ N"
using neighborhood_subset(2) by auto
ultimately show "∃U∈T. (x∈U ∧ U⊆N)" by (rule witness_exists)
qed
text‹In the the next theorem we show that if we start from
a neighborhood system, create a topology from it, then create it's natural neighborhood system,
we get back the original neighborhood system.›
theorem nei_top_nei_round_trip:
assumes "ℳ {is a neighborhood system on} X"
defines Tdef: "T ≡ {U∈Pow(X). ∀x∈U. U ∈ ℳ`(x)}"
shows "({neighborhood system of} T) = ℳ"
proof -
let ?M = "{neighborhood system of} T"
from assms have "T {is a topology}" and "⋃T = X" using topology_from_neighs
by auto
then have "?M {is a neighborhood system on} X" using neigh_from_topology
by blast
with assms(1) have "?M:X→Pow(Pow(X))" and "ℳ:X→Pow(Pow(X))"
unfolding IsNeighSystem_def by auto
moreover
{ fix x assume "x∈X"
from ‹⋃T = X› ‹x∈X› have I: "?M`(x) = {V∈Pow(X).∃U∈T.(x∈U ∧ U⊆V)}"
unfolding NeighSystem_def using ZF_fun_from_tot_val1 by simp
have "?M`(x) = ℳ`(x)"
proof
{ fix V assume "V∈?M`(x)"
with I obtain U where "U∈T" "x∈U" "U⊆V" by auto
from assms(2) ‹U∈T› ‹x∈U› have "U ∈ ℳ`(x)" by simp
from assms(1) ‹x∈X› have "ℳ`(x) {is a filter on} X"
unfolding IsNeighSystem_def by simp
with ‹U ∈ ℳ`(x)› ‹V∈?M`(x)› I ‹U⊆V› have "V ∈ ℳ`(x)"
unfolding IsFilter_def by simp
} thus "?M`(x) ⊆ ℳ`(x)" by auto
{ fix N assume "N∈ℳ`(x)"
with assms ‹x∈X› ‹⋃T = X› I have "N∈?M`(x)" using open_nei_in_nei
by auto
} thus "ℳ`(x) ⊆ ?M`(x)" by auto
qed
} hence "∀x∈X. ?M`(x) = ℳ`(x)" by simp
ultimately show ?thesis by (rule func_eq)
qed
subsection‹Set neighborhoods›
text‹Some sources (like Metamath) take a somewhat different approach where instead of defining
the collection of neighborhoods of a point $x\in X$ they define a collection of neighborhoods
of a subset of $X$ (where $X$ is the carrier of a topology $T$ (i.e. $X=\bigcup T$).
In this approach a neighborhood system is a function whose domain is the powerset of $X$, i.e.
the set of subsets of $X$. The two approaches are equivalent in a sense as
having a neighborhood system we can create a set neighborhood system and vice versa. ›
text‹We define a set neighborhood system as a function that takes a subset $A$ of the carrier of the
topology and assigns it the collection of supersets of all open sets that contain $A$. ›
definition
SetNeighSystem ( "{set neighborhood system of} _" 91)
where "{set neighborhood system of} T
≡ {⟨A,{N∈Pow(⋃T). ∃U∈T. (A⊆U ∧ U⊆N)}⟩. A∈Pow(⋃T)}"
text‹Given a set neighborhood system we can recover the (standard)
neighborhood system by taking the values of the set neighborhood system
at singletons ${x}$ where $x\in X=\bigcup T$.›
lemma neigh_from_nei: assumes "x∈⋃T"
shows "({neighborhood system of} T)`(x) = ({set neighborhood system of} T)`{x}"
using assms ZF_fun_from_tot_val1
unfolding NeighSystem_def SetNeighSystem_def
by simp
text‹The set neighborhood system of $T$ is a function mapping subsets of $\bigcup T$
to collections of subsets of $\bigcup T$. ›
lemma nei_fun:
shows "({set neighborhood system of} T):Pow(⋃T) →Pow(Pow(⋃T))"
proof -
let ?X = "⋃T"
have "∀A∈Pow(?X). {N∈Pow(?X). ∃U∈T. (A⊆U ∧ U⊆N)} ∈ Pow(Pow(?X))"
by blast
then have
"{⟨A,{N∈Pow(?X). ∃U∈T. (A⊆U ∧ U⊆N)}⟩. A∈Pow(?X)}:Pow(?X)→Pow(Pow(?X))"
by (rule ZF_fun_from_total)
then show ?thesis unfolding SetNeighSystem_def by simp
qed
text‹The value of the set neighborhood system of $T$ at subset $A$ of $\bigcup T$
is the collection of subsets $N$ of $\bigcup T$ for which exists an open subset
$U\subseteq N$ that contains $A$. ›
lemma nei_val: assumes "A ⊆ ⋃T"
shows
"({set neighborhood system of} T)`(A) = {N∈Pow(⋃T). ∃U∈T. (A⊆U ∧ U⊆N)}"
using assms ZF_fun_from_tot_val1 unfolding SetNeighSystem_def by simp
text‹A member of the value of the set neighborhood system of $T$ at $A$ is
a subset of $\bigcup T$. The interesting part is that we can show it without any
assumption on $A$. ›
lemma nei_val_subset:
assumes "N ∈ ({set neighborhood system of} T)`(A)"
shows "A ⊆ ⋃T" and "N ⊆ ⋃T"
proof -
let ?f = "{set neighborhood system of} T"
have "?f:Pow(⋃T) →Pow(Pow(⋃T))" using nei_fun by simp
with assms show "A ⊆ ⋃T" using arg_in_domain by blast
with assms show "N ⊆ ⋃T" using nei_val by simp
qed
text‹If $T$ is a topology, then every subset of its carrier (i.e. $\bigcup T$)
is a (set) neighborhood of the empty set. ›
lemma nei_empty: assumes "T {is a topology}" "N ⊆ ⋃T"
shows "N ∈ ({set neighborhood system of} T)`(0)"
using assms empty_open nei_val by auto
text‹If $T$ is a topology, then the (set) neighborhoods of a nonempty subset of
$\bigcup T$ form a filter on $X=\bigcup T$.›
theorem nei_filter: assumes "T {is a topology}" "D ⊆ (⋃T)" "D≠0"
shows "({set neighborhood system of} T)`(D) {is a filter on} (⋃T)"
proof -
let ?X = "⋃T"
let ?ℱ = "({set neighborhood system of} T)`(D)"
from assms(2) have I: "?ℱ = {N∈Pow(?X). ∃U∈T. (D⊆U ∧ U⊆N)}"
using nei_val by simp
with assms(3) have "0 ∉ ?ℱ" by auto
moreover from assms(1,2) I have "?X∈?ℱ"
using carr_open by auto
moreover from I have "?ℱ ⊆ Pow(?X)" by auto
moreover have "∀A∈?ℱ. ∀B∈?ℱ. A∩B ∈ ?ℱ"
proof -
{ fix A B assume "A∈?ℱ" "B∈?ℱ"
with I obtain U⇩A U⇩B where
"U⇩A∈T" "D⊆U⇩A" "U⇩A⊆A" and "U⇩B∈T" "D⊆U⇩B" "U⇩B⊆B"
by auto
let ?U = "U⇩A∩U⇩B"
from assms(1) ‹U⇩A∈T› ‹U⇩B∈T› ‹D⊆U⇩A› ‹D⊆U⇩B› ‹U⇩A⊆A› ‹U⇩B⊆B›
have "?U ∈ T" "D⊆?U" "?U ⊆ A∩B"
unfolding IsATopology_def by auto
with I ‹A∈?ℱ› ‹B∈?ℱ› have "A∩B ∈ ?ℱ" by auto
} thus ?thesis by simp
qed
moreover have "∀B∈?ℱ. ∀C∈Pow(?X). B⊆C ⟶ C∈?ℱ"
proof -
{ fix B C assume "B∈?ℱ" "C∈Pow(?X)" "B⊆C"
from I ‹B∈?ℱ› obtain U where "U∈T" "D⊆U" and "U⊆B"
by auto
with ‹B⊆C› have "∃U∈T. (D⊆U ∧ U⊆C)" by blast
with I ‹C∈Pow(?X)› have "C∈?ℱ" by simp
} thus ?thesis by blast
qed
ultimately show "?ℱ {is a filter on} ?X"
unfolding IsFilter_def by simp
qed
text‹If $N$ is a (set) neighborhood of $A$ in $T$, then exist an open set $U$ such that
$N$ contains $U$ which contains $A$. This is similar to the Metamath's theorem
with the same name, except that here we do not need assume that $T$ is a topology
(which is a bit worrying).›
lemma neii2: assumes "N ∈ ({set neighborhood system of} T)`(A)"
shows "∃U∈T. (A⊆U ∧ U⊆N)"
proof -
from assms have "A∈Pow(⋃T)" using nei_fun arg_in_domain
by blast
with assms show ?thesis
unfolding SetNeighSystem_def using ZF_fun_from_tot_val1
by simp
qed
text‹An open set $U$ covering a set $A$ is a set neighborhood of $A$. ›
lemma open_superset_nei: assumes "V∈T" "A⊆V"
shows "V ∈ ({set neighborhood system of} T)`(A)"
proof -
from assms have
"({set neighborhood system of} T)`(A) = {N∈Pow(⋃T). ∃U∈T. (A⊆U ∧ U⊆N)}"
using nei_val by blast
with assms show ?thesis by auto
qed
text‹An open set is a set neighborhood of itself.›
corollary open_is_nei: assumes "V∈T"
shows "V ∈ ({set neighborhood system of} T)`(V)"
using assms open_superset_nei by simp
text‹An open neighborhood of $x$ is a set neighborhood of $\{ x\}$. ›
corollary open_nei_singl: assumes "V∈T" "x∈V"
shows "V ∈ ({set neighborhood system of} T)`{x}"
using assms open_superset_nei by simp
text‹The Cartesian product of two neighborhoods is a neighborhood in the
product topology. Similar to the Metamath's theorem with the same name. ›
lemma neitx:
assumes "T {is a topology}" "S {is a topology}" and
"A ∈ ({set neighborhood system of} T)`(C)" and
"B ∈ ({set neighborhood system of} S)`(D)"
shows "A×B ∈ ({set neighborhood system of} (T×⇩tS))`(C×D)"
proof -
have "A×B ⊆ ⋃(T×⇩tS)"
proof -
from assms(3,4) have "A×B ⊆ (⋃T)×(⋃S)"
using nei_val_subset(2) by blast
with assms(1,2) show ?thesis using Top_1_4_T1 by simp
qed
let ?ℱ = "({set neighborhood system of} (T×⇩tS))`(C×D)"
{ assume "C=0 ∨ D=0"
with assms(1,2) ‹A×B ⊆ ⋃(T×⇩tS)› have "A×B ∈ ?ℱ"
using Top_1_4_T1(1) nei_empty by auto
}
moreover
{ assume "C≠0" "D≠0"
from assms(3) obtain U⇩A where
"U⇩A∈T" "C⊆U⇩A" "U⇩A⊆A" using neii2 by blast
from assms(4) obtain U⇩B where
"U⇩B∈S" "D⊆U⇩B" "U⇩B⊆B" using neii2 by blast
from assms(1,2) ‹U⇩A∈T› ‹U⇩B∈S› ‹C⊆U⇩A› ‹D⊆U⇩B›
have "U⇩A×U⇩B ∈ T×⇩tS" and "C×D ⊆ U⇩A×U⇩B"
using prod_open_open_prod by auto
then have "U⇩A×U⇩B ∈ ?ℱ" using open_superset_nei
by simp
from ‹U⇩A⊆A› ‹U⇩B⊆B› have "U⇩A×U⇩B ⊆ A×B" by auto
have "?ℱ {is a filter on} (⋃(T×⇩tS))"
proof -
from assms(1,2) have "(T×⇩tS) {is a topology}"
using Top_1_4_T1(1) by simp
moreover have "C×D ⊆ ⋃(T×⇩tS)"
proof -
from assms(3,4) have "C×D ⊆ (⋃T)×(⋃S)"
using nei_val_subset(1) by blast
with assms(1,2) show ?thesis using Top_1_4_T1(3) by simp
qed
moreover from ‹C≠0› ‹D≠0› have "C×D ≠ 0" by auto
ultimately show "?ℱ {is a filter on} (⋃(T×⇩tS))"
using nei_filter by simp
qed
with ‹U⇩A×U⇩B ∈ ?ℱ› ‹A×B ⊆ ⋃(T×⇩tS)› ‹U⇩A×U⇩B ⊆ A×B›
have "A×B ∈ ?ℱ" using is_filter_def_split(5) by simp
}
ultimately show ?thesis by auto
qed
text‹Any neighborhood of an element of the closure of a subset intersects the subset.
This is practically the same as ‹neigh_inter_nempty›, just formulated in terms
of set neighborhoods of singletons.
Compare with Metamath's theorem with the same name.›
lemma neindisj: assumes "T {is a topology}" "A⊆⋃T" "x ∈ Closure(A,T)" and
"N ∈ ({set neighborhood system of} T)`{x}"
shows "N∩A ≠ 0"
proof -
let ?X = "⋃T"
from assms(1) have cntx: "topology0(T)"
unfolding topology0_def by simp
with assms(2,3) have "x∈?X"
using topology0.Top_3_L11(1) by blast
with assms show ?thesis using neigh_from_nei neigh_inter_nempty
by simp
qed
end