(*

This file is a part of IsarMathLib -

a library of formalized mathematics written for Isabelle/Isar.

Copyright (C) 2005-2012 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.

*)

header{*\isaheader{Topology\_ZF.thy}*}

theory Topology_ZF imports ZF1 Finite_ZF Fol1

begin

text{* This theory file provides basic definitions and properties of topology,

open and closed sets, closure and boundary.*}

section{*Basic definitions and properties*}

text{*A typical textbook defines a topology on a set $X$ as a

collection $T$ of subsets

of $X$ such that $X\in T$, $\emptyset \in T$ and $T$ is closed

with respect to arbitrary unions and intersection of two sets. One can

notice here that since we always have $\bigcup T = X$, the set

on which the topology

is defined (the "carrier" of the topology) can always be constructed

from the topology itself and is

superfluous in the definition. Moreover, as Marnix Klooster pointed out to me,

the fact that the empty set is open can also be proven from other axioms.

Hence, we define a topology as

a collection of sets that is closed under

arbitrary unions and intersections of two sets, without any mention of the

set on which the topology is defined. Recall that @{text "Pow(T)"}

is the powerset of $T$, so that if $M\in$ @{text " Pow(T)"} then $M$

is a subset of $T$. The sets that belong to a topology $T$ will be sometimes called

''open in'' $T$ or just ''open'' if the topology is clear from the context.

*}

text{*Topology is a collection of sets that is closed under arbitrary unions and intersections

of two sets.*}

definition

IsATopology ("_ {is a topology}" [90] 91) where

"T {is a topology} ≡ ( ∀M ∈ Pow(T). \<Union>M ∈ T ) ∧

( ∀U∈T. ∀ V∈T. U∩V ∈ T)"

text{*We define interior of a set $A$ as the union of all open sets

contained in $A$. We use @{text "Interior(A,T)"} to denote the

interior of A.*}

definition

"Interior(A,T) ≡ \<Union> {U∈T. U ⊆ A}"

text{*A set is closed if it is contained in the carrier of topology

and its complement is open.*}

definition

IsClosed (infixl "{is closed in}" 90) where

"D {is closed in} T ≡ (D ⊆ \<Union>T ∧ \<Union>T - D ∈ T)"

text{*To prove various properties of closure we will often use

the collection of closed sets that contain a given set $A$.

Such collection does not have a separate

name in informal math. We will call it @{text "ClosedCovers(A,T)"}.

*}

definition

"ClosedCovers(A,T) ≡ {D ∈ Pow(\<Union>T). D {is closed in} T ∧ A⊆D}"

text{*The closure of a set $A$ is defined as the intersection of the collection

of closed sets that contain $A$.*}

definition

"Closure(A,T) ≡ \<Inter> ClosedCovers(A,T)"

text{*We also define boundary of a set as the intersection of

its closure with the closure of the complement (with respect to the

carrier).*}

definition

"Boundary(A,T) ≡ Closure(A,T) ∩ Closure(\<Union>T - A,T)"

text{* A set $K$ is compact if for every collection of open

sets that covers $K$ we can choose a finite one that still covers the set.

Recall that @{text "FinPow(M)"} is the collection of finite subsets of $M$

(finite powerset of $M$), defined in IsarMathLib's @{text "Finite_ZF"}

theory. *}

definition

IsCompact (infixl "{is compact in}" 90) where

"K {is compact in} T ≡ (K ⊆ \<Union>T ∧

(∀ M∈Pow(T). K ⊆ \<Union>M --> (∃ N ∈ FinPow(M). K ⊆ \<Union>N)))"

text{*A basic example of a topology: the powerset of any set is a topology.*}

lemma Pow_is_top: shows "Pow(X) {is a topology}"

proof -

have "∀A∈Pow(Pow(X)). \<Union>A ∈ Pow(X)" by fast

moreover have "∀U∈Pow(X). ∀V∈Pow(X). U∩V ∈ Pow(X)" by fast

ultimately show "Pow(X) {is a topology}" using IsATopology_def

by auto

qed;

text{*Empty set is open.*}

lemma empty_open:

assumes "T {is a topology}" shows "0 ∈ T"

proof -

have "0 ∈ Pow(T)" by simp

