Theory Topology_ZF_1
section ‹Topology 1›
theory Topology_ZF_1 imports Topology_ZF
begin
text‹In this theory file we study separation axioms and the notion of base and
subbase. Using the products of open sets as a subbase we define a natural
topology on a product of two topological spaces.›
subsection‹Separation axioms›
text‹Topological spaces cas be classified according to certain properties
called "separation axioms". In this section we define what it means that a
topological space is $T_0$, $T_1$ or $T_2$.›
text‹A topology on $X$ is $T_0$ if for every pair of distinct points of $X$
there is an open set that contains only one of them.›
definition
isT0 ("_ {is T⇩0}" [90] 91) where
"T {is T⇩0} ≡ ∀ x y. ((x ∈ ⋃T ∧ y ∈ ⋃T ∧ x≠y) ⟶
(∃U∈T. (x∈U ∧ y∉U) ∨ (y∈U ∧ x∉U)))"
text‹A topology is $T_1$ if for every such pair there exist an open set that
contains the first point but not the second.›
definition
isT1 ("_ {is T⇩1}" [90] 91) where
"T {is T⇩1} ≡ ∀ x y. ((x ∈ ⋃T ∧ y ∈ ⋃T ∧ x≠y) ⟶
(∃U∈T. (x∈U ∧ y∉U)))"
text‹ $T_1$ topological spaces are exactly those in which all singletons are closed.›
lemma (in topology0) t1_def_alt:
shows "T {is T⇩1} ⟷ (∀x∈⋃T. {x} {is closed in} T)"
proof
let ?X = "⋃T"
assume T1: "T {is T⇩1}"
{ fix x assume "x∈?X"
let ?U = "?X-{x}"
have "?U ∈ T"
proof -
let ?W = "⋃y∈?U.⋃{V∈T. y∈V ∧ x∉V}"
{ fix y assume "y∈?U"
with topSpaceAssum have "(⋃{V∈T. y∈V ∧ x∉V}) ∈ T"
unfolding IsATopology_def by blast
} hence "∀y∈?U. (⋃{V∈T. y∈V ∧ x∉V}) ∈ T" by blast
with topSpaceAssum have "?W∈T" by (rule union_indexed_open)
have "?U = ?W"
proof
show "?W⊆?U" by auto
{ fix y assume "y∈?U"
hence "y∈?X" and "y≠x" by auto
with T1 ‹x∈?X› have "y ∈ ⋃{V∈T. y∈V ∧ x∉V}"
unfolding isT1_def by blast
hence "y∈?W" by blast
} thus "?U ⊆ ?W" by blast
qed
with ‹?W∈T› show "?U∈T" by simp
qed
with ‹x∈?X› have "(?X-?U) {is closed in} T" and "?X-?U = {x}"
using Top_3_L9 by auto
hence "{x} {is closed in} T" by simp
} thus "∀x∈?X. {x} {is closed in} T" by blast
next
let ?X = "⋃T"
assume scl: "∀x∈⋃T. {x} {is closed in} T"
{ fix x y assume "x∈?X" "y∈?X" "x≠y"
let ?U = "?X-{y}"
from scl ‹x∈?X› ‹y∈?X› ‹x≠y› have "?U ∈ T" "x∈?U ∧ y∉?U"
unfolding IsClosed_def by auto
then have "∃U∈T. (x∈U ∧ y∉U)" by (rule witness_exists)
} then show "T {is T⇩1}" unfolding isT1_def by blast
qed
text‹A topology is $T_2$ (Hausdorff) if for every pair of points there exist a
pair of disjoint open sets each containing one of the points.
This is an important class of topological spaces. In particular, metric
spaces are Hausdorff.›
definition
isT2 ("_ {is T⇩2}" [90] 91) where
"T {is T⇩2} ≡ ∀ x y. ((x ∈ ⋃T ∧ y ∈ ⋃T ∧ x≠y) ⟶
(∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0))"
text‹A topology is regular if every closed set can be separated from a point in its complement
by (disjoint) opens sets.›
definition
IsRegular ("_ {is regular}" 90)
where "T {is regular} ≡ ∀D. D {is closed in} T ⟶ (∀x∈⋃T-D.∃U∈T.∃V∈T. D⊆U∧x∈V∧U∩V=0)"
text‹Some sources (e.g. Metamath) use a different definition of regularity:
any open neighborhood has a closed subneighborhood. The next lemma shows the equivalence
of this with our definition.›
lemma is_regular_def_alt: assumes "T {is a topology}"
shows "T {is regular} ⟷ (∀W∈T. ∀x∈W. ∃V∈T. x∈V ∧ Closure(V,T)⊆W)"
proof
let ?X = "⋃T"
from assms(1) have cntx: "topology0(T)"
unfolding topology0_def by simp
assume "T {is regular}"
{ fix W x assume "W∈T" "x∈W"
have "∃V∈T. x∈V ∧ Closure(V,T)⊆W"
proof -
let ?D = "?X-W"
from cntx ‹W∈T› ‹T {is regular}› ‹x∈W›
have "∃U∈T.∃V∈T. ?D⊆U∧x∈V∧U∩V=0"
using topology0.Top_3_L9 unfolding IsRegular_def by auto
then obtain U V where "U∈T" "V∈T" "?D⊆U" "x∈V" "V∩U=0"
by blast
from cntx ‹V∈T› have "Closure(V,T) ⊆ ?X"
using topology0.Top_3_L11(1) by blast
from cntx ‹V∈T› ‹U∈T› ‹V∩U=0› ‹?D⊆U›
have "Closure(V,T) ∩ ?D = 0"
using topology0.disj_open_cl_disj by blast
with ‹Closure(V,T) ⊆ ?X› ‹V∈T› ‹x∈V› show ?thesis
by blast
qed
} thus "∀W∈T. ∀x∈W. ∃V∈T. x∈V ∧ Closure(V,T)⊆W"
by simp
next
let ?X = "⋃T"
from assms(1) have cntx: "topology0(T)"
unfolding topology0_def by simp
assume regAlt: "∀W∈T. ∀x∈W. ∃V∈T. x∈V ∧ Closure(V,T)⊆W"
{ fix A assume "A {is closed in} T"
have "∀x∈?X-A.∃U∈T.∃V∈T. A⊆U ∧ x∈V ∧ U∩V=0"
proof -
{ let ?W = "?X-A"
from ‹A {is closed in} T› have "A⊆?X" and "?W∈T"
unfolding IsClosed_def by auto
fix x assume "x∈?W"
with regAlt ‹?W∈T› have "∃V∈T. x∈V ∧ Closure(V,T)⊆?W"
by simp
then obtain V where "V∈T" "x∈V" "Closure(V,T)⊆?W"
by auto
let ?U = "?X-Closure(V,T)"
from cntx ‹V∈T› have "V⊆?X" and "V⊆Closure(V,T)"
using topology0.cl_contains_set by auto
with cntx ‹A⊆?X› ‹Closure(V,T)⊆?W›
have "?U∈T" "A⊆?U" "?U∩V = 0"
using topology0.cl_is_closed(2) by auto
with ‹V∈T› ‹x∈V› have "∃U∈T.∃V∈T. A⊆U ∧ x∈V ∧ U∩V=0"
by blast
} thus ?thesis by blast
qed
} then show "T {is regular}" unfolding IsRegular_def
by blast
qed
text‹If a topology is $T_1$ then it is $T_0$.
We don't really assume here that $T$ is a topology on $X$.
Instead, we prove the relation between isT0 condition and isT1.›
lemma T1_is_T0: assumes A1: "T {is T⇩1}" shows "T {is T⇩0}"
proof -
from A1 have "∀ x y. x ∈ ⋃T ∧ y ∈ ⋃T ∧ x≠y ⟶
(∃U∈T. x∈U ∧ y∉U)"
using isT1_def by simp
then have "∀ x y. x ∈ ⋃T ∧ y ∈ ⋃T ∧ x≠y ⟶
(∃U∈T. x∈U ∧ y∉U ∨ y∈U ∧ x∉U)"
by auto
then show "T {is T⇩0}" using isT0_def by simp
qed
text‹If a topology is $T_2$ then it is $T_1$.›
lemma T2_is_T1: assumes A1: "T {is T⇩2}" shows "T {is T⇩1}"
proof -
{ fix x y assume "x ∈ ⋃T" "y ∈ ⋃T" "x≠y"
with A1 have "∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0"
using isT2_def by auto
then have "∃U∈T. x∈U ∧ y∉U" by auto
} then have "∀ x y. x ∈ ⋃T ∧ y ∈ ⋃T ∧ x≠y ⟶
(∃U∈T. x∈U ∧ y∉U)" by simp
then show "T {is T⇩1}" using isT1_def by simp
qed
text‹In a $T_0$ space two points that can not be separated
by an open set are equal. Proof by contradiction.›
lemma Top_1_1_L1: assumes A1: "T {is T⇩0}" and A2: "x ∈ ⋃T" "y ∈ ⋃T"
and A3: "∀U∈T. (x∈U ⟷ y∈U)"
shows "x=y"
proof -
{ assume "x≠y"
with A1 A2 have "∃U∈T. x∈U ∧ y∉U ∨ y∈U ∧ x∉U"
using isT0_def by simp
with A3 have False by auto
} then show "x=y" by auto
qed
subsection‹Bases and subbases›
text‹Sometimes it is convenient to talk about topologies in terms of their bases
and subbases. These are certain collections of open sets that define
the whole topology.›
text‹A base of topology is a collection of open sets such that every
open set is a union of the sets from the base.›
definition
IsAbaseFor (infixl "{is a base for}" 65) where
"B {is a base for} T ≡ B⊆T ∧ T = {⋃A. A∈Pow(B)}"
text‹A subbase is a collection
of open sets such that finite intersection of those sets form a base.›
definition
IsAsubBaseFor (infixl "{is a subbase for}" 65) where
"B {is a subbase for} T ≡
B ⊆ T ∧ {⋂A. A ∈ FinPow(B)} {is a base for} T"
text‹Below we formulate a condition that we will prove to be necessary and
sufficient for a collection $B$ of open sets to form a base.
It says that for any two sets $U,V$ from the collection $B$ we can
find a point $x\in U\cap V$ with a neighboorhod
from $B$ contained in $U\cap V$.›
definition
SatisfiesBaseCondition ("_ {satisfies the base condition}" [50] 50)
where
"B {satisfies the base condition} ≡
∀U V. ((U∈B ∧ V∈B) ⟶ (∀x ∈ U∩V. ∃W∈B. x∈W ∧ W ⊆ U∩V))"
text‹A collection that is closed with respect to intersection
satisfies the base condition.›
lemma inter_closed_base: assumes "∀U∈B.(∀V∈B. U∩V ∈ B)"
shows "B {satisfies the base condition}"
proof -
{ fix U V x assume "U∈B" and "V∈B" and "x ∈ U∩V"
with assms have "∃W∈B. x∈W ∧ W ⊆ U∩V" by blast
} then show ?thesis using SatisfiesBaseCondition_def by simp
qed
text‹Each open set is a union of some sets from the base.›
lemma Top_1_2_L1: assumes "B {is a base for} T" and "U∈T"
shows "∃A∈Pow(B). U = ⋃A"
using assms IsAbaseFor_def by simp
text‹Elements of base are open.›
lemma base_sets_open:
assumes "B {is a base for} T" and "U ∈ B"
shows "U ∈ T"
using assms IsAbaseFor_def by auto
text‹A base defines topology uniquely.›
lemma same_base_same_top:
assumes "B {is a base for} T" and "B {is a base for} S"
shows "T = S"
using assms IsAbaseFor_def by simp
text‹Every point from an open set has a neighboorhood from the base
that is contained in the set.›
lemma point_open_base_neigh:
assumes A1: "B {is a base for} T" and A2: "U∈T" and A3: "x∈U"
shows "∃V∈B. V⊆U ∧ x∈V"
proof -
from A1 A2 obtain A where "A ∈ Pow(B)" and "U = ⋃A"
using Top_1_2_L1 by blast
with A3 obtain V where "V∈A" and "x∈V" by auto
with ‹A ∈ Pow(B)› ‹U = ⋃A› show ?thesis by auto
qed
text‹A criterion for a collection to be a base for a topology
that is a slight reformulation of the definition. The only thing
different that in the definition is that we assume only that
every open set is a union of some sets from the base. The definition
requires also the opposite inclusion that every union of the
sets from the base is open, but that we can prove if we assume that
$T$ is a topology.›
lemma is_a_base_criterion: assumes A1: "T {is a topology}"
and A2: "B ⊆ T" and A3: "∀V ∈ T. ∃A ∈ Pow(B). V = ⋃A"
shows "B {is a base for} T"
proof -
from A3 have "T ⊆ {⋃A. A∈Pow(B)}" by auto
moreover have "{⋃A. A∈Pow(B)} ⊆ T"
proof
fix U assume "U ∈ {⋃A. A∈Pow(B)}"
then obtain A where "A ∈ Pow(B)" and "U = ⋃A"
by auto
with ‹B ⊆ T› have "A ∈ Pow(T)" by auto
with A1 ‹U = ⋃A› show "U ∈ T"
unfolding IsATopology_def by simp
qed
ultimately have "T = {⋃A. A∈Pow(B)}" by auto
with A2 show "B {is a base for} T"
unfolding IsAbaseFor_def by simp
qed
text‹A necessary condition for a collection of sets to be a base for some
topology : every point in the intersection
of two sets in the base has a neighboorhood from the base contained
in the intersection.›
lemma Top_1_2_L2:
assumes A1:"∃T. T {is a topology} ∧ B {is a base for} T"
and A2: "V∈B" "W∈B"
shows "∀ x ∈ V∩W. ∃U∈B. x∈U ∧ U ⊆ V ∩ W"
proof -
from A1 obtain T where
D1: "T {is a topology}" "B {is a base for} T"
by auto
then have "B ⊆ T" using IsAbaseFor_def by auto
with A2 have "V∈T" and "W∈T" using IsAbaseFor_def by auto
with D1 have "∃A∈Pow(B). V∩W = ⋃A" using IsATopology_def Top_1_2_L1
by auto
then obtain A where "A ⊆ B" and "V ∩ W = ⋃A" by auto
then show "∀ x ∈ V∩W. ∃U∈B. (x∈U ∧ U ⊆ V ∩ W)" by auto
qed
text‹We will construct a topology as the collection of unions of (would-be)
base. First we prove that if the collection of sets satisfies the
condition we want to show to be sufficient, the the intersection belongs
to what we will define as topology (am I clear here?). Having this fact
ready simplifies the proof of the next lemma. There is not much topology
here, just some set theory.›
lemma Top_1_2_L3:
assumes A1: "∀x∈ V∩W . ∃U∈B. x∈U ∧ U ⊆ V∩W"
shows "V∩W ∈ {⋃A. A∈Pow(B)}"
proof
let ?A = "⋃x∈V∩W. {U∈B. x∈U ∧ U ⊆ V∩W}"
show "?A∈Pow(B)" by auto
from A1 show "V∩W = ⋃?A" by blast
qed
text‹The next lemma is needed when proving that the would-be topology is
closed with respect to taking intersections. We show here that intersection
of two sets from this (would-be) topology can be written as union of sets
from the topology.›
lemma Top_1_2_L4:
assumes A1: "U⇩1 ∈ {⋃A. A∈Pow(B)}" "U⇩2 ∈ {⋃A. A∈Pow(B)}"
and A2: "B {satisfies the base condition}"
shows "∃C. C ⊆ {⋃A. A∈Pow(B)} ∧ U⇩1∩U⇩2 = ⋃C"
proof -
from A1 A2 obtain A⇩1 A⇩2 where
D1: "A⇩1∈ Pow(B)" "U⇩1 = ⋃A⇩1" "A⇩2 ∈ Pow(B)" "U⇩2 = ⋃A⇩2"
by auto
let ?C = "⋃U∈A⇩1.{U∩V. V∈A⇩2}"
from D1 have "(∀U∈A⇩1. U∈B) ∧ (∀V∈A⇩2. V∈B)" by auto
with A2 have "?C ⊆ {⋃A . A ∈ Pow(B)}"
using Top_1_2_L3 SatisfiesBaseCondition_def by auto
moreover from D1 have "U⇩1 ∩ U⇩2 = ⋃?C" by auto
ultimately show ?thesis by auto
qed
text‹If $B$ satisfies the base condition, then the collection of unions
of sets from $B$ is a topology and $B$ is a base for this topology.›
theorem Top_1_2_T1:
assumes A1: "B {satisfies the base condition}"
and A2: "T = {⋃A. A∈Pow(B)}"
shows "T {is a topology}" and "B {is a base for} T"
proof -
show "T {is a topology}"
proof -
have I: "∀C∈Pow(T). ⋃C ∈ T"
proof -
{ fix C assume A3: "C ∈ Pow(T)"
let ?Q = "⋃ {⋃{A∈Pow(B). U = ⋃A}. U∈C}"
from A2 A3 have "∀U∈C. ∃A∈Pow(B). U = ⋃A" by auto
then have "⋃?Q = ⋃C" using ZF1_1_L10 by simp
moreover from A2 have "⋃?Q ∈ T" by auto
ultimately have "⋃C ∈ T" by simp
} thus "∀C∈Pow(T). ⋃C ∈ T" by auto
qed
moreover have "∀U∈T. ∀ V∈T. U∩V ∈ T"
proof -
{ fix U V assume "U ∈ T" "V ∈ T"
with A1 A2 have "∃C.(C ⊆ T ∧ U∩V = ⋃C)"
using Top_1_2_L4 by simp
then obtain C where "C ⊆ T" and "U∩V = ⋃C"
by auto
with I have "U∩V ∈ T" by simp
} then show "∀U∈T. ∀ V∈T. U∩V ∈ T" by simp
qed
ultimately show "T {is a topology}" using IsATopology_def
by simp
qed
from A2 have "B⊆T" by auto
with A2 show "B {is a base for} T" using IsAbaseFor_def
by simp
qed
text‹The carrier of the base and topology are the same.›
lemma Top_1_2_L5: assumes "B {is a base for} T"
shows "⋃T = ⋃B"
using assms IsAbaseFor_def by auto
text‹If $B$ is a base for $T$, then $T$ is the smallest topology containing $B$.
›
lemma base_smallest_top:
assumes A1: "B {is a base for} T" and A2: "S {is a topology}" and A3: "B⊆S"
shows "T⊆S"
proof
fix U assume "U∈T"
with A1 obtain B⇩U where "B⇩U ⊆ B" and "U = ⋃B⇩U" using IsAbaseFor_def by auto
with A3 have "B⇩U ⊆ S" by auto
with A2 ‹U = ⋃B⇩U› show "U∈S" using IsATopology_def by simp
qed
text‹If $B$ is a base for $T$ and $B$ is a topology, then $B=T$.›
lemma base_topology: assumes "B {is a topology}" and "B {is a base for} T"
shows "B=T" using assms base_sets_open base_smallest_top by blast
subsection‹Product topology›
text‹In this section we consider a topology defined on a product of two sets.›
text‹Given two topological spaces we can define a topology on the product of
the carriers such that the cartesian products of the sets of the topologies
are a base for the product topology. Recall that for two collections $S,T$
of sets the product collection is defined (in ‹ZF1.thy›) as the collections of cartesian
products $A\times B$, where $A\in S, B\in T$. The $T\times_tS$ notation is defined as
an alternative to the verbose ‹ProductTopology(T,S)›). ›
definition ProductTopology (infixl "×⇩t" 65) where
"T ×⇩t S ≡ {⋃W. W ∈ Pow(ProductCollection(T,S))}"
text‹The product collection satisfies the base condition.›
lemma Top_1_4_L1:
assumes A1: "T {is a topology}" "S {is a topology}"
and A2: "A ∈ ProductCollection(T,S)" "B ∈ ProductCollection(T,S)"
shows "∀x∈(A∩B). ∃W∈ProductCollection(T,S). (x∈W ∧ W ⊆ A ∩ B)"
proof
fix x assume A3: "x ∈ A∩B"
from A2 obtain U⇩1 V⇩1 U⇩2 V⇩2 where
D1: "U⇩1∈T" "V⇩1∈S" "A=U⇩1×V⇩1" "U⇩2∈T" "V⇩2∈S" "B=U⇩2×V⇩2"
using ProductCollection_def by auto
let ?W = "(U⇩1∩U⇩2) × (V⇩1∩V⇩2)"
from A1 D1 have "U⇩1∩U⇩2 ∈ T" and "V⇩1∩V⇩2 ∈ S"
using IsATopology_def by auto
then have "?W ∈ ProductCollection(T,S)" using ProductCollection_def
by auto
moreover from A3 D1 have "x∈?W" and "?W ⊆ A∩B" by auto
ultimately have "∃W. (W ∈ ProductCollection(T,S) ∧ x∈W ∧ W ⊆ A∩B)"
by auto
thus "∃W∈ProductCollection(T,S). (x∈W ∧ W ⊆ A ∩ B)" by auto
qed
text‹The product topology is indeed a topology on the product.›
theorem Top_1_4_T1: assumes A1: "T {is a topology}" "S {is a topology}"
shows
"(T×⇩tS) {is a topology}"
"ProductCollection(T,S) {is a base for} (T×⇩tS)"
"⋃(T×⇩tS) = ⋃T × ⋃S"
proof -
from A1 show
"(T×⇩tS) {is a topology}"
"ProductCollection(T,S) {is a base for} (T×⇩tS)"
using Top_1_4_L1 ProductCollection_def
SatisfiesBaseCondition_def ProductTopology_def Top_1_2_T1
by auto
then show "⋃(T×⇩tS) = ⋃T × ⋃S"
using Top_1_2_L5 ZF1_1_L6 by simp
qed
text‹Each point of a set open in the product topology has a neighborhood
which is a cartesian product of open sets.›
lemma prod_top_point_neighb:
assumes A1: "T {is a topology}" "S {is a topology}" and
A2: "U ∈ ProductTopology(T,S)" and A3: "x ∈ U"
shows "∃V W. V∈T ∧ W∈S ∧ V×W ⊆ U ∧ x ∈ V×W"
proof -
from A1 have
"ProductCollection(T,S) {is a base for} ProductTopology(T,S)"
using Top_1_4_T1 by simp
with A2 A3 obtain Z where
"Z ∈ ProductCollection(T,S)" and "Z ⊆ U ∧ x∈Z"
using point_open_base_neigh by blast
then obtain V W where "V ∈ T" and "W∈S" and" V×W ⊆ U ∧ x ∈ V×W"
using ProductCollection_def by auto
thus ?thesis by auto
qed
text‹Products of open sets are open in the product topology.›
lemma prod_open_open_prod:
assumes A1: "T {is a topology}" "S {is a topology}" and
A2: "U∈T" "V∈S"
shows "U×V ∈ ProductTopology(T,S)"
proof -
from A1 have
"ProductCollection(T,S) {is a base for} ProductTopology(T,S)"
using Top_1_4_T1 by simp
moreover from A2 have "U×V ∈ ProductCollection(T,S)"
unfolding ProductCollection_def by auto
ultimately show "U×V ∈ ProductTopology(T,S)"
using base_sets_open by simp
qed
text‹Sets that are open in the product topology are contained in the product
of the carrier.›
lemma prod_open_type: assumes A1: "T {is a topology}" "S {is a topology}" and
A2: "V ∈ ProductTopology(T,S)"
shows "V ⊆ ⋃T × ⋃S"
proof -
from A2 have "V ⊆ ⋃ ProductTopology(T,S)" by auto
with A1 show ?thesis using Top_1_4_T1 by simp
qed
text‹A reverse of ‹prod_top_point_neighb›: if each point of set has an neighborhood in the set
that is a cartesian product of open sets, then the set is open.›
lemma point_neighb_prod_top:
assumes "T {is a topology}" "S {is a topology}"
and "∀p∈V. ∃U∈T.∃W∈S. p∈U×W ∧ U×W ⊆ V"
shows "V ∈ ProductTopology(T,S)"
proof -
from assms(1,2) have I: "topology0(ProductTopology(T,S))"
using Top_1_4_T1(1) topology0_def by simp
moreover
{ fix p assume "p∈V"
with assms(3) obtain U W where "U∈T" "W∈S" "p∈U×W" "U×W ⊆ V"
by auto
with assms(1,2) have "∃N∈ProductTopology(T,S). p∈N ∧ N⊆V"
using prod_open_open_prod by auto
} hence "∀p∈V. ∃N∈ProductTopology(T,S). p∈N ∧ N⊆V" by blast
ultimately show ?thesis using topology0.open_neigh_open by simp
qed
text‹Suppose we have subsets $A\subseteq X, B\subseteq Y$, where
$X,Y$ are topological spaces with topologies $T,S$. We can the consider
relative topologies on $T_A, S_B$ on sets $A,B$ and the collection
of cartesian products of sets open in $T_A, S_B$, (namely
$\{U\times V: U\in T_A, V\in S_B\}$. The next lemma states that
this collection is a base of the product topology on $X\times Y$
restricted to the product $A\times B$.›
lemma prod_restr_base_restr:
assumes A1: "T {is a topology}" "S {is a topology}"
shows
"ProductCollection(T {restricted to} A, S {restricted to} B)
{is a base for} (ProductTopology(T,S) {restricted to} A×B)"
proof -
let ?ℬ = "ProductCollection(T {restricted to} A, S {restricted to} B)"
let ?τ = "ProductTopology(T,S)"
from A1 have "(?τ {restricted to} A×B) {is a topology}"
using Top_1_4_T1 topology0_def topology0.Top_1_L4
by simp
moreover have "?ℬ ⊆ (?τ {restricted to} A×B)"
proof
fix U assume "U ∈ ?ℬ"
then obtain U⇩A U⇩B where "U = U⇩A × U⇩B" and
"U⇩A ∈ (T {restricted to} A)" and "U⇩B ∈ (S {restricted to} B)"
using ProductCollection_def by auto
then obtain W⇩A W⇩B where
"W⇩A ∈ T" "U⇩A = W⇩A ∩ A" and "W⇩B ∈ S" "U⇩B = W⇩B ∩ B"
using RestrictedTo_def by auto
with ‹U = U⇩A × U⇩B› have "U = W⇩A×W⇩B ∩ (A×B)" by auto
moreover from A1 ‹W⇩A ∈ T› and ‹W⇩B ∈ S› have "W⇩A×W⇩B ∈ ?τ"
using prod_open_open_prod by simp
ultimately show "U ∈ ?τ {restricted to} A×B"
using RestrictedTo_def by auto
qed
moreover have "∀U ∈ ?τ {restricted to} A×B.
∃C ∈ Pow(?ℬ). U = ⋃C"
proof
fix U assume "U ∈ ?τ {restricted to} A×B"
then obtain W where "W ∈ ?τ" and "U = W ∩ (A×B)"
using RestrictedTo_def by auto
from A1 ‹W ∈ ?τ› obtain A⇩W where
"A⇩W ∈ Pow(ProductCollection(T,S))" and "W = ⋃A⇩W"
using Top_1_4_T1 IsAbaseFor_def by auto
let ?C = "{V ∩ A×B. V ∈ A⇩W}"
have "?C ∈ Pow(?ℬ)" and "U = ⋃?C"
proof -
{ fix R assume "R ∈ ?C"
then obtain V where "V ∈ A⇩W" and "R = V ∩ A×B"
by auto
with ‹A⇩W ∈ Pow(ProductCollection(T,S))› obtain V⇩T V⇩S where
"V⇩T ∈ T" and "V⇩S ∈ S" and "V = V⇩T × V⇩S"
using ProductCollection_def by auto
with ‹R = V ∩ A×B› have "R ∈ ?ℬ"
using ProductCollection_def RestrictedTo_def
by auto
} then show "?C ∈ Pow(?ℬ)" by auto
from ‹U = W ∩ (A×B)› and ‹W = ⋃A⇩W›
show "U = ⋃?C" by auto
qed
thus "∃C ∈ Pow(?ℬ). U = ⋃C" by blast
qed
ultimately show ?thesis by (rule is_a_base_criterion)
qed
text‹We can commute taking restriction (relative topology) and
product topology. The reason the two topologies are the same is
that they have the same base.›
lemma prod_top_restr_comm:
assumes A1: "T {is a topology}" "S {is a topology}"
shows
"ProductTopology(T {restricted to} A,S {restricted to} B) =
ProductTopology(T,S) {restricted to} (A×B)"
proof -
let ?ℬ = "ProductCollection(T {restricted to} A, S {restricted to} B)"
from A1 have
"?ℬ {is a base for} ProductTopology(T {restricted to} A,S {restricted to} B)"
using topology0_def topology0.Top_1_L4 Top_1_4_T1 by simp
moreover from A1 have
"?ℬ {is a base for} ProductTopology(T,S) {restricted to} (A×B)"
using prod_restr_base_restr by simp
ultimately show ?thesis by (rule same_base_same_top)
qed
text‹Projection of a section of an open set is open.›
lemma prod_sec_open1: assumes A1: "T {is a topology}" "S {is a topology}" and
A2: "V ∈ ProductTopology(T,S)" and A3: "x ∈ ⋃T"
shows "{y ∈ ⋃S. ⟨x,y⟩ ∈ V} ∈ S"
proof -
let ?A = "{y ∈ ⋃S. ⟨x,y⟩ ∈ V}"
from A1 have "topology0(S)" using topology0_def by simp
moreover have "∀y∈?A.∃W∈S. (y∈W ∧ W⊆?A)"
proof
fix y assume "y ∈ ?A"
then have "⟨x,y⟩ ∈ V" by simp
with A1 A2 have "⟨x,y⟩ ∈ ⋃T × ⋃S" using prod_open_type by blast
hence "x ∈ ⋃T" and "y ∈ ⋃S" by auto
from A1 A2 ‹⟨x,y⟩ ∈ V› have "∃U W. U∈T ∧ W∈S ∧ U×W ⊆ V ∧ ⟨x,y⟩ ∈ U×W"
by (rule prod_top_point_neighb)
then obtain U W where "U∈T" "W∈S" "U×W ⊆ V" "⟨x,y⟩ ∈ U×W"
by auto
with A1 A2 show "∃W∈S. (y∈W ∧ W⊆?A)" using prod_open_type section_proj
by auto
qed
ultimately show ?thesis by (rule topology0.open_neigh_open)
qed
text‹Projection of a section of an open set is open. This is dual of
‹prod_sec_open1› with a very similar proof.›
lemma prod_sec_open2: assumes A1: "T {is a topology}" "S {is a topology}" and
A2: "V ∈ ProductTopology(T,S)" and A3: "y ∈ ⋃S"
shows "{x ∈ ⋃T. ⟨x,y⟩ ∈ V} ∈ T"
proof -
let ?A = "{x ∈ ⋃T. ⟨x,y⟩ ∈ V}"
from A1 have "topology0(T)" using topology0_def by simp
moreover have "∀x∈?A.∃W∈T. (x∈W ∧ W⊆?A)"
proof
fix x assume "x ∈ ?A"
then have "⟨x,y⟩ ∈ V" by simp
with A1 A2 have "⟨x,y⟩ ∈ ⋃T × ⋃S" using prod_open_type by blast
hence "x ∈ ⋃T" and "y ∈ ⋃S" by auto
from A1 A2 ‹⟨x,y⟩ ∈ V› have "∃U W. U∈T ∧ W∈S ∧ U×W ⊆ V ∧ ⟨x,y⟩ ∈ U×W"
by (rule prod_top_point_neighb)
then obtain U W where "U∈T" "W∈S" "U×W ⊆ V" "⟨x,y⟩ ∈ U×W"
by auto
with A1 A2 show "∃W∈T. (x∈W ∧ W⊆?A)" using prod_open_type section_proj
by auto
qed
ultimately show ?thesis by (rule topology0.open_neigh_open)
qed
subsection‹Hausdorff spaces›
text‹In this section we study properties of Hausdorff spaces (sometimes called separated spaces)
These are topological spaces that are $T_2$ as defined above.›
text‹A space is Hausdorff if and only if the diagonal $\Delta = \{\langle x,x\rangle : x\in X\}$
is closed in the product topology on $X\times X$. ›
theorem t2_iff_diag_closed: assumes "T {is a topology}"
shows "T {is T⇩2} ⟷ {⟨x,x⟩. x∈⋃T} {is closed in} ProductTopology(T,T)"
proof
let ?X = "⋃T"
from assms(1) have I: "topology0(ProductTopology(T,T))"
using Top_1_4_T1(1) topology0_def by simp
assume "T {is T⇩2}" show "{⟨x,x⟩. x∈?X} {is closed in} ProductTopology(T,T)"
proof -
let ?D⇩c = "?X×?X - {⟨x,x⟩. x∈?X}"
have "∀p∈?D⇩c.∃U∈T.∃V∈T. p∈U×V ∧ U×V ⊆ ?D⇩c"
proof -
{ fix p assume "p∈?D⇩c"
then obtain x y where "p=⟨x,y⟩" "x∈?X" "y∈?X" "x≠y" by auto
with ‹T {is T⇩2}› obtain U V where "U∈T" "V∈T" "x∈U" "y∈V" "U∩V = 0"
unfolding isT2_def by blast
with assms ‹p=⟨x,y⟩› have "∃U∈T.∃V∈T. p∈U×V ∧ U×V ⊆ ?D⇩c" by auto
} hence "∀p. p∈?D⇩c ⟶ (∃U∈T.∃V∈T. p∈U×V ∧ U×V ⊆ ?D⇩c)" by simp
then show ?thesis by (rule exists_in_set)
qed
with assms show ?thesis using Top_1_4_T1(3) point_neighb_prod_top
unfolding IsClosed_def by auto
qed
next
let ?X = "⋃T"
assume A: "{⟨x,x⟩. x∈?X} {is closed in} ProductTopology(T,T)" show "T {is T⇩2}"
proof -
{ let ?D⇩c = "?X×?X - {⟨x,x⟩. x∈?X}"
fix x y assume "x∈?X" "y∈?X" "x≠y"
with assms A have "?D⇩c ∈ ProductTopology(T,T)" and "⟨x,y⟩ ∈ ?D⇩c"
using Top_1_4_T1(3) unfolding IsClosed_def by auto
with assms obtain U V where "U∈T" "V∈T" "U×V ⊆ ?D⇩c" "⟨x,y⟩ ∈ U×V"
using prod_top_point_neighb by blast
moreover from ‹U×V ⊆ ?D⇩c› have "U∩V = 0" by auto
ultimately have "∃U∈T.∃V∈T. x∈U ∧ y∈V ∧ U∩V=0" by auto
} then show "T {is T⇩2}" unfolding isT2_def by simp
qed
qed
end