(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2019-2022 Slawomir Kolodynski This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) 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×⇩_{t}S))`(C×D)" proof - have "A×B ⊆ ⋃(T×⇩_{t}S)" 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×⇩_{t}S))`(C×D)" { assume "C=0 ∨ D=0" with assms(1,2) ‹A×B ⊆ ⋃(T×⇩_{t}S)› 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×⇩_{t}S" 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×⇩_{t}S))" proof - from assms(1,2) have "(T×⇩_{t}S) {is a topology}" using Top_1_4_T1(1) by simp moreover have "C×D ⊆ ⋃(T×⇩_{t}S)" 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×⇩_{t}S))" using nei_filter by simp qed with ‹U⇩_{A}×U⇩_{B}∈ ?ℱ› ‹A×B ⊆ ⋃(T×⇩_{t}S)› ‹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