with assms have "\<Union>0 ∈ T" using IsATopology_def by blast

thus "0 ∈ T" by simp

qed

text{*Union of a collection of open sets is open.*}

lemma union_open: assumes "T {is a topology}" and "∀A∈\<A>. A ∈ T"

shows "(\<Union>\<A>) ∈ T" using assms IsATopology_def by auto

text{*Union of a indexed family of open sets is open.*}

lemma union_indexed_open: assumes A1: "T {is a topology}" and A2: "∀i∈I. P(i) ∈ T"

shows "(\<Union>i∈I. P(i)) ∈ T" using assms union_open by simp

text{*The intersection of any nonempty collection of topologies on a set $X$ is a topology.*}

lemma Inter_tops_is_top:

assumes A1: "\<M> ≠ 0" and A2: "∀T∈\<M>. T {is a topology}"

shows "(\<Inter>\<M>) {is a topology}"

proof -

{ fix A assume "A∈Pow(\<Inter>\<M>)"

with A1 have "∀T∈\<M>. A∈Pow(T)" by auto

with A1 A2 have "\<Union>A ∈ \<Inter>\<M>" using IsATopology_def

by auto

} then have "∀A. A∈Pow(\<Inter>\<M>) --> \<Union>A ∈ \<Inter>\<M>" by simp

hence "∀A∈Pow(\<Inter>\<M>). \<Union>A ∈ \<Inter>\<M>" by auto

moreover

{ fix U V assume "U ∈ \<Inter>\<M>" and "V ∈ \<Inter>\<M>"

then have "∀T∈\<M>. U ∈ T ∧ V ∈ T" by auto

with A1 A2 have "∀T∈\<M>. U∩V ∈ T" using IsATopology_def

by simp

} then have "∀ U ∈ \<Inter>\<M>. ∀ V ∈ \<Inter>\<M>. U∩V ∈ \<Inter>\<M>"

by auto

ultimately show "(\<Inter>\<M>) {is a topology}"

using IsATopology_def by simp

qed;

text{*We will now introduce some notation. In Isar, this is done by definining

a "locale". Locale is kind of a context that holds some assumptions and

notation used in all theorems proven in it. In the locale (context)

below called @{text "topology0"} we assume that $T$ is a topology.

The interior of the set $A$ (with respect to the topology in the context)

is denoted @{text "int(A)"}. The closure of a set $A\subseteq \bigcup T$ is

denoted @{text "cl(A)"} and the boundary is @{text "∂A"}.*}

locale topology0 =

fixes T

assumes topSpaceAssum: "T {is a topology}"

fixes int

defines int_def [simp]: "int(A) ≡ Interior(A,T)"

fixes cl

defines cl_def [simp]: "cl(A) ≡ Closure(A,T)"

fixes boundary ("∂_" [91] 92)

defines boundary_def [simp]: "∂A ≡ Boundary(A,T)"

text{*Intersection of a finite nonempty collection of open sets is open.*}

lemma (in topology0) fin_inter_open_open: assumes "N≠0" "N ∈ FinPow(T)"

shows "\<Inter>N ∈ T"

using topSpaceAssum assms IsATopology_def inter_two_inter_fin

by simp

text{*Having a topology $T$ and a set $X$ we can

define the induced topology

as the one consisting of the intersections of $X$ with sets from $T$.

The notion of a collection restricted to a set is defined in ZF1.thy.*}

lemma (in topology0) Top_1_L4:

shows "(T {restricted to} X) {is a topology}"

proof -

let ?S = "T {restricted to} X"

have "∀A∈Pow(?S). \<Union>A ∈ ?S"

proof

fix A assume A1: "A∈Pow(?S)"

have "∀V∈A. \<Union> {U ∈ T. V = U∩X} ∈ T"

proof -

{ fix V

let ?M = "{U ∈ T. V = U∩X}"

have "?M ∈ Pow(T)" by auto

with topSpaceAssum have "\<Union>?M ∈ T" using IsATopology_def by simp

} thus ?thesis by simp

qed

hence "{\<Union>{U∈T. V = U∩X}.V∈ A} ⊆ T" by auto

with topSpaceAssum have "(\<Union>V∈A. \<Union>{U∈T. V = U∩X}) ∈ T"

using IsATopology_def by auto

then have "(\<Union>V∈A. \<Union>{U∈T. V = U∩X})∩ X ∈ ?S"

using RestrictedTo_def by auto

moreover

from A1 have "∀V∈A. ∃U∈T. V = U∩X"

using RestrictedTo_def by auto

hence "(\<Union>V∈A. \<Union>{U∈T. V = U∩X})∩X = \<Union>A" by blast

ultimately show "\<Union>A ∈ ?S" by simp

qed

moreover have "∀U∈?S. ∀V∈?S. U∩V ∈ ?S"

proof -

{ fix U V assume "U∈?S" "V∈?S"

then obtain U⇩_{1}V⇩_{1}where

"U⇩_{1}∈ T ∧ U = U⇩_{1}∩X" and "V⇩_{1}∈ T ∧ V = V⇩_{1}∩X"

using RestrictedTo_def by auto

with topSpaceAssum have "U⇩_{1}∩V⇩_{1}∈ T" and "U∩V = (U⇩_{1}∩V⇩_{1})∩X"

using IsATopology_def by auto

then have " U∩V ∈ ?S" using RestrictedTo_def by auto

} thus "∀U∈?S. ∀ V∈?S. U∩V ∈ ?S"

by simp

qed

ultimately show "?S {is a topology}" using IsATopology_def

by simp

qed;

section{*Interior of a set*}

text{*In section we show basic properties of the interior of a set.*}

text{*Interior of a set $A$ is contained in $A$.*}

lemma (in topology0) Top_2_L1: shows "int(A) ⊆ A"

using Interior_def by auto

text{*Interior is open.*}

lemma (in topology0) Top_2_L2: shows "int(A) ∈ T"

proof -

have "{U∈T. U⊆A} ∈ Pow(T)" by auto

with topSpaceAssum show "int(A) ∈ T"

using IsATopology_def Interior_def by auto

qed

text{*A set is open iff it is equal to its interior.*}

lemma (in topology0) Top_2_L3: shows "U∈T <-> int(U) = U"

proof

assume "U∈T" then show "int(U) = U"

using Interior_def by auto

next assume A1: "int(U) = U"

have "int(U) ∈ T" using Top_2_L2 by simp

with A1 show "U∈T" by simp

qed

text{*Interior of the interior is the interior.*}

lemma (in topology0) Top_2_L4: shows "int(int(A)) = int(A)"

proof -

let ?U = "int(A)"

from topSpaceAssum have "?U∈T" using Top_2_L2 by simp

then show "int(int(A)) = int(A)" using Top_2_L3 by simp

qed

text{*Interior of a bigger set is bigger.*}

lemma (in topology0) interior_mono:

assumes A1: "A⊆B" shows "int(A) ⊆ int(B)"

proof -

from A1 have "∀ U∈T. (U⊆A --> U⊆B)" by auto

then show "int(A) ⊆ int(B)" using Interior_def by auto

qed

text{*An open subset of any set is a subset of the interior of that set.*}

lemma (in topology0) Top_2_L5: assumes "U⊆A" and "U∈T"

shows "U ⊆ int(A)"

using assms Interior_def by auto

text{*If a point of a set has an open neighboorhood contained in the set,

then the point belongs to the interior of the set.*}

lemma (in topology0) Top_2_L6: assumes "∃U∈T. (x∈U ∧ U⊆A)"

shows "x ∈ int(A)"

using assms Interior_def by auto

text{*A set is open iff its every point has a an open neighbourhood

contained in the set. We will formulate this statement as two lemmas

(implication one way and the other way).

The lemma below shows that if a set is open then every point has a

an open neighbourhood contained in the set.*}

lemma (in topology0) open_open_neigh:

assumes A1: "V∈T"

shows "∀x∈V. ∃U∈T. (x∈U ∧ U⊆V)"

proof -

from A1 have "∀x∈V. V∈T ∧ x ∈ V ∧ V ⊆ V" by simp

thus ?thesis by auto

qed

text{*If every point of a set has a an open neighbourhood

contained in the set then the set is open.*}

lemma (in topology0) open_neigh_open:

assumes A1: "∀x∈V. ∃U∈T. (x∈U ∧ U⊆V)"

