# 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

- The empty set
`{}`

and the set`S`

both belong to`τ`

. - If
`U∈τ`

and`V∈τ`

then`U ∩ V∈τ`

. - 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

`{}`

and`S`

are open- (only finite) intersection of open sets is open
- (possibly infinite) union of open sets is open

*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 `T`

s. The union of `T`

s 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`

.