TopSpace.thy

(* 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 *)