shows "V∈T"

proof -

from A1 have "V = int(V)" using Top_2_L1 Top_2_L6

by blast

then show "V∈T" using Top_2_L3 by simp

qed

section{*Closed sets, closure, boundary.*}

text{*This section is devoted to closed sets and properties

of the closure and boundary operators.*}

text{* The carrier of the space is closed.*}

lemma (in topology0) Top_3_L1: shows "(\<Union>T) {is closed in} T"

proof -

have "\<Union>T - \<Union>T = 0" by auto

with topSpaceAssum have "\<Union>T - \<Union>T ∈ T" using IsATopology_def by auto

then show ?thesis using IsClosed_def by simp

qed

text{*Empty set is closed.*}

lemma (in topology0) Top_3_L2: shows "0 {is closed in} T"

using topSpaceAssum IsATopology_def IsClosed_def by simp

text{*The collection of closed covers of a subset of the carrier of topology

is never empty. This is good to know, as we want to intersect this collection

to get the closure.*}

lemma (in topology0) Top_3_L3:

assumes A1: "A ⊆ \<Union>T" shows "ClosedCovers(A,T) ≠ 0"

proof -

from A1 have "\<Union>T ∈ ClosedCovers(A,T)" using ClosedCovers_def Top_3_L1

by auto

thus ?thesis by auto

qed

text{*Intersection of a nonempty family of closed sets is closed. *}

lemma (in topology0) Top_3_L4: assumes A1: "K≠0" and

A2: "∀D∈K. D {is closed in} T"

shows "(\<Inter>K) {is closed in} T"

proof -

from A2 have I: "∀D∈K. (D ⊆ \<Union>T ∧ (\<Union>T - D)∈ T)"

using IsClosed_def by simp

then have "{\<Union>T - D. D∈ K} ⊆ T" by auto

with topSpaceAssum have "(\<Union> {\<Union>T - D. D∈ K}) ∈ T"

using IsATopology_def by auto

moreover from A1 have "\<Union> {\<Union>T - D. D∈ K} = \<Union>T - \<Inter>K" by fast

moreover from A1 I have "\<Inter>K ⊆ \<Union>T" by blast

ultimately show "(\<Inter>K) {is closed in} T" using IsClosed_def

by simp

qed

text{*The union and intersection of two closed sets are closed.*}

lemma (in topology0) Top_3_L5:

assumes A1: "D⇩_{1}{is closed in} T" "D⇩_{2}{is closed in} T"

shows

"(D⇩_{1}∩D⇩_{2}) {is closed in} T"

"(D⇩_{1}∪D⇩_{2}) {is closed in} T"

proof -

have "{D⇩_{1},D⇩_{2}} ≠ 0" by simp

with A1 have "(\<Inter> {D⇩_{1},D⇩_{2}}) {is closed in} T" using Top_3_L4

by fast

thus "(D⇩_{1}∩D⇩_{2}) {is closed in} T" by simp

from topSpaceAssum A1 have "(\<Union>T - D⇩_{1}) ∩ (\<Union>T - D⇩_{2}) ∈ T"

using IsClosed_def IsATopology_def by simp

moreover have "(\<Union>T - D⇩_{1}) ∩ (\<Union>T - D⇩_{2}) = \<Union>T - (D⇩_{1}∪ D⇩_{2})"

by auto

moreover from A1 have "D⇩_{1}∪ D⇩_{2}⊆ \<Union>T" using IsClosed_def

by auto

ultimately show "(D⇩_{1}∪D⇩_{2}) {is closed in} T" using IsClosed_def

by simp

qed

text{*Finite union of closed sets is closed. To understand the proof

recall that $D\in$@{text "Pow(\<Union>T)"} means

that $D$ is a subset of the carrier of the topology.*}

lemma (in topology0) fin_union_cl_is_cl:

assumes

A1: "N ∈ FinPow({D∈Pow(\<Union>T). D {is closed in} T})"

shows "(\<Union>N) {is closed in} T"

proof -

let ?C = "{D∈Pow(\<Union>T). D {is closed in} T}"

have "0∈?C" using Top_3_L2 by simp

moreover have "∀A∈?C. ∀B∈?C. A∪B ∈ ?C"

