5 Topology

This chapter follows the book Topology without tears by Sydney A. Morris. It builds upon and extends the formalism in Grothendieck’s Schemes in Algebraic Geometry, which in turn builds upon A Case Study in Basic Algebra. You can import it from AFP (see 2.15)

The goal of topology is to generalize the definition of continuity. Intuitively we think of continuous functions as any functions that you can draw without taking the pen off the paper. The problem with relying on intuition is that here any many functions that look continuous but aren’t. For example sin(1/x) is not continuous while weierstrass function is.

Topology is ubiquitous in real, complex and functional analysis but also in many places where we wouldn’t expect it. For example it is possible to take derivatives of types.

5.1 Topological spaces

5.1.1 Topology

Topological space (S,τ) is a set S :: 'a set equipped with topology τ :: 'a set set (tau) such that

  1. The empty set {} and the set S both belong to τ.
  2. If U∈τ and V∈τ then U ∩ V∈τ.
  3. If F::'a set set is a family of subsets, such that all x∈F are in x∈τ, then the union ⋃x∈F. x is also a member of τ.

The members of τ are called open sets. Therefore we could paraphrase the axioms above as

  1. {} and S are open
  2. (only finite) intersection of open sets is open
  3. (possibly infinite) union of open sets is open
The term open set was invented as a generalization of open intervals. In the space of real numbers all sets of the form (a,b)={x∈ℝ | a < x < b} are open intervals.
A different notation is used in Isabelle

Brackets (a,b)={x∈ℝ | a < x < b} are a mathematical notation of open intervals. Actual Isabelle notation would be

definition greaterThanLessThan :: "'a => 'a => 'a set"  ("(1{_<..<_})") where
  "{l<..<u} == {l<..} Int {..<u}"

defined in Set_Interval and Real. You need to import them if you want to experiment

theory Test
  imports Main HOL.Real 
begin
value "x::real" (* "x" *)
value "{2..(4::nat)}" (* "{2, 3, 4}" *)
value "{2..(4::real)}" (* error! *)
end
To see why the error in last value, check out the hidden note under 2.12.4.1.

In general, open sets could be anything (for example sets of infinite strings that start with some prefix are open in Martin-Löf–Chaitin randomness which is the foundation of information theory and Kolmogorov complexity).

Topological spaces are defined In Isabelle as follows.

text ‹p 25, def 1.1.1›  (* You can find this in the book on page 25 *)
locale topological_space = fixes S :: "'a set" and is_open :: "'a set ⇒ bool"
  assumes open_space [simp, intro]: "is_open S"
    and open_imp_subset: "is_open U ⟹ U ⊆ S"
    and open_inter [intro]: "⟦is_open U; is_open V⟧ ⟹ is_open (U ∩ V)"
    and open_union [intro]: "⋀F::('a set) set. (⋀x. x ∈ F ⟹ is_open x) ⟹ is_open (⋃x∈F. x)"

Instead of a set τ we have a predicate is_open such that is_open U ⟹ U ⊆ S. The two definitions are equivalent because τ={U∈Pow S . is_open U} (recall that Pow is the power-set 2.12.5.2). Moreover we do not specify that {} is open because this fact already follows from open_union axiom.

context topological_space begin

text ‹p 25, def 1.1.1›
theorem open_empty [simp, intro]: "is_open {}"
  using open_union[of "{}"] by auto

If we can take unions over infinite sets, then clearly we can take finite unions.

lemma open_Un [continuous_intros, intro]: "is_open S ⟹ is_open T ⟹ is_open (S ∪ T)"
  using open_union [of "{S, T}"] by auto

The axiom open_inter only allows us to take intersections of two open sets. This means that we can take intersections over finite sets.

text ‹p 30, exercise 4›
lemma open_Inter [continuous_intros, intro]: "finite F ⟹ ∀T∈F. is_open T ⟹ is_open (S ∩ ⋂F)"
  apply(induction set: finite)
  apply(auto)
  apply(subst Set.Int_assoc[symmetric])
  apply(subst Set.Int_commute[symmetric])
  apply(subst Set.Int_assoc)
  apply(rule open_inter)
  by auto
