# Theory Topology

```(*  Title:      Topology.thy
Author:     Stefan Friedrich
Maintainer: Stefan Friedrich
*)

section ‹A bit of general topology›

theory Topology
imports "HOL-Library.FuncSet"
begin

text‹
This theory gives a formal account of basic notions of general
topology as they can be found in various textbooks, e.g. in
\<^cite>‹"mccarty67:_topol"› or in \<^cite>‹"querenburg01:_mengen_topol"›.
The development includes open and closed sets, neighbourhoods, as
well as closure, open core, frontier, and adherent points of a set,
dense sets, continuous functions, filters, ultra filters,
convergence, and various separation axioms.
›

text‹We use the theory on ``Pi and Function Sets'' by Florian
Kammueller and Lawrence C Paulson.›

subsection‹Preliminaries›

lemma seteqI:
"⟦ ⋀x. x∈A ⟹ x∈B; ⋀x. x∈B ⟹ x∈A ⟧ ⟹ A = B"
by auto

lemma subset_mono: "A ⊆ B ⟹ M ⊆ A ⟶ M ⊆ B"
by auto

lemma diff_diff:
"C - (A - B) = (C - A) ∪ (C ∩ B)"
by blast

lemma diff_diff_inter: "⟦B ⊆ A; B ⊆ X⟧ ⟹ (X - (A - B)) ∩ A = B"
by auto

lemmas diffsimps = double_diff Diff_Un vimage_Diff
Diff_Int_distrib Diff_Int

lemma vimage_comp:
"f: A → B ⟹ A ∩ (f -` B ∩ f -` g -` m)= A ∩ (g ∘ f) -` m "
by (auto dest: funcset_mem)

lemma funcset_comp:
"⟦ f : A → B; g : B → C ⟧ ⟹ g ∘ f : A → C"
by (auto intro!: funcsetI dest!: funcset_mem)

subsection‹Definition›

text‹A topology is defined by a set of sets (the open sets)
that is closed under finite intersections and infinite unions.›

type_synonym 'a top = "'a set set"

definition
carr :: "'a top ⇒ 'a set" ("carrierı") where
"carr T = ⋃T"

definition
is_open :: "'a top ⇒ 'a set ⇒ bool" ("_ openı" [50] 50) where
"is_open T s ⟷ s ∈ T"

locale carrier =
fixes T :: "'a top" (structure)

lemma (in carrier) openI:
"m ∈ T ⟹ m open"

lemma (in carrier) openE:
"⟦ m open; m ∈ T ⟹ R ⟧ ⟹ R"
by (auto simp: is_open_def)

lemma (in carrier) carrierI [intro]:
"⟦ t open; x ∈ t ⟧ ⟹ x ∈ carrier"
by (auto simp: is_open_def carr_def)

lemma (in carrier) carrierE [elim]:
"⟦ x ∈ carrier;
⋀t. ⟦ t open; x ∈ t ⟧ ⟹ R
⟧ ⟹ R"
by (auto simp: is_open_def carr_def)

lemma (in carrier) subM:
"⟦ t ∈ M; M ⊆ T ⟧ ⟹ t open"
by (auto simp: is_open_def)

lemma (in carrier) topeqI [intro!]:
fixes S (structure)
shows "⟦ ⋀m. m open⇘T⇙ ⟹ m open⇘S⇙;
⋀m. m open⇘S⇙ ⟹ m open⇘T⇙ ⟧
⟹ T = S"
by (auto simp: is_open_def)

locale topology = carrier T for T (structure) +
assumes Int_open [intro!]:   "⟦ x open; y open⟧ ⟹ x ∩ y open"
and     union_open [intro]: "∀m ∈ M. m open ⟹ ⋃ M open"

lemma topologyI:
"⟦ ⋀ x y. ⟦ is_open T x; is_open T y⟧ ⟹ is_open T (x ∩ y);
⋀ M. ∀ m ∈ M. is_open T m ⟹ is_open T (⋃ M)
⟧ ⟹ topology T"
by (auto simp: topology_def)

lemma (in topology) Un_open [intro!]:
assumes abopen: "A open" "B open"
shows "A ∪ B open"
proof-
have "⋃{A, B} open" using abopen
by fast
thus ?thesis by simp
qed

text‹Common definitions of topological spaces require that the empty
set and the carrier set of the space be open. With our definition,
however, the carrier is implicitly given as the union of all open
sets; therefore it is trivially open. The empty set is open by the
laws of HOLs typed set theory.›

lemma (in topology) empty_open [iff]: "{} open"
proof-
have "⋃{} open" by fast
thus ?thesis by simp
qed

lemma (in topology) carrier_open [iff]: "carrier open"
by (auto simp: carr_def intro: openI)

lemma (in topology) open_kriterion:
assumes t_contains_open: "⋀ x. x∈t ⟹ ∃t'. t' open ∧ x∈t' ∧ t'⊆t"
shows "t open"
proof-
let ?M = "⋃x∈t. {t'. t' open ∧ x∈t' ∧ t'⊆t}"
have "∀ m ∈ ?M. m open" by simp
hence  "⋃?M open" by auto
moreover have "t = ⋃?M"
by (auto dest!: t_contains_open)
ultimately show ?thesis
by simp
qed

text‹We can obtain a topology from a set of basic open sets by
closing the set under finite intersections and arbitrary unions.›

inductive_set
topo :: "'a set set ⇒ 'a top"
for B :: "'a set set"
where
basic [intro]: "x ∈ B ⟹ x ∈ topo B"
| inter [intro]: "⟦ x ∈ topo B; y ∈ topo B ⟧ ⟹ x ∩ y ∈ topo B"
| union [intro]: "(⋀x. x ∈ M ⟹ x ∈ topo B) ⟹ ⋃M ∈ topo B"

locale topobase = carrier T for B and T (structure) +
defines "T ≡ topo B"

lemma (in topobase) topo_open:
"t open = (t ∈ topo B)"
by (auto simp: T_def is_open_def)

lemma (in topobase)
basic [intro]: "t ∈ B ⟹ t open" and
inter [intro]: "⟦x open; y open ⟧ ⟹ (x ∩ y) open" and
union [intro]: "(⋀t. t∈M ⟹ t open) ⟹ ⋃M open"
by (auto simp: topo_open)

lemma (in topobase) topo_induct
[case_names basic inter union, induct set: topo, consumes 1]:
assumes opn: "x open"
and bas: "⋀x. x ∈ B ⟹ P x"
and int: "⋀x y. ⟦x open; P x; y open; P y⟧ ⟹ P (x ∩ y)"
and uni: "⋀M. (∀t∈M. t open ∧ P t) ⟹ P (⋃M)"
shows "P x"
proof-
from opn have "x ∈ topo B" by (simp add: topo_open)
thus ?thesis
by induct (auto intro: bas int intro!:uni simp: topo_open)
qed

lemma topo_topology [iff]:
"topology (topo B)"
by (auto intro!: union topologyI simp: is_open_def)

lemma topo_mono:
assumes asubb: "A ⊆ B"
shows  "topo A ⊆ topo B"
proof
fix m assume mintopoa: "m ∈ topo A"
hence "A ⊆ B ⟶ m ∈ topo B"
by (rule topo.induct) auto
with asubb show "m ∈ topo B"
by auto
qed

lemma topo_open_imp:
fixes A and S (structure) defines "S ≡ topo A"
fixes B and T (structure) defines "T ≡ topo B"
shows "⟦ A ⊆ B; x open⇘S⇙ ⟧ ⟹ x open⇘T⇙" (is "PROP ?P")
proof -
interpret A_S: topobase A S by fact
interpret topobase B T by fact
show "PROP ?P" by (auto dest: topo_mono iff: A_S.topo_open topo_open)
qed

lemma (in topobase) carrier_topo: "carrier = ⋃B"
proof
show "carrier ⊆ ⋃B"
proof
fix x assume "x ∈ carrier"
then obtain t where "t open" and "x ∈ t" ..
thus "x ∈ ⋃B" by (induct, auto)
qed
qed (auto iff: topo_open)

text‹Topological subspace›

locale subtopology = carrier S + carrier T for S (structure) and T (structure) +
assumes subtop[iff]: "s open = (∃t. t open⇘T⇙ ∧ s = t ∩ carrier)"

lemma subtopologyI:
fixes S (structure)
fixes T (structure)
assumes H1: "⋀s. s open ⟹ ∃t. t open⇘T⇙ ∧ s = t ∩ carrier"
and     H2: "⋀t. t open⇘T⇙ ⟹ t ∩ carrier open"
shows "subtopology S T"
by (auto simp: subtopology_def intro: assms)

lemma (in subtopology) subtopologyE [elim]:
assumes major: "s open"
and     minor: "⋀t. ⟦ t open⇘T⇙; s = t ∩ carrier ⟧ ⟹ R"
shows "R"
using assms by auto

lemma (in subtopology) subtopI [intro]:
"t open⇘T⇙ ⟹ t ∩ carrier open"
by auto

lemma (in subtopology) carrier_subset:
"carrier⇘S⇙ ⊆ carrier⇘T⇙"
by auto

lemma (in subtopology) subtop_sub:
assumes "topology T"
assumes carrSopen: "carrier⇘S⇙ open⇘T⇙"
and s_open: "s open⇘S⇙"
shows "s open⇘T⇙"
proof -
interpret topology T by fact
show ?thesis using assms by auto
qed

lemma (in subtopology) subtop_topology [iff]:
assumes "topology T"
shows "topology S"
proof -
interpret topology T by fact
show ?thesis proof (rule topologyI)
fix u v assume uopen: "u open" and vopen: "v open"
thus "u ∩ v open"  by (auto simp add: Int_ac)
next
fix M assume msub: "∀m∈M. m open"
let ?N = "{x. x open⇘T⇙ ∧ x ∩ carrier ∈ M}"
have "⋃?N open⇘T⇙" by auto
hence "⋃?N ∩ carrier open" ..
moreover have "⋃?N  ∩ carrier = ⋃M"
proof
show "⋃M ⊆ ⋃?N ∩ carrier"
proof
fix x assume "x ∈ ⋃M"
then obtain s where sinM: "s ∈ M" and xins: "x ∈ s"
by auto
from msub sinM have s_open: "s open" ..
then obtain t
where t_open: "t open⇘T⇙" and s_inter: "s = t ∩ carrier" by auto
with xins have xint: "x∈t" and xpoint: "x ∈ carrier" by auto
moreover
from t_open s_inter sinM have "t ∈ ?N" by auto
ultimately show "x ∈ ⋃?N ∩ carrier"
by auto
qed
qed auto
finally show "⋃M open" .
qed
qed

lemma  subtop_lemma:
fixes A and S (structure) defines "S ≡ topo A"
fixes B and T (structure) defines "T ≡ topo B"
assumes  Asub: "A = (⋃t∈B. { t ∩ ⋃A })"
shows   "subtopology S T"
proof -
interpret A_S: topobase A S by fact
interpret topobase B T by fact
show ?thesis proof (rule subtopologyI)
fix s assume "s open⇘S⇙"
thus "∃t. t open⇘T⇙ ∧ s = t ∩ carrier"
proof induct
case (basic s) with Asub
obtain t where tB: "t ∈ B" and stA: "s = t ∩ ⋃A" by blast
thus ?case by (auto simp: A_S.carrier_topo)
next case (inter s t) thus ?case by auto
next case (union M)
let ?N = "⋃{u. u open⇘T⇙ ∧ (∃m∈M. m = u ∩ carrier)}"
have "?N open⇘T⇙" and "⋃M = ?N ∩ carrier" using union by auto
thus ?case by auto
qed
next
fix t assume "t open⇘T⇙"
thus "t ∩ carrier open"
proof induct
case (basic u) with Asub show ?case
by (auto simp: A_S.carrier_topo)
next case (inter u v)
hence "(u ∩ carrier) ∩ (v ∩ carrier) open" by auto
thus ?case  by (simp add: Int_ac)
next case (union M)
let ?N = "⋃{s. ∃m∈M. s = m ∩ carrier}"
from union have "?N open" and "?N = ⋃M ∩ carrier" by auto
thus ?case by auto
qed
qed
qed

text‹Sample topologies›

definition
trivial_top :: "'a top" where
"trivial_top = {{}}"

definition
discrete_top :: "'a set ⇒ 'a set set" where
"discrete_top X = Pow X"

definition
indiscrete_top :: "'a set ⇒ 'a set set" where
"indiscrete_top X = {{}, X}"

definition
order_base :: "('a::order) set ⇒ 'a set set" where
"order_base A = (⋃x∈A. {{y. y ∈ A ∧ x ≤ y}})"

definition
order_top :: "('a::order) set ⇒ 'a set set" where
"order_top X = topo(order_base X)"

locale trivial = carrier +
defines "T ≡ {{}}"

lemma (in trivial) open_iff [iff]:
"m open = (m = {})"
by (auto simp: T_def is_open_def)

lemma trivial_topology:
fixes T (structure) defines "T ≡ {{}}"
shows "topology T"
proof -
interpret trivial T by fact
show ?thesis by (auto intro: topologyI)
qed

lemma empty_carrier_implies_trivial:
fixes S (structure) assumes "topology S"
fixes T (structure) defines "T ≡ {{}}"
shows "carrier = {} ⟹ S = T" (is "PROP ?P")
proof -
interpret topology S by fact
interpret trivial T by fact
show "PROP ?P" by auto
qed

locale discrete = carrier T for X and T (structure) +
defines "T ≡ discrete_top X"

lemma (in discrete) carrier:
"carrier = X"
by (auto intro!:carrierI elim!:carrierE)
(auto simp: discrete_top_def T_def is_open_def)

lemma (in discrete) open_iff [iff]:
"t open = (t ∈ Pow carrier)"
proof-
have "t open = (t ∈ Pow X)"
by (auto simp: T_def discrete_top_def is_open_def)
thus ?thesis by (simp add: carrier)
qed

lemma discrete_topology: "topology (discrete_top X)"
by (auto intro!: topologyI simp: is_open_def discrete_top_def)
blast

locale indiscrete = carrier T for X and T (structure) +
defines "T ≡ indiscrete_top X"

lemma (in indiscrete) carrier:
"X = carrier"
by (auto intro!: carrierI elim!: carrierE)
(auto simp: T_def indiscrete_top_def is_open_def)

lemma (in indiscrete) open_iff [iff]:
"t open = (t = {} ∨ t = carrier)"
proof-
have "t open = (t = {} ∨ t = X)"
by (auto simp: T_def indiscrete_top_def is_open_def)
thus ?thesis by (simp add: carrier)
qed

lemma indiscrete_topology: "topology (indiscrete_top X)"
by (rule topologyI) (auto simp: is_open_def indiscrete_top_def)

locale orderbase =
fixes X and B
defines "B ≡ order_base X"

locale ordertop1 =  orderbase X B + topobase B T for X and B and T (structure)

locale ordertop = carrier T for X and T (structure) +
defines "T ≡ order_top X"

lemma (in ordertop) ordertop_open:
"t open = (t ∈ order_top X)"
by (auto simp: T_def is_open_def)

lemma ordertop_topology [iff]:
"topology (order_top X)"
by (auto simp: order_top_def)

subsection‹Neighbourhoods›

definition
nhd :: "'a top ⇒ 'a ⇒ 'a set set"  ( "nhdsı") where
"nhd T x = {U. U ⊆ carr T ∧ (∃ m. is_open T m ∧ x∈m ∧ m ⊆ U)}"

lemma (in carrier) nhdI [intro]:
"⟦ U ⊆ carrier; m open; x ∈ m; m ⊆ U ⟧ ⟹  U ∈ nhds x"
by (auto simp: nhd_def)

lemma (in carrier) nhdE [elim]:
"⟦ U ∈ nhds x; ⋀m. ⟦ U ⊆ carrier; m open; x ∈ m; m ⊆ U ⟧ ⟹ R ⟧ ⟹ R"
by (auto simp: nhd_def)

lemma (in carrier) elem_in_nhd:
"U ∈ nhds x ⟹ x ∈ U"
by auto

lemma (in carrier) carrier_nhd [intro]: "x ∈ carrier ⟹ carrier ∈ nhds x"
by auto

lemma (in carrier) empty_not_nhd [iff]:
"{} ∉ nhds x "
by auto

lemma (in carrier) nhds_greater:
"⟦V ⊆ carrier; U ⊆ V;  U ∈ nhds x⟧ ⟹ V ∈ nhds x"
by (erule nhdE) blast

lemma (in topology) nhds_inter:
assumes nhdU: "U ∈ nhds x"
and     nhdV: "V ∈ nhds x"
shows "(U ∩ V) ∈ nhds x"
proof-
from nhdU obtain u where
Usub: "U ⊆ carrier" and
uT:   "u open" and
xu:   "x ∈ u" and
usub: "u ⊆ U"
by auto
from nhdV obtain v where
Vsub: "V ⊆ carrier" and
vT: "v open" and
xv: "x ∈ v" and
vsub: "v ⊆ V"
by auto
from Usub Vsub have "U ∩ V ⊆ carrier" by auto
moreover from uT vT have "u ∩ v open" ..
moreover from xu xv have "x ∈ u ∩ v" ..
moreover from usub vsub have "u ∩ v ⊆ U ∩ V" by auto
ultimately show  ?thesis by auto
qed

lemma (in carrier) sub_nhd:
"U ∈ nhds x ⟹ ∃V ∈ nhds x. V ⊆ U ∧ (∀ z ∈ V. U ∈ nhds z)"
by (auto elim!: nhdE)

lemma (in ordertop1) l1:
assumes mopen: "m open"
and xpoint: "x ∈ X"
and ypoint: "y ∈ X"
and xley: "x ≤ y"
and xinm: "x ∈ m"
shows "y ∈ m"
using mopen xinm
proof induct
case (basic U) thus ?case
by (auto simp: B_def order_base_def ypoint
intro: xley dest: order_trans)
qed auto

lemma (in ordertop1)
assumes xpoint: "x ∈ X" and ypoint: "y ∈ X" and xley: "x ≤ y"
shows "nhds x ⊆ nhds y"
proof
fix u assume "u ∈ nhds x"
then obtain m where "m open"
and "m ⊆ u" and "u ⊆ carrier" and "x ∈ m"
by auto
with xpoint ypoint xley
show "u ∈ nhds y"
by (auto dest: l1)
qed

subsection‹Closed sets›

text‹A set is closed if its complement is open.›

definition
is_closed :: "'a top ⇒ 'a set ⇒ bool" ("_ closedı" [50] 50) where
"is_closed T s ⟷ is_open T (carr T - s)"

lemma (in carrier) closedI:
"(carrier - s) open ⟹ s closed"
by (auto simp: is_closed_def)

lemma (in carrier) closedE:
"⟦ s closed; (carrier - s) open ⟹ R ⟧ ⟹ R"
by (auto simp: is_closed_def)

lemma (in topology) empty_closed [iff]:
"{} closed"
by (auto intro!: closedI)

lemma (in topology) carrier_closed [iff]:
"carrier closed"
by (auto intro!: closedI)

lemma (in carrier) compl_open_closed:
assumes mopen: "m open"
shows "(carrier - m) closed"
proof (rule closedI)
from mopen have "m ⊆ carrier"
by auto
hence "carrier - (carrier - m) = m"
thus "carrier - (carrier - m) open"
using mopen by simp
qed

lemma (in carrier) compl_open_closed1:
"⟦ m ⊆ carrier; (carrier - m) closed ⟧ ⟹ m open"
by (auto elim: closedE simp: diffsimps)

lemma (in carrier) compl_closed_iff [iff]:
" m ⊆ carrier ⟹ (carrier - m) closed = (m open)"
by (auto dest: compl_open_closed1 intro: compl_open_closed)

lemma (in topology) Un_closed [intro!]:
"⟦ x closed; y closed ⟧ ⟹ x ∪ y closed"
by (auto simp:Diff_Un elim!: closedE intro!: closedI)

lemma (in topology) inter_closed:
assumes xsclosed: "⋀x. x∈S ⟹ x closed"
shows "⋂S closed"
proof (rule closedI)
let ?M = "{m. ∃x∈S. m = carrier - x}"
have "∀ m ∈ ?M. m open"
by (auto dest: xsclosed elim: closedE)
hence "⋃ ?M open" ..
moreover have "⋃ ?M = carrier - ⋂S" by auto
ultimately show "carrier - ⋂S open" by auto
qed

corollary (in topology) Int_closed [intro!]:
assumes abclosed: "A closed" "B closed"
shows  "A ∩ B closed"
proof-
from assms have "⋂{A, B} closed"
by (blast intro!: inter_closed)
thus ?thesis by simp
qed

lemma (in topology) closed_diff_open:
assumes aclosed: "A closed"
and   bopen: "B open"
shows "A - B closed"
proof (rule closedI)
from aclosed have "carrier - A open"
by (rule closedE)
moreover from bopen have "carrier ∩ B open" by auto
ultimately have "(carrier - A) ∪ (carrier ∩ B) open" ..
thus "carrier - (A - B) open" by (simp add: diff_diff)
qed

lemma (in topology) open_diff_closed:
assumes aclosed: "A closed"
and   bopen: "B open"
shows "B - A open"
proof-
from aclosed have "carrier - A open"
by (rule closedE)
hence "(carrier - A) ∩ B open" using bopen ..
moreover from bopen have "B ⊆ carrier"
by auto
hence "(carrier - A) ∩ B = B - A" by auto
ultimately show "B - A open" by simp
qed

subsection‹Core, closure, and frontier of a set›

definition
cor :: "'a top ⇒ 'a set ⇒ 'a set"          ("coreı") where
"cor T s = (⋃{m. is_open T m ∧ m ⊆ s})"

definition
clsr :: "'a top ⇒ 'a set ⇒ 'a set"          ("closureı") where
"clsr T a = (⋂{c. is_closed T c ∧ a ⊆ c})"

definition
frt :: "'a top ⇒ 'a set ⇒ 'a set"          ("frontierı") where
"frt T s = clsr T s - cor T s"

subsubsection‹Core›

lemma (in carrier) coreI:
"⟦m open; m ⊆ s; x ∈ m ⟧ ⟹ x ∈ core s"
by (auto simp: cor_def)

lemma (in carrier) coreE:
"⟦ x ∈ core s; ⋀m. ⟦m open; m ⊆ s; x ∈ m ⟧ ⟹ R ⟧ ⟹ R"
by (auto simp: cor_def)

lemma (in topology) core_open [iff]:
"core a open"
by (auto simp: cor_def)

lemma (in carrier) core_subset:
"core a ⊆ a"
by (auto simp: cor_def)

lemmas (in carrier) core_subsetD = subsetD [OF core_subset]

lemma (in carrier) core_greatest:
"⟦ m open; m ⊆ a ⟧ ⟹ m ⊆ core a"
by (auto simp: cor_def)

lemma (in carrier) core_idem [simp]:
"core (core a) = core a"
by  (auto simp: cor_def)

lemma (in carrier) open_core_eq [simp]:
"a open ⟹ core a = a"
by (auto simp: cor_def)

lemma (in topology) core_eq_open:
"core a = a ⟹ a open"
by (auto elim: subst)

lemma (in topology) core_iff:
"a open = (core a = a)"
by (auto intro: core_eq_open)

lemma (in carrier) core_mono:
"a ⊆ b ⟹ core a ⊆ core b"
by (auto simp: cor_def)

lemma (in topology) core_Int [simp]:
"core (a ∩ b) = core a ∩ core b"
by (auto simp: cor_def)

lemma (in carrier) core_nhds:
"⟦ U ⊆ carrier; x ∈ core U ⟧ ⟹ U ∈ nhds x"
by (auto elim!: coreE)

lemma (in carrier) nhds_core:
"U ∈ nhds x ⟹ x ∈ core U"
by (auto intro: coreI)

lemma (in carrier) core_nhds_iff:
"U ⊆ carrier ⟹ (x ∈ core U) = (U ∈ nhds x)"
by (auto intro: core_nhds nhds_core)

subsubsection‹Closure›

lemma (in carrier) closureI [intro]:
"(⋀c. ⟦c closed; a ⊆ c⟧ ⟹ x ∈ c) ⟹ x ∈ closure a"
by (auto simp: clsr_def)

lemma (in carrier) closureE [elim]:
"⟦ x ∈ closure a; ¬ c closed ⟹ R;  ¬ a ⊆ c ⟹ R;  x ∈ c ⟹ R ⟧ ⟹ R"
by (auto simp: clsr_def)

lemma (in carrier) closure_least:
"s closed ⟹ closure s ⊆ s"
by auto

lemma (in carrier) subset_closure:
"s ⊆ closure s"
by auto

lemma (in topology) closure_carrier [simp]:
"closure carrier = carrier"
by auto

lemma (in topology) closure_subset:
"A ⊆ carrier ⟹ closure A ⊆ carrier"
by auto

lemma (in topology) closure_closed [iff]:
"closure a closed"
by (auto simp: clsr_def intro: inter_closed)

lemma (in carrier) closure_idem [simp]:
"closure (closure s) = closure s"
by (auto simp: clsr_def)

lemma (in carrier) closed_closure_eq [simp]:
"a closed ⟹ closure a = a"
by (auto simp: clsr_def)

lemma (in topology) closure_eq_closed:
"closure a = a ⟹ a closed"
by (erule subst) simp

lemma (in topology) closure_iff:
"a closed = (closure a = a)"
by (auto intro: closure_eq_closed)

lemma (in carrier) closure_mono1:
"mono (closure)"
by (rule, auto simp: clsr_def)

lemma (in carrier) closure_mono:
"a ⊆ b ⟹ closure a ⊆ closure b"
by (auto simp: clsr_def)

lemma (in topology) closure_Un [simp]:
"closure (a ∪ b) = closure a ∪ closure b"
by (rule, blast) (auto simp: clsr_def)

subsubsection‹Frontier›

lemma (in carrier) frontierI:
"⟦x ∈ closure s; x ∈ core s ⟹ False⟧ ⟹ x ∈ frontier s"
by (auto simp: frt_def)

lemma (in carrier) frontierE:
"⟦ x ∈ frontier s; ⟦x ∈ closure s; x ∈ core s ⟹ False⟧ ⟹ R ⟧ ⟹ R"
by (auto simp: frt_def)

lemma (in topology) frontier_closed [iff]:
"frontier s closed"
by (unfold frt_def)
(intro closure_closed core_open closed_diff_open)

lemma (in carrier) frontier_Un_core:
"frontier s ∪ core s = closure s"
by (auto dest: subsetD [OF core_subset] simp: frt_def)

lemma (in carrier) frontier_Int_core:
"frontier s ∩ core s = {}"
by (auto simp: frt_def)

lemma (in topology) closure_frontier [simp]:
"closure (frontier a) = frontier a"
by simp

lemma (in topology) frontier_carrier [simp]:
"frontier carrier = {}"
by (auto simp: frt_def)

text‹Hence frontier is not monotone. Also @{prop "cor T (frt T A) =
{}"} is not a theorem as illustrated by the following counter
example. By the way: could the counter example be prooved using an
instantiation?›

lemma counter_example_core_frontier:
fixes X defines [simp]: "X ≡ (UNIV::nat set)"
fixes T (structure) defines "T ≡ indiscrete_top X"
shows "core (frontier {0}) = X"
proof -
interpret indiscrete X T by fact
have "core {0} = {}"
by (auto simp add: carrier [symmetric] cor_def)
moreover have "closure {0} = UNIV"
by (auto simp: clsr_def carrier [symmetric] is_closed_def)
ultimately have "frontier {0} = UNIV"
by (auto simp: frt_def)
thus ?thesis
by (auto simp add: cor_def carrier [symmetric])
qed

definition
adhs :: "'a top ⇒ 'a ⇒ 'a set ⇒ bool"     (infix "adhı" 50) where
"adhs T x A ⟷ (∀ U ∈ nhd T x. U ∩ A ≠ {})"

"⟦x adh A;  U ∉ nhds x ⟹ R; U ∩ A ≠ {}  ⟹ R⟧ ⟹ R"

"(⋀U. U ∈ nhds x ⟹ U ∩ A ≠ {}) ⟹ x adh A"

assumes asub: "A ⊆ carrier"
and closure: "x ∈ closure A"
proof
fix U assume unhd: "U ∈ nhds x"
show "U ∩ A ≠ {}"
proof
assume UA: "U ∩ A = {}"
from unhd obtain V where "V open" "x ∈ V" and VU: "V ⊆ U" ..
moreover from UA VU have "V ∩ A = {}" by auto
ultimately show "False" using asub closure
by (auto  dest!: compl_open_closed simp: clsr_def)
qed
qed

assumes xpoint: "x ∈ carrier"
shows "x ∈ closure A"
proof (rule ccontr)
assume notclosure: "x ∉ closure A"
then obtain C
where closed: "C closed"
and   asubc:  "A ⊆ C"
and   xnotinc: "x ∉ C"
by (auto simp: clsr_def)
from closed have "carrier - C open" by (rule closedE)
moreover from xpoint xnotinc have "x ∈ carrier - C" by simp
ultimately have "carrier - C ∈ nhds x" by auto
with adh have "(carrier - C) ∩ A ≠ {}"
with asubc show "False" by auto
qed

assumes Asub: "A ⊆ carrier"
shows "A closed = (∀ x ∈ carrier. x adh A ⟶ x ∈ A)"
proof
assume "A closed"
hence AA: "closure A = A"
by auto
thus "(∀ x ∈ carrier. x adh A ⟶ x ∈ A)"
next assume adhA: "∀ x ∈ carrier. x adh A ⟶ x ∈ A"
have "closure A ⊆ A"
proof
fix x assume xclosure: "x ∈ closure A"
hence "x ∈ carrier" using Asub by (auto dest: closure_subset)
with xclosure show "x ∈ A" using Asub adhA
qed
thus "A closed" by (auto intro: closure_eq_closed)
qed

"⟦ A ⊆ carrier; x ∈ carrier ⟧ ⟹ (x adh A) = (x ∈ closure A)"

lemma (in topology) closure_complement [simp]:
shows  "closure (carrier - A) = carrier - core A"
proof
have  "closure (carrier - A) ⊆ carrier"
by (auto intro: closure_subset)
moreover have "closure (carrier - A) ∩ core A = {}"
proof (rule seteqI, clarsimp)
fix x assume xclosure: "x ∈ closure (carrier - A)"
moreover assume xcore: "x ∈ core A"
hence "core A ∈ nhds x"
by auto
ultimately have "core A ∩ (carrier - A) ≠ {}"
thus "False" by (auto dest: core_subsetD)
qed auto
ultimately show "closure (carrier - A) ⊆ carrier - core A"
by auto
next
show "carrier - core A ⊆ closure (carrier - A)"
by (auto simp: cor_def clsr_def is_closed_def)
qed

lemma (in carrier) core_complement [simp]:
assumes asub: "A ⊆ carrier"
shows  "core (carrier - A) = carrier - closure A"
proof
show "carrier - closure A ⊆ core (carrier - A)"
by (auto simp: cor_def clsr_def is_closed_def)
next
have "core (carrier - A) ⊆ carrier"
by (auto elim!: coreE)
moreover have  "core (carrier - A) ∩ closure A = {}"
proof auto
fix x assume "x ∈ core (carrier - A)"
hence "(carrier - A) ∈ nhds x"
by (auto iff: core_nhds_iff)
moreover assume "x ∈ closure A"
ultimately have "A ∩ (carrier - A) ≠ {}" using asub
thus "False" by auto
qed
ultimately show "core (carrier - A) ⊆ carrier - closure A"
by auto
qed

lemma (in carrier) core_closure_diff_empty [simp]:
assumes asub: "A ⊆ carrier"
shows "core (closure A - A) = {}"
proof auto
fix x assume "x ∈ core (closure A - A)"
then obtain m where
mopen: "m open" and
xinm: "x ∈ m" and
msub: "m ⊆ closure A" and
minter: "m ∩ A = {}"
by (auto elim!: coreE)
from xinm msub have "x adh A" using asub
moreover from xinm mopen have "m ∈ nhds x"
by auto
ultimately have "m ∩ A ≠ {}" by (auto elim: adhCE)
with minter show "False" by auto
qed

subsection‹Dense sets›

definition
is_densein :: "'a top ⇒ 'a set ⇒ 'a set ⇒ bool" (infix "denseinı" 50) where
"is_densein T A B ⟷ B ⊆ clsr T A"

definition
is_dense :: "'a top ⇒ 'a set ⇒ bool"             ("_ denseı" [50] 50) where
"is_dense T A = is_densein T A (carr T)"

lemma (in carrier) densinI [intro!]: "B ⊆ closure A ⟹ A densein B"
by (auto simp: is_densein_def)

lemma (in carrier) denseinE [elim!]: "⟦ A densein B; B ⊆ closure A ⟹ R ⟧ ⟹ R"
by (auto simp: is_densein_def)

lemma (in carrier) denseI [intro!]: "carrier ⊆ closure A ⟹ A dense"
by (auto simp: is_dense_def)

lemma (in carrier) denseE [elim]: "⟦ A dense; carrier ⊆ closure A ⟹ R ⟧ ⟹ R"
by (auto simp: is_dense_def)

lemma (in topology) dense_closure_eq [dest]:
"⟦ A dense; A ⊆ carrier ⟧ ⟹ closure A = carrier"
by (auto dest: closure_subset)

lemma (in topology) dense_lemma:
"A ⊆ carrier ⟹ carrier - (closure A - A) dense"
by auto

lemma (in topology) ex_dense_closure_inter:
assumes ssub: "S ⊆ carrier"
shows "∃ D C. D dense ∧ C closed ∧ S = D ∩ C"
proof-
let ?D = "carrier - (closure S - S)" and
?C = "closure S"
from ssub have "?D dense" by auto
moreover have "?C closed" ..
moreover from ssub
have "(carrier - (closure S - S)) ∩ closure S = S"
ultimately show ?thesis
by auto
qed

lemma (in topology) ex_dense_closure_interE:
assumes ssub: "S ⊆ carrier"
and H: "⋀D C. ⟦ D ⊆ carrier; C ⊆ carrier; D dense; C closed; S = D ∩ C ⟧ ⟹ R"
shows "R"
proof-
let ?D = "(carrier - (closure S - S))"
and ?C = "closure S"
have "?D ⊆ carrier" by auto
moreover from assms have "?C ⊆ carrier"
by (auto dest!: closure_subset)
moreover from assms have "?D dense" by auto
moreover have "?C closed" ..
moreover from ssub have "S = ?D ∩ ?C"
ultimately show ?thesis
by (rule H)
qed

subsection‹Continuous functions›

definition
INJ :: "'a set ⇒ 'b set ⇒ ('a ⇒ 'b) set" where
"INJ A B = {f. f : A → B ∧ inj_on f A}"

definition
SUR :: "'a set ⇒ 'b set ⇒ ('a ⇒ 'b) set" where
"SUR A B = {f. f : A → B ∧ (∀ y∈B. ∃ x∈A. y = f x)}"

definition
BIJ :: "'a set ⇒ 'b set ⇒ ('a ⇒ 'b) set" where
"BIJ A B = INJ A B ∩ SUR A B"

definition
cnt :: "'a top ⇒ 'b top ⇒ ('a ⇒ 'b) set" where
"cnt S T = {f. f : carr S → carr T ∧
(∀ m. is_open T m ⟶ is_open S (carr S ∩ (f -` m)))}"

