Instantly share code, notes, and snippets.

Embed
What would you like to do?
(* Topological Spaces
Based on "A Bridge to Advanced Mathematics" by Dennis Sentilles
Translated to Isar by Michal J Wallace *)
theory TopSpace
imports Main
begin
textA topological space (X,T) is a pair where X is a set whose elements
are called the "points" of the topological space, and T is a fixed collection of
subsets of X called neighborhoods, with the following properties:
locale topspace =
fixes X :: "'a set"
fixes T :: "('a set) set"
assumes A1 [simp]: "x∈X ≡ ∃N∈T. x∈N"
assumes A2 [simp]: "U∈T ∧ V∈T ∧ x∈(U∩V) ⟹ ∃N∈T. x∈N ∧ N⊆(U∩V)"
begin
textA set NT which contains pX is called a neighborhood of p.
definition nhs :: "'a ⇒ ('a set) set"
where [simp]: "nhs p ≡ {N∈T. p∈N}"
textIfAXin topological space(X,T), thenpXis called a ❙‹limit point
ofAif the intersection of every neighborhood ofpwithAis non-empty.
In loose geometrical terms,pis either a point inAor as close as possible
toAwithout actually being in it.
definition limpt :: "'a set ⇒ 'a ⇒ bool" (* def 4.2.1 *)
where [simp]: "limpt A p ≡ A⊆X ∧ p∈X ∧ (∀N∈nhs p. (A∩N) ≠ {})"
textIfAXin topological space(X,T), thenxXis called an ❙‹interior point
ofAif at least one neighborhood ofxis contained entirely withinA.
definition intpt :: "'a set ⇒ 'a ⇒ bool" (* def 4.2.2 *)
where [simp]: "intpt A p ≡ A⊆X ∧ p∈A ∧ (∃N∈nhs p. N⊆A)"
definition boundpt :: "'a set ⇒ 'a ⇒ bool" (* def 4.2.3 *)
where "boundpt A p ≡ (limpt A p) ∧ (limpt (X-A) p)"
definition "open" :: "'a set ⇒ bool" (* def 4.2.4a *)
where "open A ≡ (∀p∈A. intpt A p)"
definition closed :: "'a set ⇒ bool" (* def 4.2.4b *)
where [simp, intro]: "closed A ⟷ open (X-A)"
textTHEOREM 4.2.5: A setAXin a topological space "‹(X,T)› is closed
iff every limit point of ‹A› belongs to ‹A›. Hence, if ‹∃› a limit point
of ‹A› not in ‹A›, then ‹A› is not closed. Conversely, if ‹A› is not
closed, then ‹∃› a limit point of ‹A› not in ‹A›.›
theorem t425a: assumes "closed A" and "limpt A p" shows "pA"
proof (rule ccontr)
assume "pA"
with `limpt A p` have "p(X-A)" by simp
moreover from `closed A` have "open (X-A)" by simp
ultimately have "intpt (X-A) p" using open_def by blast
― ‹that is, there's a neighborhood, ‹N∈T› of p such that ‹N⊆(X-A)› ›
with A2 `p∈(X-A)` obtain N where "pN" and "NT" and "N(X-A)" by auto
then have "NA={}" by auto ― ‹which contradicts the definition of a limit point.›
moreover have "NA{}" using `limpt A p` `p∈N` `N∈T` limpt_def by auto
ultimately show "False" by simp
qed
text ‹To prove the converse in Isar, I needed to make use of the following lemma,
which says that if some ‹x∈X› is not a limit point of ‹A⊆X› then there must be some
neighborhood ‹N› of ‹x› that does not intersect ‹A› at all.›
lemma non_limpt_nh:
assumes "AX" "xX" and "¬(limpt A x)"
obtains N where "Nnhs x" and "NA={}"
proof -
― "Start with the (negated) definition oflimpt A x"
from limpt_def have "¬(limpt A x) ≡ ¬(AXxX(Nnhs x. (AN){}))" by simp
― "Distributing ¬ overgives us three possibilities"
also have "… ≡ ¬(AX)(xX)(Nnhs x. AN={})" by simp
― "But our assumptions rule out the first two."
finally have "… ≡ ∃Nnhs x. AN = {}" using assms by auto
with `¬(limpt A x)` obtain N where "Nnhs x" and "NA={}" by auto
then show ?thesis using that by auto
qed
text ‹Now we can prove the second part of theorem 4.2.5: if ‹A› contains all its limit
points, then A is closed.›
theorem t425b: assumes a0: "AX" and a1: "p. limpt A ppA" shows "closed A"
― ‹Quoting Sentilles here (replacing his syntax with isar's and using my variable names:›
― ‹"To showAis closed, we must argue thatX-Ais open."›
― ‹"That is, that any point ofX-Ais an interior point ofX-A."›
― ‹"SupposexX-A. ThenxA."›
― ‹"SinceAcontains all its limit points, thenxis not a limit point ofA."›
― ‹"By [limpt_def] this means there is a neighborhoodNTofx
whose intersection withAis empty. In other words,N(X-A)."›
― ‹"But this meansX-Ais open by [open_def]."›
― ‹"This is what we wished to prove."›
proof -
have "x(X-A). intpt (X-A) x" proof
fix x assume "x(X-A)" hence "xA" by auto
have "¬(limpt A x)" using a1 ‹x∉A› by auto
with `x ∈ X-A` obtain N where "Nnhs x" and "NA={}" using a0 non_limpt_nh by blast
hence "NX-A" by auto
with `N∈nhs x` show "intpt (X-A) x" by auto
qed
hence "open (X-A)" using open_def by simp
thus "closed A" by simp
qed
text ‹❙‹COROLLARY 4.2.6›
A subset ‹A⊆X› of a topological space ‹(X,T)› is closed if ‹A› contains its boundary.›
text ‹
The last theorem shows that if ‹A⊆X› contains all its limit points, then it's closed.
Can we show that if ‹A› contains all its boundary points, it must contain all
its limit points?
First, many of the limit points are interior points, right? From intpt_def,
it seems like all interior points are limit points... right?
lemma int_lim:
assumes "AX" "intpt A p" shows "limpt A p"
using assms ball_empty intpt_def by auto
text ‹
It seems so. (We won't actually need that lemma, so I'll just trust the proof.
Isabelle generated when i typed the word 'try' after the `shows` clause.)
Anyway, back to the question of whether ‹A› containing its boundary implies
that it contains all its limit points.
Assume ‹A⊆X› contains its boundary points, and let ‹p› be a limit point of ‹A›
If ‹p› is an interior point, then ‹p∈A›.
else if it's a boundary point, then ‹p∈A› by assumption.
else ... well, what would that even mean?
The final case would be a limit point that is neither an interior point
nor a boundary point. It's hard for me to imagine such a thing, so maybe no
such thing exists.
If it doesn't exist, then we've covered all our bases, and the corollary
can be proven just by formalizing the argument above.
So... let's try to show that if ‹limpt A p ⟹ (intpt A p) ∨ (boundpt A p)›.
We know all boundary points are limit points by definition, and all interior
points are limit points from the lemma above, so really we only need to show
that a limit point that isn't one of those two things must be the other.
Here's the proof I came up with:
lemma bnd_ext_lim: assumes "AX" "limpt A p" "~intpt A p" shows "boundpt A p"
proof -
from `limpt A p` have "pX" by simp
moreover have "Nnhs p. (X-A)N{}"
proof
fix N assume "Nnhs p"
from `¬intpt A p` `A⊆X` have "pA ∨ ¬(Nnhs p. NA)" by auto
then consider "p(X-A)" | "(Nnhs p. ¬NA)" by auto
thus"(X-A)N{}" proof (cases)
case 1 then show ?thesis using ‹N ∈ nhs p› by fastforce
next
case 2 then have "¬NA" using ‹N ∈ nhs p› by blast
thus ?thesis using ‹N ∈ nhs p› by fastforce
qed
qed
moreover from `A⊆X` have "(X-A)X" by auto
ultimately have "limpt (X-A) p" by simp
thus "boundpt A p" using `limpt A p` boundpt_def by blast
qed
text ‹I'll let Isabelle prove to itself that the two cases are mutually exclusive:›
lemma lim_bnd_xor_int: assumes "limpt A p" shows "(boundpt A p)(intpt A p)"
using assms bnd_ext_lim boundpt_def by auto
text ‹Now we can show what we really wanted to show:›
corollary c426: (* cor 4.2.6 *)
assumes ax: "AX"
and ap: "p. boundpt A ppA"
shows "closed A"
proof -
have "p. limpt A ppA" proof
fix p assume "limpt A p"
consider (0) "boundpt A p"
| (1) "intpt A p"
using ‹limpt A p› lim_bnd_xor_int by auto
then show "pA" using ap intpt_def by auto
qed
thus "closed A" using ax t425b by simp
qed
text ‹❙‹COROLLARY 4.2.7›
In any topological space ‹(X,T)›, both ‹X› and ‹{}› are closed sets,
and both are empty sets.›
― "The first two statements can be proved directly from the definition of 'open':"
corollary open_empty: "open {}" using open_def by auto
corollary open_univ: "open X" using open_def by fastforce
― "Once we have those two, the others two are obvious:"
corollary closed_univ: "closed X" using open_empty by simp
corollary closed_empty: "closed {}" using open_univ by simp
end (* locale topspace *)
end (* theory TopSpace *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment