Instantly share code, notes, and snippets.

# tangentstorm/TopSpace.thy Last active Jul 11, 2018

 (* Topological Spaces Based on "A Bridge to Advanced Mathematics" by Dennis Sentilles Translated to Isar by Michal J Wallace *) theory TopSpace imports Main begin text ‹A 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 text ‹A set N∈T which contains p∈X is called a neighborhood of p.› definition nhs :: "'a ⇒ ('a set) set" where [simp]: "nhs p ≡ {N∈T. p∈N}" text ‹If ‹A⊆X› in topological space ‹(X,T)›, then ‹p∈X› is called a ❙‹limit point› of ‹A› if the intersection of every neighborhood of ‹p› with ‹A› is non-empty. In loose geometrical terms, ‹p› is either a point in ‹A› or as close as possible to ‹A› without 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) ≠ {})" text ‹If ‹A⊂X› in topological space ‹(X,T)›, then ‹x∈X› is called an ❙‹interior point› of ‹A› if at least one neighborhood of ‹x› is contained entirely within ‹A›.› 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)" text ‹THEOREM 4.2.5: A set ‹A∈X› in 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 "p ∈ A" proof (rule ccontr) assume "p∉A" 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 "p∈N" and "N∈T" and "N⊆(X-A)" by auto then have "N∩A={}" by auto ― ‹which contradicts the definition of a limit point.› moreover have "N∩A≠{}" 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 "A⊆X" "x∈X" and "¬(limpt A x)" obtains N where "N∈nhs x" and "N∩A={}" proof - ― "Start with the (negated) definition of ‹limpt A x›" from limpt_def have "¬(limpt A x) ≡ ¬(A⊆X ∧ x∈X ∧ (∀N∈nhs x. (A∩N) ≠ {}))" by simp ― "Distributing ¬ over ∧ gives us three possibilities …" also have "… ≡ ¬(A⊆X) ∨ (x∉X) ∨ (∃N∈nhs x. A∩N={})" by simp ― "… But our assumptions rule out the first two." finally have "… ≡ ∃N∈nhs x. A∩N = {}" using assms by auto with `¬(limpt A x)` obtain N where "N∈nhs x" and "N∩A={}" 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: "A⊆X" and a1: "∀p. limpt A p ⟶ p∈A" shows "closed A" ― ‹Quoting Sentilles here (replacing his syntax with isar's and using my variable names:› ― ‹"To show ‹A› is closed, we must argue that ‹X-A› is open."› ― ‹"That is, that any point of ‹X-A› is an interior point of ‹X-A›."› ― ‹"Suppose ‹x∈X-A›. Then ‹x∉A›."› ― ‹"Since ‹A› contains all its limit points, then ‹x› is not a limit point of ‹A›."› ― ‹"By [‹limpt_def›] this means there is a neighborhood ‹N∈T› of ‹x› whose intersection with ‹A› is empty. In other words, ‹N⊆(X-A)›."› ― ‹"But this means ‹X-A› is 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 "x∉A" by auto have "¬(limpt A x)" using a1 ‹x∉A› by auto with `x ∈ X-A` obtain N where "N∈nhs x" and "N∩A={}" using a0 non_limpt_nh by blast hence "N⊆X-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 "A⊆X" "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 "A⊆X" "limpt A p" "~intpt A p" shows "boundpt A p" proof - from `limpt A p` have "p∈X" by simp moreover have "∀N∈nhs p. (X-A)∩N≠{}" proof fix N assume "N∈nhs p" from `¬intpt A p` `A⊆X` have "p∉A ∨ ¬(∃N∈nhs p. N⊆A)" by auto then consider "p∈(X-A)" | "(∀N∈nhs p. ¬N⊆A)" by auto thus"(X-A)∩N≠{}" proof (cases) case 1 then show ?thesis using ‹N ∈ nhs p› by fastforce next case 2 then have "¬N⊆A" 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: "A⊆X" and ap: "∀p. boundpt A p ⟶ p∈A" shows "closed A" proof - have "⋀p. limpt A p ⟶ p∈A" 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 "p∈A" 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 *)
to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.