definition
HOM :: " 'a top ⇒ 'b top ⇒ ('a ⇒ 'b) set" where
"HOM S T = {f. f ∈ cnt S T ∧ inv f ∈ cnt T S ∧ f ∈ BIJ (carr S) (carr T)}"

definition
homeo :: "'a top ⇒ 'b top ⇒ bool" where
"homeo S T ⟷ (∃h ∈ BIJ (carr S) (carr T). h ∈ cnt S T ∧ inv h ∈ cnt T S)"

definition
fimg :: "'b top ⇒ ('a ⇒ 'b) ⇒ 'a set set ⇒ 'b set set" where
"fimg T f F = {v. v ⊆ carr T ∧ (∃ u ∈ F. f`u ⊆ v)}"

lemma domain_subset_vimage:
"f : A → B ⟹ A ⊆ f-`B"
by (auto intro: funcset_mem)

lemma domain_inter_vimage:
"f : A → B ⟹ A ∩ f-`B = A"
by (auto intro: funcset_mem)

lemma funcset_vimage_diff:
"f : A → B ⟹ A - f-`(B - C) = A ∩ f-`C"
by (auto intro: funcset_mem)

locale func = S?: carrier S + T?: carrier T
for f and S (structure) and T (structure) and fimage +
assumes func [iff]: "f : carrier⇘S⇙ → carrier⇘T⇙"
defines "fimage ≡ fimg T f"
notes func_mem [simp, intro] = funcset_mem [OF func]
and   domain_subset_vimage [iff] = domain_subset_vimage [OF func]
and   domain_inter_vimage  [simp] = domain_inter_vimage [OF func]
and   vimage_diff          [simp] = funcset_vimage_diff [OF func]

