Theory Topology_ZF_1b
section ‹Topology 1b›
theory Topology_ZF_1b imports Topology_ZF_1
begin
text‹One of the facts demonstrated in every class on General Topology is that
in a $T_2$ (Hausdorff) topological space compact sets are closed.
Formalizing the proof of this fact gave me an interesting insight
into the role of the Axiom of Choice (AC) in many informal proofs.
A typical informal proof of this fact goes like this: we want to show
that the complement of $K$ is open. To do this,
choose an arbitrary point $y\in K^c$.
Since $X$ is $T_2$, for every point $x\in K$ we can find an
open set $U_x$ such that $y\notin \overline{U_x}$.
Obviously $\{U_x\}_{x\in K}$ covers $K$, so select a finite subcollection
that covers $K$, and so on. I had never realized that
such reasoning requires the Axiom of Choice.
Namely, suppose we have a lemma that states "In $T_2$ spaces,
if $x\neq y$, then there is an open set
$U$ such that $x\in U$ and $y\notin \overline{U}$" (like our
lemma ‹T2_cl_open_sep› below). This only states that
the set of such open sets $U$ is not empty. To get the collection
$\{U_x \}_{x\in K}$ in this proof we have to select one such set
among many for every $x\in K$ and this is where we use the Axiom of Choice.
Probably in 99/100 cases when an informal calculus proof states something like
$\forall \varepsilon \exists \delta_\varepsilon \cdots$ the proof uses AC.
Most of the time the use of AC in such proofs can be avoided. This is also
the case for the fact that in a $T_2$ space compact sets are closed.
›
subsection‹Compact sets are closed - no need for AC›
text‹In this section we show that in a $T_2$ topological
space compact sets are closed.›
text‹First we prove a lemma that in a $T_2$ space two points
can be separated by the closure of an open set.›
lemma (in topology0) T2_cl_open_sep:
assumes "T {is T⇩2}" and "x ∈ ⋃T" "y ∈ ⋃T" "x≠y"
shows "∃U∈T. (x∈U ∧ y ∉ cl(U))"
proof -
from assms have "∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0"
using isT2_def by simp
then obtain U V where "U∈T" "V∈T" "x∈U" "y∈V" "U∩V=0"
by auto
then have "U∈T ∧ x∈U ∧ y∈ V ∧ cl(U) ∩ V = 0"
using disj_open_cl_disj by auto
thus "∃U∈T. (x∈U ∧ y ∉ cl(U))" by auto
qed
text‹AC-free proof that in a Hausdorff space compact sets
are closed. To understand the notation recall that in Isabelle/ZF
‹Pow(A)› is the powerset (the set of subsets) of $A$
and ‹FinPow(A)› denotes the set of finite subsets of $A$
in IsarMathLib.›
theorem (in topology0) in_t2_compact_is_cl:
assumes A1: "T {is T⇩2}" and A2: "K {is compact in} T"
shows "K {is closed in} T"
proof -
let ?X = "⋃T"
have "∀y ∈ ?X - K. ∃U∈T. y∈U ∧ U ⊆ ?X - K"
proof -
{ fix y assume "y ∈ ?X" "y∉K"
have "∃U∈T. y∈U ∧ U ⊆ ?X - K"
proof -
let ?B = "⋃x∈K. {V∈T. x∈V ∧ y ∉ cl(V)}"
have I: "?B ∈ Pow(T)" "FinPow(?B) ⊆ Pow(?B)"
using FinPow_def by auto
from ‹K {is compact in} T› ‹y ∈ ?X› ‹y∉K› have
"∀x∈K. x ∈ ?X ∧ y ∈ ?X ∧ x≠y"
using IsCompact_def by auto
with ‹T {is T⇩2}› have "∀x∈K. {V∈T. x∈V ∧ y ∉ cl(V)} ≠ 0"
using T2_cl_open_sep by auto
hence "K ⊆ ⋃?B" by blast
with ‹K {is compact in} T› I have
"∃N ∈ FinPow(?B). K ⊆ ⋃N"
using IsCompact_def by auto
then obtain N where "N ∈ FinPow(?B)" "K ⊆ ⋃N"
by auto
with I have "N ⊆ ?B" by auto
hence "∀V∈N. V∈?B" by auto
let ?M = "{cl(V). V∈N}"
let ?C = "{D ∈ Pow(?X). D {is closed in} T}"
from ‹N ∈ FinPow(?B)› have "∀V∈?B. cl(V) ∈ ?C" "N ∈ FinPow(?B)"
using cl_is_closed IsClosed_def by auto
then have "?M ∈ FinPow(?C)" by (rule fin_image_fin)
then have "?X - ⋃?M ∈ T" using fin_union_cl_is_cl IsClosed_def
by simp
moreover from ‹y ∈ ?X› ‹y∉K› ‹∀V∈N. V∈?B› have
"y ∈ ?X - ⋃?M" by simp
moreover have "?X - ⋃?M ⊆ ?X - K"
proof -
from ‹∀V∈N. V∈?B› have "⋃N ⊆ ⋃?M" using cl_contains_set by auto
with ‹K ⊆ ⋃N› show "?X - ⋃?M ⊆ ?X - K" by auto
qed
ultimately have "∃U. U∈T ∧ y ∈ U ∧ U ⊆ ?X - K"
by auto
thus "∃U∈T. y∈U ∧ U ⊆ ?X - K" by auto
qed
} thus "∀y ∈ ?X - K. ∃U∈T. y∈U ∧ U ⊆ ?X - K"
by auto
qed
with A2 show "K {is closed in} T"
using open_neigh_open IsCompact_def IsClosed_def by auto
qed
end