A detailed proof 
text ‹p 30, exercise 4›
lemma open_Inter [continuous_intros, intro]: "finite F ⟹ ∀T∈F. is_open T ⟹ is_open (S ∩ ⋂F)"
  apply(induction set: finite)
  (* 
    1. Ball {} is_open ⟹ is_open (S ∩ ⋂ {})
    2. ⋀x F. finite F ⟹
           x ∉ F ⟹
           (Ball F is_open ⟹ is_open (S ∩ ⋂ F)) ⟹ Ball (insert x F) is_open ⟹ is_open (S ∩ ⋂ (insert x F))
  *)
   apply(simp)
  apply(simp)
  (* 1. ⋀x F. finite F ⟹ x ∉ F ⟹ is_open (S ∩ ⋂ F) ⟹ is_open x ∧ (∀x∈F. is_open x) ⟹ is_open (S ∩ (x ∩ ⋂ F)) *)
  apply(subst Set.Int_assoc[symmetric])
  (* 1. ⋀x F. finite F ⟹ x ∉ F ⟹ is_open (S ∩ ⋂ F) ⟹ is_open x ∧ (∀x∈F. is_open x) ⟹ is_open (S ∩ x ∩ ⋂ F) *)
  apply(subst Set.Int_commute[symmetric])
  (* 1. ⋀x F. finite F ⟹ x ∉ F ⟹ is_open (S ∩ ⋂ F) ⟹ is_open x ∧ (∀x∈F. is_open x) ⟹ is_open (x ∩ S ∩ ⋂ F) *)
  apply(subst Set.Int_assoc)
  (* 1. ⋀x F. finite F ⟹ x ∉ F ⟹ is_open (S ∩ ⋂ F) ⟹ is_open x ∧ (∀x∈F. is_open x) ⟹ is_open (x ∩ (S ∩ ⋂ F)) *)
  apply(rule open_inter)
  (* 
     1. ⋀x F. finite F ⟹ x ∉ F ⟹ is_open (S ∩ ⋂ F) ⟹ is_open x ∧ (∀x∈F. is_open x) ⟹ is_open x
     2. ⋀x F. finite F ⟹ x ∉ F ⟹ is_open (S ∩ ⋂ F) ⟹ is_open x ∧ (∀x∈F. is_open x) ⟹ is_open (S ∩ ⋂ F)
  *)
  by auto

An infinite intersection of open sets is not guaranteed to be open.

If for all x ∈ U there exists some open subset T ⊆ U containing x ∈ U then S must be open.

lemma openI:
  assumes "⋀x. x ∈ U ⟹ ∃T. is_open T ∧ x ∈ T ∧ T ⊆ U"
  shows "is_open U"
proof -
  have "is_open (⋃{T. is_open T ∧ T ⊆ U})" by auto
  moreover have "⋃{T. is_open T ∧ T ⊆ U} = U" by (auto dest!: assms)
  ultimately show "is_open U" by simp
qed

This holds true because we could take union of all Ts. The union of Ts must be open and equal U. Therefore U must be open.

5.1.2 Discrete topology

Discrete topology is a special case of topological space in which all subsets U ⊆ S are open

locale discrete_topology = topological_space +
  assumes open_discrete: "⋀U. U ⊆ S ⟹ is_open U"
Mind the context!

While all the theorems above lived in

context topological_space
begin
...
end
discrete topology is a new locale defined outside of it.

The opposite of discrete space is the indiscrete space in which the only open sets are the improper subsets of S

text ‹p 27, def 1.1.7›
locale indiscrete_topology = topological_space +
  assumes open_discrete: "⋀U. is_open U ⟹ U = {} ∨ U = S"

If all singleton sets are open then the space is discrete (which follows easily from openI theorem above)

text ‹p 29, def 1.1.9›
theorem singl_open_discr : 
  assumes tp:"topological_space S is_open"
  and sng:"⋀ x. x ∈ S ⟹ is_open {x}"
  shows "discrete_topology S is_open"
proof -
  interpret S: topological_space S is_open by fact
  from tp sng show ?thesis 
    apply(unfold_locales)
    apply(rule local.S.openI)
    by(auto)
qed

5.1.3 Open, closed and clopen sets

Closed set is defined to be a complement of an open set.

text ‹p 34, def 1.2.4›
definition is_closed :: "'a set ⇒ bool"
  where "is_closed U ≡ U ⊆ S ∧ is_open (S ∖ U)"
Equivalent definitions used by simp 
lemma open_closed[simp]: "U ⊆ S ⟹ is_closed (S ∖ U) ⟷ is_open U"
  by(simp add: is_closed_def double_diff)
  
lemma closed_open: "U ⊆ S ⟹ is_closed U ⟷ is_open (S ∖ U)"
  by(simp add: is_closed_def double_diff)

All properties of open sets also hold for closed sets if we swap unions with intersections. This follows from De Morgan’s law.

Mind the context!

All theorems in this section as well as definition of is_closed live in topological_space context.

context topological_space
begin
...
end

The empty set is closed.

text ‹p 34, def 1.2.5 i›
theorem closed_empty [simp, intro]: "is_closed {}"
  by(unfold is_closed_def) (auto)

The space S is closed itself

text ‹p 34, def 1.2.5 i›
theorem closed_space [simp, intro]: "is_closed S"
  by(unfold is_closed_def) (auto)

Infinite intersection is closed

text ‹p 34, def 1.2.5 ii›
lemma closed_Inter [continuous_intros, intro]: "⋀F::('a set) set. (⋀x. x ∈ F ⟹ is_closed x) ⟹ is_closed (S ∩ ⋂F)"
  unfolding is_closed_def by(auto simp add: Diff_dist[symmetric] Diff_Int_nAry simp del: Complete_Lattices.UN_simps)
More detailed proof.

Notice that the additional intersection S ∩ is necessary in is_closed (S ∩ ⋂F) because if F is an empty familiy of sets (F={}) then the quantifier ⋂F returns the full set ⋂F=UNIV which need not be a subset of S. In mathematical textbooks this would often be left implicit. In formal logic, we have to be extra precise.

text ‹p 34, def 1.2.5 ii›
lemma closed_Inter [continuous_intros, intro]: "⋀F::('a set) set. (⋀x. x ∈ F ⟹ is_closed x) ⟹ is_closed (S ∩ ⋂F)"
  unfolding is_closed_def
  (* 1. ⋀F. (⋀x. x ∈ F ⟹ x ⊆ S ∧ is_open (S∖x)) ⟹ S ∩ ⋂ F ⊆ S ∧ is_open (S∖(S ∩ ⋂ F)) *)
  apply(rule conjI)
   (* 
     1. ⋀F. (⋀x. x ∈ F ⟹ x ⊆ S ∧ is_open (S∖x)) ⟹ S ∩ ⋂ F ⊆ S
     2. ⋀F. (⋀x. x ∈ F ⟹ x ⊆ S ∧ is_open (S∖x)) ⟹ is_open (S∖(S ∩ ⋂ F))
   *)
   apply(simp) (* solves first subgoal *)
  apply(subst Diff_dist[symmetric]) 
  (* 1. ⋀F. (⋀x. x ∈ F ⟹ x ⊆ S ∧ is_open (S∖x)) ⟹ is_open (S∖⋂ F ∪ (S∖S)) *)
  apply(subst Diff_cancel)
  (* 1. ⋀F. (⋀x. x ∈ F ⟹ x ⊆ S ∧ is_open (S∖x)) ⟹ is_open (S∖⋂ F ∪ {}) *)
  apply(subst Set.Un_empty_right)
  (* 1. ⋀F. (⋀x. x ∈ F ⟹ x ⊆ S ∧ is_open (S∖x)) ⟹ is_open (S∖⋂ F) *)
  apply(subst Diff_Int_nAry)
  (* 1. ⋀F. (⋀x. x ∈ F ⟹ x ⊆ S ∧ is_open (S∖x)) ⟹ is_open (⋃V∈F . S ∖ V) *)
  apply(rule open_union)
  (* 1. ⋀F. (⋀x. x ∈ F ⟹ x ⊆ S ∧ is_open (S∖x)) ⟹ x ∈ complement_in_of S ` F ⟹ is_open x *)
  by auto

Union of closed sets is closed

text ‹p 34, def 1.2.5 iii›
lemma closed_Un [continuous_intros, intro]: "is_closed U ⟹ is_closed V ⟹ is_closed (U ∪ V)"
  by(unfold is_closed_def) (simp add:Set.Diff_Un open_inter)
Sets that are both closed and open are called clopen
Note By finding clopen sets it is possible to detect disconnected components, which you can intuitively think of like “cracks” in the space. If {} and UNIV are the only clopen sets, then there are no “cracks”. 
text ‹p 36, def 1.2.6›
definition is_clopen :: "'a set ⇒ bool"
  where "is_clopen U ≡ is_open U ∧ is_closed U"

Difference of open and closed set is open

lemma open_Diff [continuous_intros, intro]: 
  assumes ou:"is_open U"
    and cv: "is_closed V"
  shows "is_open (U ∖ V)"
Proof 
proof -
  from ou have us: "U ⊆ S" by (rule open_imp_subset)
  from cv have osv: "is_open (S∖V)" by (unfold is_closed_def) simp
  from osv ou have svu: "is_open ((S∖V) ∩ U)" by (rule open_inter)
  from us svu show "is_open (U∖V)" by (subst Diff_eq_on[OF us]) (subst Set.Int_commute)
qed

Difference of closed and open set is closed

lemma closed_Diff [continuous_intros, intro]: 
  assumes cu:"is_closed U" 
    and ov: "is_open V" 
  shows "is_closed (U ∖ V)"
Proof 
proof -
  from cu have ou: "U ⊆ S" by (unfold is_closed_def) simp
  from cu have osu: "is_open (S∖U)" by (unfold is_closed_def) simp
  from osu ov have suv: "is_open ((S∖U) ∪ V)" by(rule open_Un)
    from suv have osu: "is_closed (S∖(S∖U ∪ V))" 
    using open_imp_subset[OF ov]
    apply(subst is_closed_def)
    apply(subst double_diff)
    by(auto)
  from osu have ssuv: "is_closed ((S∖(S∖U))∖V)" by(subst diff_as_union)
  from ssuv show "is_closed (U ∖ V)" 
    by(subst double_diff[OF ou, symmetric])
qed

5.1.4 Finite-closed topology

A topological space is called cofinite if closed sets are exactly those sets that are finite

text ‹p 39, def 1.3.1›
locale cofinite_topology = topological_space +
  assumes finite_is_closed: "⋀U. ⟦ U⊆ S ; finite U ⟧ ⟹ is_closed U"
  assumes closed_is_finite: "⋀U. is_closed U ⟹ finite U"

For definitions 1.3.4, 1.3.5, 1.3.6 from page 41 of the book, see 3.1 and 2.12.5.3.

5.1.5 Basis

Topological space can be generated by a basis S which is a set of subsets 'a set set.

inductive generate_topology :: "'a set set ⇒ 'a set ⇒ bool" for S :: "'a set set"
  where
    UNIV: "generate_topology S UNIV"
  | Int: "generate_topology S (a ∩ b)" if "generate_topology S a" and "generate_topology S b"
  | UN: "generate_topology S (⋃K)" if "(⋀k. k ∈ K ⟹ generate_topology S k)"
  | Basis: "generate_topology S s" if "s ∈ S"

Defining open = generate_topology B would mean that open sets are inductively defined, that is, all sets in B are open (Basis) and UNIV is open and any union (‘UN’) and intersection (‘Int’) of open sets is open. The proof that generate_topology indeed yields a topological space is given as follows.

lemma topological_space_generate_topology: "class.topological_space (generate_topology S)"
  by standard (auto intro: generate_topology.intros)

An example of generated topology is the order_topology in the next section.

5.2 Order and separation

5.2.1 Order topology

Every set equipped with order (2.12.1.2) can be easily turned into a topological space by assuming open_generated_order.

class order_topology = order + "open" +
  assumes open_generated_order: "open = generate_topology (range (λa. {..< a}) ∪ range (λa. {a <..}))"
This is sometimes called a natural topology. On a real line, this would mean that all half-open intervals are open sets and any union or intersection of open intervals is an open set too. This includes all open intervals because an intersection of two half-open intervals {..< a} and {b <..} yields an open interval {b <..< a}.
Recall the meaning of this notation 
definition lessThan    :: "'a => 'a set" ("(1{..<_})") where
  "{..<u} == {x. x < u}"

definition atMost      :: "'a => 'a set" ("(1{.._})") where
  "{..u} == {x. x ≤ u}"

definition greaterThan :: "'a => 'a set" ("(1{_<..})") where
  "{l<..} == {x. l<x}"

definition atLeast     :: "'a => 'a set" ("(1{_..})") where
  "{l..} == {x. l≤x}"
  
definition greaterThanLessThan :: "'a => 'a => 'a set"  ("(1{_<..<_})") where
  "{l<..<u} == {l<..} Int {..<u}"

definition atLeastLessThan :: "'a => 'a => 'a set"      ("(1{_..<_})") where
  "{l..<u} == {l..} Int {..<u}"

definition greaterThanAtMost :: "'a => 'a => 'a set"    ("(1{_<.._})") where
  "{l<..u} == {l<..} Int {..u}"

definition atLeastAtMost :: "'a => 'a => 'a set"        ("(1{_.._})") where
  "{l..u} == {l..} Int {..u}"

We can use subclass keyword to tell Isabelle that every order_topology is a topological_space

class order_topology = order + "open" +
  assumes open_generated_order: "open = generate_topology (range (λa. {..< a}) ∪ range (λa. {a <..}))"
begin

subclass topological_space
  unfolding open_generated_order
  by (rule topological_space_generate_topology)
  
end

The simplest example of topological space is bool which is also a discrete topology

class discrete_topology = topological_space +
  assumes open_discrete: "⋀A. open A"

instance discrete_topology < t2_space
proof
  fix x y :: 'a
  assume "x ≠ y"
  then show "∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}"
    by (intro exI[of _ "{_}"]) (auto intro!: open_discrete)
qed

instantiation bool :: linorder_topology
begin

A notable special case of order_topology is

class linorder_topology = linorder + order_topology

In linorder_topology the intervals {..< a} and {a <..} really are intervals. In order_topology with partial order, the sets {a <..< b} may instead look like convex sublattices (when the topological space is also a lattice 2.12.2).

5.2.2 T0, T1 and T2 spaces

Topological spaces only tell us what operations can be performed on open sets but there are no axioms that would say anything about individual elements of those sets. Therefore, to obtain more interesting properties it is necessary to include additional axioms relating elements and sets. These are called separation axioms.

The first one says that for any two distinct points x and y there exists an open set containing one but not the other.

class t0_space = topological_space +
  assumes t0_space: "x ≠ y ⟹ ∃U. open U ∧ ¬ (x ∈ U ⟷ y ∈ U)"

This means that all points can be topologically distinguishable from one another. Intuitively you may think of it as if there were two points so close to each other that they seem to overlap but if you zoom in close enough then you will eventually spot two distinguished points. In spaces that are not t0_space you might zoom-in forever and the points would always “overlap” (at least from topological point of view).

Spaces that satisfy this axiom are called T0 spaces or Kolmogorov spaces.

The next axiom characterizes T1 spaces

class t1_space = topological_space +
  assumes t1_space: "x ≠ y ⟹ ∃U. open U ∧ x ∈ U ∧ y ∉ U"

This axiom is nearly identical to T0 but now there must exist one open set containing x but not y and another one containing y but not x (if you replaced and with or then this would be the T0 axiom). Every T1 space is T0 but not every T0 is T1.

instance t1_space ⊆ t0_space (* every T1 space is T0 *)
  by standard (fast dest: t1_space)

The T1 spaces guarantee that every singleton set {x} must be closed because you can take the union of all open sets not containing point x.


context t1_space begin

lemma separation_t1: "x ≠ y ⟷ (∃U. open U ∧ x ∈ U ∧ y ∉ U)"
  using t1_space[of x y] by blast

lemma closed_singleton [iff]: "closed {a}"
proof -
  let ?T = "⋃{S. open S ∧ a ∉ S}"
  have "open ?T"
    by (simp add: open_Union)
  also have "?T = - {a}"
    by (auto simp add: set_eq_iff separation_t1)
  finally show "closed {a}"
    by (simp only: closed_def)
qed

end

The axioms of T1 and T0 spaces are rather weak. It is at T2 where things start to get interesting.

class t2_space = topological_space +
  assumes hausdorff: "x ≠ y ⟹ ∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}"

This axiom is similar to T1 but it additionally guarantees that the two open sets are disjoint. T2 spaces are commonly called Hausdorff. Every Hausdorff space is a T1 space.

instance t2_space ⊆ t1_space
  by standard (fast dest: hausdorff)

lemma (in t2_space) separation_t2: "x ≠ y ⟷ (∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {})"
  using hausdorff [of x y] by blast

lemma (in t0_space) separation_t0: "x ≠ y ⟷ (∃U. open U ∧ ¬ (x ∈ U ⟷ y ∈ U))"
  using t0_space [of x y] by blast

Observe that every discrete topology is T2.

instance discrete_topology < t2_space
proof
  fix x y :: 'a
  assume "x ≠ y"
  then show "∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}"
    by (intro exI[of _ "{_}"]) (auto intro!: open_discrete)
qed

5.2.3 Linear order and separation axioms

We can find many interesting relations between topologies with total order (linorder_topology) and the separation axioms that they satisfy. First notice that these closed intervals are indeed closed sets.


lemma closed_atMost [continuous_intros, simp]: "closed {..a}"
  for a :: "'a::linorder_topology"
  by (simp add: closed_open)

lemma closed_atLeast [continuous_intros, simp]: "closed {a..}"
  for a :: "'a::linorder_topology"
  by (simp add: closed_open)

lemma closed_atLeastAtMost [continuous_intros, simp]: "closed {a..b}"
  for a b :: "'a::linorder_topology"
proof -
  have "{a .. b} = {a ..} ∩ {.. b}"
    by auto
  then show ?thesis
    by (simp add: closed_Int)
qed

This is because the complement of {a .. } is an open interval {..< a} and recall that order_topology is generated by

open = generate_topology (range (λa. {..< a}) ∪ range (λa. {a <..}))

In any partially ordered set we can show that for any two distinct points x<y there exist two open “cones” {b <..} and {..< a} containing each of the points x ∈ {..< a} and y ∈ {b <..} but which are disjoint {..< a} ∩ {b <..} = {}. The proof follows by considering cases when there exists z between x and y or not.

lemma (in order) less_separate:
  assumes "x < y"
  shows "∃a b. x ∈ {..< a} ∧ y ∈ {b <..} ∧ {..< a} ∩ {b <..} = {}"
proof (cases "∃z. x < z ∧ z < y")
  case True
  then obtain z where "x < z ∧ z < y" ..
  then have "x ∈ {..< z} ∧ y ∈ {z <..} ∧ {z <..} ∩ {..< z} = {}"
    by auto
  then show ?thesis by blast
next
  case False
  with ‹x < y› have "x ∈ {..< y}" "y ∈ {x <..}" "{x <..} ∩ {..< y} = {}"
    by auto
  then show ?thesis by blast
qed

This looks a lot like separation axiom of Hausdorff space. Indeed we have

instance linorder_topology ⊆ t2_space
proof
  fix x y :: 'a
  show "x ≠ y ⟹ ∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}"
    using less_separate [of x y] less_separate [of y x]
    by (elim neqE; metis open_lessThan open_greaterThan Int_commute)
qed

5.2.4 Instances of topologies

The bool type is the simplest example of a linearly-ordered topological space

instantiation bool :: linorder_topology
begin

definition open_bool :: "bool set ⇒ bool"
  where "open_bool = generate_topology (range (λa. {..< a}) ∪ range (λa. {a <..}))"

instance
  by standard (rule open_bool_def)

end

and it is also discrete

instance bool :: discrete_topology
proof
  fix A :: "bool set"
  have *: "{False <..} = {True}" "{..< True} = {False}"
    by auto
  have "A = UNIV ∨ A = {} ∨ A = {False <..} ∨ A = {..< True}"
    using subset_UNIV[of A] unfolding UNIV_bool * by blast
  then show "open A"
    by auto
qed

instantiation nat :: linorder_topology
begin

The same holds for nat and int. Textbooks such as “Topology without tears” have the privilege of jumping straight to Euclidean topology on real numbers. For us reaching the definition of real numbers requires a lot more involvement and preparation. First we would need to understand Cauchy sequences and before that we need to cover neighborhoods and limit points. For now all the topologies we can instantiate are discrete.

5.3 Neighborhoods and filters

Isabelle defines topological spaces using open sets. There exist several equivalent definitions and one of them involves filters. Filters are not covered directly in “Topology without tears” (but are mentioned in the appendix). We have to cover them because they will make working with neighborhoods a lot easier.

5.3.1 Filters

Recall (5.1.1) that open:: 'a set ⇒ bool was a predicate. With set comprehension it could be turned into the set {x . open x} :: 'a set set of open subsets. The distinction between set and predicate is blurry. Indeed, the axiomatization of set ((set-def)) states explicitly the one-to-one correspondence between sets and predicates. Therefore, the definition of filter looks as follows.

locale is_filter =
  fixes F :: "('a ⇒ bool) ⇒ bool"
  assumes True: "F (λx. True)"
  assumes conj: "F (λx. P x) ⟹ F (λx. Q x) ⟹ F (λx. P x ∧ Q x)"
  assumes mono: "∀x. P x ⟶ Q x ⟹ F (λx. P x) ⟹ F (λx. Q x)"
This definition comes from old times before Isabelle had set.
Correspondence between sets and predicates

The type 'a ⇒ bool is a predicate, which might as well be thought of as 'a set. Then ('a ⇒ bool) ⇒ bool is like a set of subsets 'a set set. Hence, filter F is a set of subsets of the topological space 'a just like τ. Unlike τ the axioms are different. The conj says that for any two sets P and Q belonging to F, their intersection is also in F. This axiom could have been equivalently written as

assumes conj: "P ∈ F ∧ Q ∈ F ⟹ Q ∩ P ∈ F"

The expression F (λx. P x) could be simplified to F P (using eta reduction of lambda calculus) and then reformulated using set notation P ∈ F.

A similar reasoning allows us to rewrite mono into a more readable form

assumes mono: "P ⊆ Q ∧ P ∈ F ⟹ Q ∈ F"

The (λx. True) is the definition of the full set UNIV.

assumes True: "UNIV ∈ F"

In modern Isabelle it could be written as follows.

locale `is_filter =
  fixes F :: "'a set set"
  assumes True: "UNIV ∈ F"
  assumes conj: "P ∈ F ∧ Q ∈ F ⟹ Q ∩ P ∈ F"
  assumes mono: "P ⊆ Q ∧ P ∈ F ⟹ Q ∈ F"

Fortunately the notation doesn’t matter because the following typedef turns the is_filter predicate into a set. Then we don’t need to use is_filter anymore.

typedef 'a filter = "{F :: ('a ⇒ bool) ⇒ bool. is_filter F}"
proof
  show "(λx. True) ∈ ?filter" by (auto intro: is_filter.intro)
qed
Important note: proper vs improper filters The definition above is different from the one in “Topology without tears”. Usually mathematicians would use axiom {} ∉ F instead of UNIV ∈ F. A filter that contains {} is called an improper filter. We can always assume {} ∉ F later on in proofs where it matters but there are also many proofs that would apply even to improper filters. Therefore Isabelle’s definition is more general and flexible than that in textbooks. Also note that the True axiom is necessary because without it, it would be possible to define F P = False for all P (or in set theoretic notation F = {}) and then the axioms conj and mono would hold vacuously. Lack of True would render most proofs impossible but if {} ∉ F was used in place of True then UNIV ∈ F would follow from mono.

5.3.2 Eventually