lemma (in func) fimageI [intro!]:
shows "⟦ v ⊆ carrier⇘T⇙; u ∈ F; f`u ⊆ v⟧ ⟹ v ∈ fimage F"
by (auto simp: fimg_def fimage_def)

lemma (in func) fimageE [elim!]:
"⟦ v ∈ fimage F; ⋀u. ⟦ v ⊆ carrier⇘T⇙ ; u∈F; f`u ⊆ v⟧ ⟹ R ⟧ ⟹ R"
by (auto simp: fimage_def fimg_def)

lemma cntI:
"⟦ f : carr S → carr T;
(⋀m. is_open T m ⟹ is_open S (carr S ∩ (f -` m))) ⟧
⟹ f ∈ cnt S T"
by (auto simp: cnt_def)

lemma cntE:
"⟦ f ∈ cnt S T;
⟦ f : carr S → carr T;
∀m. is_open T m ⟶ is_open S (carr S ∩ (f -` m)) ⟧ ⟹ P
⟧ ⟹ P"
by (auto simp: cnt_def)

lemma cntCE:
"⟦ f ∈ cnt S T;
⟦ ¬ is_open T m; f : carr S → carr T ⟧ ⟹ P;
⟦ is_open S (carr S ∩ (f -` m)); f : carr S → carr T ⟧  ⟹ P
⟧ ⟹ P"
by (auto simp: cnt_def)

lemma cnt_fun:
"f ∈ cnt S T ⟹ f : carr S → carr T"

lemma cntD1:
"⟦ f ∈ cnt S T; x ∈ carr S ⟧ ⟹ f x ∈ carr T"
by (auto simp add: cnt_def intro: funcset_mem)

lemma cntD2:
"⟦ f ∈ cnt S T; is_open T m ⟧ ⟹ is_open S (carr S ∩ (f -` m))"
by (auto simp: cnt_def)

locale continuous = func +
assumes continuous [dest, simp]:
"m open⇘T⇙ ⟹ carrier ∩ (f -` m) open"

lemma continuousI:
fixes S (structure)
fixes T (structure)
assumes  "f : carrier⇘S⇙ → carrier⇘T⇙"
"⋀m. m open⇘T⇙ ⟹ carrier ∩ (f -` m) open"
shows "continuous f S T"
using assms by (auto simp: continuous_def func_def continuous_axioms_def)

lemma continuousE:
fixes S (structure)
fixes T (structure)
shows
"⟦ continuous f S T;
⟦ f : carrier⇘S⇙ → carrier⇘T⇙;
∀m. m open⇘T⇙ ⟶ carrier⇘S⇙ ∩ (f -` m) open ⟧ ⟹ P
⟧ ⟹ P"
by (auto simp: continuous_def func_def continuous_axioms_def)

lemma continuousCE:
fixes S (structure)
fixes T (structure)
shows
"⟦ continuous f S T;
⟦ ¬ m open⇘T⇙; f : carrier⇘S⇙ → carrier⇘T⇙ ⟧ ⟹ P;
⟦ carrier⇘S⇙ ∩ (f -` m) open⇘S⇙; f : carrier⇘S⇙ → carrier⇘T⇙ ⟧  ⟹ P
⟧ ⟹ P"
by (auto simp: continuous_def func_def continuous_axioms_def)

lemma (in continuous) closed_vimage [intro, simp]:
assumes csubset: "c ⊆ carrier⇘T⇙"
and cclosed: "c closed⇘T⇙"
shows "f -` c closed"
proof-
from cclosed have  "carrier⇘T⇙ - c open⇘T⇙"  by (rule closedE)
hence "carrier ∩ f -` (carrier⇘T⇙ - c) open" by auto
hence "carrier - f -` c open" by (auto simp: diffsimps)
thus "f -` c closed" by (rule S.closedI)
qed

lemma continuousI2:
fixes S (structure)
fixes T (structure)
assumes func: "f : carrier⇘S⇙ → carrier⇘T⇙"
assumes R: "⋀c. ⟦ c ⊆ carrier⇘T⇙; c closed⇘T⇙ ⟧ ⟹ f -` c closed"
shows "continuous f S T"
proof (rule continuous.intro)
from func show "func f S T" by (auto simp: func_def)
next
interpret S: carrier S .
interpret T: carrier T .
show "continuous_axioms f S T"
proof (rule continuous_axioms.intro)
fix m let ?c = "carrier⇘T⇙ - m" assume "m open⇘T⇙"
hence csubset: "?c ⊆ carrier⇘T⇙" and cclosed: "?c closed⇘T⇙"
by auto
hence "f -` ?c closed" by (rule R)
hence  "carrier - f -` ?c open"
by (rule S.closedE)
thus "carrier ∩ f -` m open" by (simp add: funcset_vimage_diff [OF func])
qed
qed

lemma cnt_compose:
"⟦ f ∈ cnt S T; g ∈ cnt T U ⟧ ⟹ (g ∘ f) ∈ cnt S U "
by (auto intro!: cntI funcset_comp elim!: cntE simp add: vimage_comp)

lemma continuous_compose:
"⟦ continuous f S T; continuous g T U ⟧ ⟹ continuous (g ∘ f) S U"
by (auto intro!: continuousI funcset_comp

lemma id_continuous:
fixes T (structure)
shows "continuous id T T"
proof(rule continuousI)
show "id ∈ carrier → carrier"
by (auto intro: funcsetI)
next
interpret T: carrier T .
fix m assume mopen: "m open"
hence "m ⊆ carrier" by auto
hence "carrier ∩ m = m" by auto
thus "carr T ∩ id -` m open" using mopen
by auto
qed

lemma (in discrete) continuous:
fixes f and S (structure) and fimage
assumes "func f T S" defines "fimage ≡ fimg S f"
shows "continuous f T S"
proof -
interpret func f T S fimage by fact fact
show ?thesis by (auto intro!: continuousI)
qed

lemma (in indiscrete) continuous:
fixes S (structure)
assumes "topology S"
fixes f and fimage
assumes "func f S T" defines "fimage ≡ fimg T f"
shows "continuous f S T"
proof -
interpret S: topology S by fact
interpret func f S T fimage by fact fact
show ?thesis by (auto del: S.Int_open intro!: continuousI)
qed

subsection‹Filters›

definition
fbas :: "'a top ⇒ 'a set set ⇒ bool" ("fbaseı") where
"fbas T B ⟷ {} ∉ B ∧ B ≠ {} ∧
(∀ a∈B. ∀ b∈B. ∃ c∈B. c ⊆ a ∩ b)"

definition
filters :: "'a top ⇒ 'a set set set"      ("Filtersı") where
"filters T = { F. {} ∉ F ∧ ⋃F ⊆ carr T ∧
(∀ A B. A∈F ∧ B∈F ⟶ A∩B ∈ F) ∧
(∀ A B. A∈F ∧ A⊆B ∧ B ⊆ carr T ⟶ B ∈ F) }"

definition
ultr :: "'a top ⇒ 'a set set ⇒ bool"      ("ultraı") where
"ultr T F ⟷ (∀ A. A ⊆ carr T ⟶ A ∈ F ∨ (carr T - A) ∈ F)"

lemma filtersI [intro]:
fixes T (structure)
assumes a1: "{} ∉ F"
and a2: "⋃F ⊆ carrier"
and a3: "⋀ A B. ⟦ A ∈ F; B ∈ F ⟧ ⟹ A ∩ B ∈ F"
and a4: "⋀ A B. ⟦ A ∈ F; A ⊆ B; B ⊆ carrier ⟧ ⟹ B ∈ F"
shows "F ∈ Filters"
using a1 a2
by (auto simp add: filters_def intro: a3 a4)

lemma filtersE:
assumes a1: "F ∈ filters T"
and R: "⟦ {} ∉ F;
⋃F ⊆ carr T;
∀ A B. A∈F ∧  B∈F ⟶ A∩B ∈ F;
∀ A B. A∈F ∧ A⊆B ∧ B⊆ carr T ⟶ B ∈ F
⟧ ⟹ R"
shows "R"
using a1
apply (rule R)
apply ((erule conjE)+, assumption)+
done

lemma filtersD1:
"F ∈ filters T ⟹ {} ∉ F"
by (erule filtersE)

lemma filtersD2:
"F ∈ filters T ⟹ ⋃F ⊆ carr T"
by (erule filtersE)

lemma filtersD3:
"⟦ F ∈ filters T; A∈F;  B∈F ⟧ ⟹ A ∩ B ∈ F"
by (blast elim: filtersE)

lemma filtersD4:
"⟦ F ∈ filters T; A ⊆ B; B ⊆ carr T; A∈F ⟧ ⟹ B ∈ F"
by (blast elim: filtersE)

locale filter = carrier T for F and T (structure) +
assumes F_filter: "F ∈ Filters"
notes not_empty [iff]       = filtersD1 [OF F_filter]
and   union_carr [iff]      = filtersD2 [OF F_filter]
and   filter_inter [intro!, simp] = filtersD3 [OF F_filter]
and   filter_greater [dest] = filtersD4 [OF F_filter]

lemma (in filter) elem_carrier [elim]:
assumes A: "A ∈ F"
assumes R: "⟦ A ⊆ carrier; A ≠ {} ⟧ ⟹ R"
shows "R"
proof-
have "⋃F ⊆ carrier" ..
thus ?thesis using A by (blast intro: R)
qed

lemma empty_filter [iff]: "{} ∈ filters T"
by auto

lemma (in filter) contains_carrier [intro, simp]:
assumes F_not_empty: "F≠{}"
shows "carrier ∈ F"
proof-
from F_not_empty obtain A where  "A ⊆ carrier" "A ∈ F"
by auto
thus ?thesis by auto
qed

lemma nonempty_filter_implies_nonempty_carrier:
fixes T (structure)
assumes F_filter: "F ∈ Filters"
and F_not_empty: "F ≠ {}"
shows "carrier ≠ {}"
proof-
from assms have "carrier ∈ F"
by (auto dest!: filter.contains_carrier [OF filter.intro])
thus ?thesis using F_filter
by(auto dest: filtersD1)
qed

lemma carrier_singleton_filter:
fixes T (structure)
shows "carrier ≠ {} ⟹ {carrier} ∈ Filters"
by auto

lemma (in topology) nhds_filter:
"nhds x ∈ Filters"
by (auto dest: nhds_greater intro!: filtersI nhds_inter)

lemma fimage_filter:
fixes f and S (structure) and T (structure) and fimage
assumes "func f S T" defines "fimage ≡ fimg T f"
fixes F assumes "filter F S"
shows "fimage F ∈ Filters⇘T⇙"
proof -
interpret func f S T fimage by fact fact
interpret filter F S by fact
show ?thesis proof
fix A B assume "A ∈ fimage F" "B ∈ fimage F"
then obtain a b where
AY: "A⊆carrier⇘T⇙" and aF: "a∈F" and fa: "f ` a ⊆ A" and
BY: "B⊆carrier⇘T⇙" and bF: "b∈F" and fb: "f ` b ⊆ B"
by (auto)
from AY BY have "A∩B ⊆ carrier⇘T⇙" by auto
moreover from aF bF have "a ∩ b ∈ F" by auto
moreover from aF bF fa fb have "f`(a ∩ b) ⊆ A ∩ B" by auto
ultimately show "A∩B ∈ fimage F" by auto
qed auto
qed

lemma Int_filters:
fixes F and T (structure) assumes "filter F T"
fixes E assumes "filter E T"
shows "F ∩ E ∈ Filters"
proof -
interpret filter F T by fact
interpret filter E T by fact
show ?thesis by auto
qed

lemma ultraCI [intro!]:
fixes T (structure)
shows "(⋀A. ⟦ A ⊆ carrier; carrier - A ∉ F ⟧ ⟹ A ∈ F) ⟹ ultra F"
by (auto simp: ultr_def)

lemma ultraE:
fixes T (structure)
shows "⟦ ultra F; A ⊆ carrier;
A ∈ F ⟹ R;
carrier - A ∈ F ⟹ R
⟧ ⟹ R"
by (auto simp: ultr_def)

fixes T (structure)
shows "⟦ ultra F; A ⊆ carrier; A ∉ F ⟧ ⟹ (carrier - A) ∈ F"
by (erule ultraE) auto

locale ultra_filter = filter +
assumes ultra: "ultra F"
notes ultraE [elim] = ultraE [OF ultra]

lemma (in ultra_filter) max:
fixes E assumes "filter E T"
assumes fsube: "F ⊆ E"
shows "E ⊆ F"
proof -
interpret filter E T by fact
show ?thesis proof
fix x assume xinE: "x ∈ E"
hence "x ⊆ carrier" ..
hence "x ∈ F ∨ carrier - x ∈ F" by auto
thus "x ∈ F"
proof clarify
assume "carrier - x ∈ F"
hence "carrier - x ∈ E" using fsube ..
with xinE have "x ∩ (carrier - x) ∈ E" ..
hence False by auto
thus "x ∈ F" ..
qed
qed
qed

lemma (in filter) max_ultra:
assumes carrier_not_empty: "carrier ≠ {}"
and fmax: "∀ E ∈ Filters. F ⊆ E ⟶ F = E"
shows "ultra F"
proof

fix A let ?CA = "carrier - A"
assume A_subset_carrier: "A ⊆ carrier"
and CA_notin_F: "?CA ∉ F"

let ?E  = "{V. ∃ U∈F. V ⊆ carrier ∧ A ∩ U ⊆ V}"
have "?E ∈ Filters"
proof
show "{} ∉ ?E"
proof clarify
fix U assume U_in_F: "U ∈ F" and "A ∩ U ⊆ {}"
hence "U ⊆ ?CA" by auto
with U_in_F have "?CA ∈ F" by auto
with CA_notin_F show False ..
qed
next show "⋃?E ⊆ carrier" by auto
next fix a b assume "a ∈ ?E" and "b ∈ ?E"
then obtain u v where props: "u ∈ F" "a ⊆ carrier" "A ∩ u ⊆ a"
"v ∈ F" "b ⊆ carrier" "A ∩ v ⊆ b" by auto
hence "(u ∩ v) ∈ F" "a ∩ b ⊆ carrier" "A ∩ (u ∩ v) ⊆ a ∩ b"
by auto
thus "a ∩ b ∈ ?E" by auto
next fix a b assume "a ∈ ?E" and asub: "a ⊆ b" and bsub: "b ⊆ carrier"
thus "b ∈ ?E" by blast
qed

moreover have "F ⊆ ?E" by auto

moreover from carrier_not_empty
have "{carrier} ∈ Filters" by auto
hence "F ≠ {}" using fmax by blast
hence "A ∈ ?E" using A_subset_carrier by auto

ultimately show "A ∈ F" using fmax by auto

qed

lemma filter_chain_lemma:
fixes T (structure) and F
assumes "filter F T"
assumes C_chain: "C ∈ chains {V. V ∈ Filters ∧ F ⊆ V}" (is "C ∈ chains ?FF")
shows "⋃(C ∪ {F}) ∈ Filters" (is "?E ∈ Filters")
proof-
interpret filter F T by fact
from C_chain have C_subset_FF[dest]: "⋀ x. x∈C ⟹ x ∈ ?FF" and
C_ordered: "∀ A ∈ C. ∀ B ∈ C. A ⊆ B ∨ B ⊆ A"
by (auto simp: chains_def chain_subset_def)

show ?thesis
proof
show "{} ∉ ?E" by (auto dest: filtersD1)
next
show "⋃?E ⊆ carrier" by (blast dest: filtersD2)
next
fix a b assume a_in_E: "a ∈ ?E" and a_subset_b: "a ⊆ b"
and b_subset_carrier: "b ⊆ carrier"
thus "b ∈ ?E" by (blast dest: filtersD4)
next
fix a b assume a_in_E: "a ∈ ?E" and b_in_E: "b ∈ ?E"
then obtain A B where A_in_chain: "A ∈ C ∪ {F}" and B_in_chain: "B ∈ C ∪ {F}"
and a_in_A: "a ∈ A" and b_in_B: "b ∈ B" and A_filter: "A ∈ Filters"
and B_filter: "B ∈ Filters"
by auto
with C_ordered have "A ⊆ B ∨ B ⊆ A" by auto
thus "a∩b ∈ ?E"
proof
assume "A ⊆ B"
with a_in_A have "a ∈ B" ..
with B_filter b_in_B have "a∩b ∈ B" by (intro filtersD3)
with B_in_chain show ?thesis ..
next
assume "B ⊆ A" ― ‹Symmetric case›
with  b_in_B A_filter a_in_A A_in_chain
show ?thesis by (blast intro: filtersD3)
qed
qed
qed

lemma expand_filter_ultra:
fixes T (structure)
assumes carrier_not_empty: "carrier ≠ {}"
and     F_filter: "F ∈ Filters"
and     R: "⋀U.  ⟦ U ∈ Filters;  F ⊆ U; ultra U ⟧ ⟹ R"
shows "R"
proof-
let ?FF = "{V. V ∈ Filters ∧ F ⊆ V}"
have "∀ C ∈ chains ?FF. ∃y ∈ ?FF. ∀x ∈ C. x ⊆ y"
proof clarify
fix C let ?M = "⋃(C ∪ {F})"
assume C_in_chain: "C ∈ chains ?FF"
hence "?M ∈ ?FF" using F_filter
by (auto dest: filter_chain_lemma [OF filter.intro])
moreover have "∀ x ∈ C. x ⊆ ?M" using C_in_chain
by (auto simp: chain_def)
ultimately show "∃y∈?FF. ∀x∈C. x ⊆ y"
by auto
qed then obtain U where
U_FFilter: "U ∈ ?FF" and U_max: "∀ V ∈ ?FF. U ⊆ V ⟶ V = U"
by (blast dest!: Zorn_Lemma2)
hence U_filter: "U ∈ Filters" and F_subset_U: "F ⊆ U"
by auto
moreover from U_filter carrier_not_empty have "ultra U"
proof (rule filter.max_ultra [OF filter.intro], clarify)
fix E x assume "E ∈ Filters" and  U_subset_E: "U ⊆ E" and x_in_E: "x ∈ E"
with F_subset_U have "E ∈ ?FF" by auto
with U_subset_E x_in_E U_max show "x ∈ U" by blast
qed
ultimately show ?thesis
by (rule R)
qed

subsection ‹Convergence›

definition
converges :: "'a top ⇒ 'a set set ⇒ 'a ⇒ bool" ("(_ ⤏ı _)" [55, 55] 55) where
"converges T F x ⟷ nhd T x ⊆ F"

notation
converges  ("(_ ⊢ _ ⟶ _)" [55, 55, 55] 55)

definition
cnvgnt :: "'a top ⇒ 'a set set ⇒ bool" ("_ convergentı" [50] 50) where
"cnvgnt T F ⟷ (∃ x ∈ carr T. converges T F x)"

definition
limites :: "'a top ⇒ 'a set set ⇒ 'a set" ("limsı") where
"limites T F = {x. x ∈ carr T ∧ T ⊢ F ⟶ x}"

definition
limes :: "'a top ⇒ 'a set set ⇒ 'a" ("limı") where
"limes T F = (THE x. x ∈ carr T ∧ T ⊢ F ⟶ x)"

lemma (in carrier) convergesI [intro]:
"nhds x ⊆ F ⟹ F ⤏ x"
by (auto simp: converges_def)

lemma (in carrier) convergesE [elim]:
"⟦ F ⤏ x; nhds x ⊆ F ⟹ R ⟧ ⟹ R"
by (auto simp: converges_def)

lemma (in carrier) convergentI [intro?]:
"⟦ F ⤏ x; x ∈ carrier ⟧ ⟹ F convergent"
by (auto simp: cnvgnt_def)

lemma (in carrier) convergentE [elim]:
"⟦ F convergent;
⋀ x. ⟦ F ⤏ x; x ∈ carrier ⟧ ⟹ R
⟧ ⟹ R"
by (auto simp: cnvgnt_def)

lemma (in continuous) fimage_converges:
assumes   xpoint: "x ∈ carrier"
and       conv:   "F ⤏⇘S⇙ x"
shows    "fimage F ⤏⇘T⇙ (f x)"
proof (rule, rule)
fix v assume vnhd: "v ∈ nhds⇘T⇙ (f x)"
then obtain m where v_subset_carrier: "v ⊆ carrier⇘T⇙"
and m_open: "m open⇘T⇙"
and m_subset_v: "m ⊆ v"
and fx_in_m: "f x ∈ m" ..
let ?m' = "carrier ∩ f-`m"
from fx_in_m xpoint have "x ∈ ?m'" by auto
with m_open have "?m' ∈ nhds x" by auto
with conv have "?m' ∈ F" by auto
moreover from m_subset_v have "f`?m' ⊆ v" by auto
ultimately show "v ∈ fimage F" using v_subset_carrier by auto
qed

corollary (in continuous) fimage_convergent [intro!]:
"F convergent⇘S⇙ ⟹ fimage F convergent⇘T⇙"
by (blast intro: convergentI fimage_converges)

lemma (in topology) closure_convergent_filter:
assumes xclosure: "x ∈ closure A"
and xpoint: "x ∈ carrier"
and asub: "A ⊆ carrier"
and H: "⋀F. ⟦ F ∈ Filters; F ⤏ x; A ∈ F⟧ ⟹ R"
shows "R"
proof-
let ?F = "{v. v ⊆ carrier ∧ (∃ u ∈ nhds x. u ∩ A ⊆ v)}"
have "?F ∈ Filters"
proof
thus "{} ∉ ?F" by (auto elim: adhCE)
next show "⋃?F ⊆ carrier" by auto
next fix a b assume aF: "a ∈ ?F" and bF: "b ∈ ?F"
then obtain u v where
aT: "a ⊆ carrier" and bT: "b ⊆ carrier" and
ux: "u ∈ nhds x" and vx: "v ∈ nhds x" and
uA: "u ∩ A ⊆ a" and vA: "v ∩ A ⊆ b"
by auto
moreover from ux vx have "u ∩ v ∈ nhds x"
by (auto intro: nhds_inter)
moreover from uA vA have "(u ∩ v) ∩ A ⊆ a ∩ b" by auto
ultimately show  "a ∩ b ∈ ?F" by auto
next fix a b assume aF: "a ∈ ?F" and ab: "a ⊆ b" and bT: "b ⊆ carrier"
then obtain u
where at: "a ⊆ carrier" and ux: "u ∈ nhds x" and  uA: "u ∩ A ⊆ a"
by auto
moreover from ux bT have "u ∪ b ∈ nhds x"
by (auto intro: nhds_greater)
moreover from uA ab have "(u ∪ b) ∩ A ⊆ b" by auto
ultimately show "b ∈ ?F" by auto
qed
moreover have "?F ⤏ x"
by auto
moreover from asub xpoint have "A ∈ ?F"
by blast
ultimately show ?thesis
by (rule H)
qed

lemma convergent_filter_closure:
fixes F and T (structure)
assumes "filter F T"
assumes converge: "F ⤏ x"
and   xpoint: "x ∈ carrier"
and   AF: "A ∈ F"
shows "x ∈ closure A"
proof-
interpret filter F T by fact
proof
fix u assume unhd: "u ∈ nhds x"
with converge have "u ∈ F" by auto
with AF have "u ∩ A ∈ F" by auto
thus "u ∩ A ≠ {}"  by blast
qed
with xpoint show ?thesis
qed

subsection‹Separation›

subsubsection‹T0 spaces›

locale T0 = topology +
assumes T0: "∀ x ∈ carrier. ∀ y ∈ carrier. x ≠ y ⟶
(∃ u ∈ nhds x. y ∉ u) ∨ (∃ v ∈ nhds y. x ∉ v)"

lemma (in T0) T0_eqI:
assumes points: "x ∈ carrier" "y ∈ carrier"
and R1: "⋀u. u ∈ nhds x ⟹ y ∈ u"
and R2: "⋀v. v ∈ nhds y ⟹ x ∈ v"
shows "x = y"
using T0 points
by (auto intro: R1 R2)

lemma (in T0) T0_neqE [elim]:
assumes x_neq_y: "x ≠ y"
and points: "x ∈ carrier" "y ∈ carrier"
and R1: "⋀u. ⟦ u ∈ nhds x; y ∉ u ⟧ ⟹ R"
and R2: "⋀v. ⟦ v ∈ nhds y; x ∉ v ⟧ ⟹ R"
shows "R"
using T0 points x_neq_y
by (auto intro: R1 R2)

subsubsection‹T1 spaces›

locale T1 = T0 +
assumes DT01: "∀ x ∈ carrier. ∀ y ∈ carrier. x ≠ y ⟶
(∃ u ∈ nhds x. y ∉ u) = (∃ v ∈ nhds y. x ∉ v)"

lemma (in T1) T1_neqE [elim]:
assumes x_neq_y: "x ≠ y"
and points: "x ∈ carrier" "y ∈ carrier"
and R [intro] : "⋀u v. ⟦ u ∈ nhds x; v ∈ nhds y; y ∉ u; x ∉ v⟧ ⟹ R"
shows "R"
proof-
from DT01 x_neq_y points
have nhd_iff: "(∃ v ∈ nhds y. x ∉ v) = (∃ u ∈ nhds x. y ∉ u)"
by force
from x_neq_y points show ?thesis
proof
fix u assume u_nhd: "u ∈ nhds x" and y_notin_u: "y ∉ u"
with nhd_iff obtain v where  "v ∈ nhds y" and "x ∉ v" by blast
with u_nhd y_notin_u show "R" by auto
next
fix v assume v_nhd: "v ∈ nhds y" and x_notin_v: "x ∉ v"
with nhd_iff obtain u where  "u ∈ nhds x" and "y ∉ u" by blast
with v_nhd x_notin_v show "R" by auto
qed
qed

declare (in T1) T0_neqE [rule del]

lemma (in T1) T1_eqI:
assumes points: "x ∈ carrier" "y ∈ carrier"
and R1: "⋀u v. ⟦ u ∈ nhds x; v ∈ nhds y; y ∉ u ⟧ ⟹  x ∈ v"
shows "x = y"
proof (rule ccontr)
assume "x ≠ y" thus False using points
by (auto intro: R1)
qed

lemma (in T1) singleton_closed [iff]: "{x} closed"
proof (cases "x ∈ carrier")
case False hence "carrier - {x} = carrier"
by auto
thus ?thesis by (clarsimp intro!: closedI)
next
case True show ?thesis
proof (rule closedI, rule open_kriterion)
fix y assume "y ∈ carrier - {x}"
hence "y ∈ carrier" "x ≠ y" by auto
with True obtain v where "v ∈ nhds y" "x ∉ v"
by (elim T1_neqE)
then obtain m where "m open" "y∈m" "m ⊆ carrier - {x}"
by (auto elim!: nhdE)
thus "∃m. m open ∧ y ∈ m ∧ m ⊆ carrier - {x}"
by blast
qed
qed

lemma (in T1) finite_closed:
assumes finite: "finite A"
shows "A closed"
using finite
proof induct
case empty show ?case ..
next
case (insert x F)
hence "{x} ∪ F closed" by blast
thus ?case by simp
qed

subsubsection‹T2 spaces (Hausdorff spaces)›

locale T2 = T1 +
assumes T2: "∀ x ∈ carrier. ∀ y ∈ carrier. x ≠ y
⟶ (∃ u ∈ nhds x. ∃ v ∈ nhds y. u ∩ v = {})"

lemma T2_axiomsI:
fixes T (structure)
shows
"(⋀x y. ⟦ x ∈ carrier; y ∈ carrier; x ≠ y ⟧ ⟹
∃ u ∈ nhds x. ∃ v ∈ nhds y. u ∩ v = {})
⟹ T2_axioms T"
by (auto simp: T2_axioms_def)