using Top_3_L5 by auto

moreover note A1

ultimately have "\<Union>N ∈ ?C" by (rule union_two_union_fin)

thus "(\<Union>N) {is closed in} T" by simp

qed

text{*Closure of a set is closed.*}

lemma (in topology0) cl_is_closed: assumes "A ⊆ \<Union>T"

shows "cl(A) {is closed in} T"

using assms Closure_def Top_3_L3 ClosedCovers_def Top_3_L4

by simp

text{*Closure of a bigger sets is bigger.*}

lemma (in topology0) top_closure_mono:

assumes A1: "A ⊆ \<Union>T" "B ⊆ \<Union>T" and A2:"A⊆B"

shows "cl(A) ⊆ cl(B)"

proof -

from A2 have "ClosedCovers(B,T)⊆ ClosedCovers(A,T)"

using ClosedCovers_def by auto

with A1 show ?thesis using Top_3_L3 Closure_def by auto

qed

text{*Boundary of a set is closed.*}

lemma (in topology0) boundary_closed:

assumes A1: "A ⊆ \<Union>T" shows "∂A {is closed in} T"

proof -

from A1 have "\<Union>T - A ⊆ \<Union>T" by fast

with A1 show "∂A {is closed in} T"

using cl_is_closed Top_3_L5 Boundary_def by auto

qed

text{*A set is closed iff it is equal to its closure.*}

lemma (in topology0) Top_3_L8: assumes A1: "A ⊆ \<Union>T"

shows "A {is closed in} T <-> cl(A) = A"

proof

assume "A {is closed in} T"

with A1 show "cl(A) = A"

using Closure_def ClosedCovers_def by auto

next assume "cl(A) = A"

then have "\<Union>T - A = \<Union>T - cl(A)" by simp

with A1 show "A {is closed in} T" using cl_is_closed IsClosed_def

by simp

qed

text{*Complement of an open set is closed.*}

lemma (in topology0) Top_3_L9:

assumes A1: "A∈T"

shows "(\<Union>T - A) {is closed in} T"

proof -

from topSpaceAssum A1 have "\<Union>T - (\<Union>T - A) = A" and "\<Union>T - A ⊆ \<Union>T"

using IsATopology_def by auto

with A1 show "(\<Union>T - A) {is closed in} T" using IsClosed_def by simp

qed

text{*A set is contained in its closure.*}

lemma (in topology0) cl_contains_set: assumes "A ⊆ \<Union>T" shows "A ⊆ cl(A)"

using assms Top_3_L1 ClosedCovers_def Top_3_L3 Closure_def by auto

text{*Closure of a subset of the carrier is a subset of the carrier and closure

of the complement is the complement of the interior.*}

lemma (in topology0) Top_3_L11: assumes A1: "A ⊆ \<Union>T"

shows

"cl(A) ⊆ \<Union>T"

"cl(\<Union>T - A) = \<Union>T - int(A)"

proof -

from A1 show "cl(A) ⊆ \<Union>T" using Top_3_L1 Closure_def ClosedCovers_def

by auto

from A1 have "\<Union>T - A ⊆ \<Union>T - int(A)" using Top_2_L1

by auto

moreover have I: "\<Union>T - int(A) ⊆ \<Union>T" "\<Union>T - A ⊆ \<Union>T" by auto

ultimately have "cl(\<Union>T - A) ⊆ cl(\<Union>T - int(A))"

using top_closure_mono by simp

moreover

from I have "(\<Union>T - int(A)) {is closed in} T"

using Top_2_L2 Top_3_L9 by simp

with I have "cl((\<Union>T) - int(A)) = \<Union>T - int(A)"

using Top_3_L8 by simp

ultimately have "cl(\<Union>T - A) ⊆ \<Union>T - int(A)" by simp

moreover

from I have "\<Union>T - A ⊆ cl(\<Union>T - A)" using cl_contains_set by simp

hence "\<Union>T - cl(\<Union>T - A) ⊆ A" and "\<Union>T - A ⊆ \<Union>T" by auto

then have "\<Union>T - cl(\<Union>T - A) ⊆ int(A)"

using cl_is_closed IsClosed_def Top_2_L5 by simp

hence "\<Union>T - int(A) ⊆ cl(\<Union>T - A)" by auto

ultimately show "cl(\<Union>T - A) = \<Union>T - int(A)" by auto

qed

text{*Boundary of a set is the closure of the set

minus the interior of the set.*}

lemma (in topology0) Top_3_L12: assumes A1: "A ⊆ \<Union>T"

shows "∂A = cl(A) - int(A)"

proof -

from A1 have "∂A = cl(A) ∩ (\<Union>T - int(A))"

using Boundary_def Top_3_L11 by simp

moreover from A1 have

"cl(A) ∩ (\<Union>T - int(A)) = cl(A) - int(A)"

using Top_3_L11 by blast

ultimately show "∂A = cl(A) - int(A)" by simp

qed

text{*If a set $A$ is contained in a closed set $B$, then the closure of $A$

is contained in $B$.*}

lemma (in topology0) Top_3_L13:

assumes A1: "B {is closed in} T" "A⊆B"

shows "cl(A) ⊆ B"

proof -

from A1 have "B ⊆ \<Union>T" using IsClosed_def by simp

with A1 show "cl(A) ⊆ B" using ClosedCovers_def Closure_def by auto

qed

(*text{*If two open sets are disjoint, then we can close one of them

and they will still be disjoint.*}

lemma (in topology0) open_disj_cl_disj:

assumes A1: "U∈T" "V∈T" and A2: "U∩V = 0"

shows "cl(U) ∩ V = 0"

proof -

from topSpaceAssum A1 have I: "U ⊆ \<Union>T" using IsATopology_def

by auto

with A2 have "U ⊆ \<Union>T - V" by auto

moreover from A1 have "(\<Union>T - V) {is closed in} T" using Top_3_L9

by simp

ultimately have "cl(U) - (\<Union>T - V) = 0"

using Top_3_L13 by blast

moreover

from I have "cl(U) ⊆ \<Union>T" using cl_is_closed IsClosed_def by simp

then have "cl(U) -(\<Union>T - V) = cl(U) ∩ V" by auto

ultimately show "cl(U) ∩ V = 0" by simp

qed;*)

text{*If a set is disjoint with an open set, then we can close it

and it will still be disjoint.*}

lemma (in topology0) disj_open_cl_disj:

assumes A1: "A ⊆ \<Union>T" "V∈T" and A2: "A∩V = 0"

shows "cl(A) ∩ V = 0"

proof -

from assms have "A ⊆ \<Union>T - V" by auto

moreover from A1 have "(\<Union>T - V) {is closed in} T" using Top_3_L9 by simp

ultimately have "cl(A) - (\<Union>T - V) = 0"

using Top_3_L13 by blast

moreover from A1 have "cl(A) ⊆ \<Union>T" using cl_is_closed IsClosed_def by simp

then have "cl(A) -(\<Union>T - V) = cl(A) ∩ V" by auto

ultimately show ?thesis by simp

qed

text{*A reformulation of @{text "disj_open_cl_disj"}:

If a point belongs to the closure of a set, then we can find a point

from the set in any open neighboorhood of the point.*}

lemma (in topology0) cl_inter_neigh:

assumes "A ⊆ \<Union>T" and "U∈T" and "x ∈ cl(A) ∩ U"

shows "A∩U ≠ 0" using assms disj_open_cl_disj by auto

text{*A reverse of @{text "cl_inter_neigh"}: if every open neiboorhood of a point

has a nonempty intersection with a set, then that point belongs to the closure

of the set.*}

lemma (in topology0) inter_neigh_cl:

assumes A1: "A ⊆ \<Union>T" and A2: "x∈\<Union>T" and A3: "∀U∈T. x∈U --> U∩A ≠ 0"

shows "x ∈ cl(A)"

proof -

{ assume "x ∉ cl(A)"

with A1 obtain D where "D {is closed in} T" and "A⊆D" and "x∉D"

using Top_3_L3 Closure_def ClosedCovers_def by auto

let ?U = "(\<Union>T) - D"

from A2 `D {is closed in} T` `x∉D` `A⊆D` have "?U∈T" "x∈?U" and "?U∩A = 0"

unfolding IsClosed_def by auto

with A3 have False by auto

} thus ?thesis by auto

qed

end