declare (in T2) T1_neqE [rule del]

lemma (in T2) neqE [elim]:
assumes neq: "x ≠ y"
and points: "x ∈ carrier" "y ∈ carrier"
and R: "⋀ u v. ⟦ u ∈ nhds x; v ∈ nhds y; u ∩ v = {} ⟧ ⟹ R"
shows R
proof-
from T2 points neq obtain u v where
"u ∈ nhds x" "v ∈ nhds y" "u ∩ v = {}" by force
thus R by (rule R)
qed

lemma (in T2) neqE2 [elim]:
assumes neq: "x ≠ y"
and points: "x ∈ carrier" "y ∈ carrier"
and R: "⋀ u v. ⟦ u ∈ nhds x; v ∈ nhds y; z ∉ u ∨ z ∉ v⟧ ⟹ R"
shows R
proof-
from T2 points neq obtain u v where
"u ∈ nhds x" "v ∈ nhds y" "u ∩ v = {}" by force
thus R by (auto intro: R)
qed

lemma T2_axiom_implies_T1_axiom:
fixes T (structure)
assumes T2: "∀ x ∈ carrier. ∀ y ∈ carrier. x ≠ y
⟶ (∃ u ∈ nhds x. ∃ v ∈ nhds y. u ∩ v = {})"
shows "T1_axioms T"
proof (rule T1_axioms.intro, clarify)
interpret carrier T .
fix x y assume neq: "x ≠ y" and
points: "x ```