# Theory Topological_Space

```text ‹Authors: Anthony Bordg and Lawrence Paulson,
with some contributions from Wenda Li›

theory Topological_Space
imports Complex_Main
"Jacobson_Basic_Algebra.Set_Theory"
Set_Extras

begin

section ‹Topological Spaces›

locale topological_space = fixes S :: "'a set" and is_open :: "'a set ⇒ bool"
assumes open_space [simp, intro]: "is_open S" and open_empty [simp, intro]: "is_open {}"
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)"

begin

definition is_closed :: "'a set ⇒ bool"
where "is_closed U ≡ U ⊆ S ∧ is_open (S - U)"

definition neighborhoods:: "'a ⇒ ('a set) set"
where "neighborhoods x ≡ {U. is_open U ∧ x ∈ U}"

text ‹Note that by a neighborhood we mean what some authors call an open neighborhood.›

lemma open_union' [intro]: "⋀F::('a set) set. (⋀x. x ∈ F ⟹ is_open x) ⟹ is_open (⋃F)"
using open_union by auto

lemma open_preimage_identity [simp]: "is_open B ⟹ identity S ⇧¯ S B = B"
by (metis inf.orderE open_imp_subset preimage_identity_self)

definition is_connected:: "bool" where
"is_connected ≡ ¬ (∃U V. is_open U ∧ is_open V ∧ (U ≠ {}) ∧ (V ≠ {}) ∧ (U ∩ V = {}) ∧ (U ∪ V = S))"

definition is_hausdorff:: "bool" where
"is_hausdorff ≡
∀x y. (x ∈ S ∧ y ∈ S ∧ x ≠ y) ⟶ (∃U V. U ∈ neighborhoods x ∧ V ∈ neighborhoods y ∧ U ∩ V = {})"

end (* topological_space *)

text ‹T2 spaces are also known as Hausdorff spaces.›

locale t2_space = topological_space +
assumes hausdorff: "is_hausdorff"

subsection ‹Topological Basis›

inductive generated_topology :: "'a set ⇒ 'a set set ⇒ 'a set ⇒ bool"
for S :: "'a set" and B :: "'a set set"
where
UNIV: "generated_topology S B S"
| Int: "generated_topology S B (U ∩ V)"
if "generated_topology S B U" and "generated_topology S B V"
| UN: "generated_topology S B (⋃K)" if "(⋀U. U ∈ K ⟹ generated_topology S B U)"
| Basis: "generated_topology S B b" if "b ∈ B ∧ b ⊆ S"

lemma generated_topology_empty [simp]: "generated_topology S B {}"
by (metis UN Union_empty empty_iff)

lemma generated_topology_subset: "generated_topology S B U ⟹ U ⊆ S"
by (induct rule:generated_topology.induct) auto

lemma generated_topology_is_topology:
fixes S:: "'a set" and B:: "'a set set"
shows "topological_space S (generated_topology S B)"
by (simp add: Int UN UNIV generated_topology_subset topological_space_def)

subsection ‹Covers›

locale cover_of_subset =
fixes X:: "'a set" and U:: "'a set" and index:: "real set" and cover:: "real ⇒ 'a set"
(* We use real instead of index::"'b set" otherwise we get some troubles with locale sheaf_of_rings
in Comm_Ring_Theory.thy *)
assumes is_subset: "U ⊆ X" and are_subsets: "⋀i. i ∈ index ⟹ cover i ⊆ X"
and covering: "U ⊆ (⋃i∈index. cover i)"
begin

lemma
assumes "x ∈ U"
shows "∃i∈index. x ∈ cover i"
using assms covering by auto

definition select_index:: "'a ⇒ real"
where "select_index x ≡ SOME i. i ∈ index ∧ x ∈ cover i"

lemma cover_of_select_index:
assumes "x ∈ U"
shows "x ∈ cover (select_index x)"
using assms by (metis (mono_tags, lifting) UN_iff covering select_index_def someI_ex subset_iff)

lemma select_index_belongs:
assumes "x ∈ U"
shows "select_index x ∈ index"
using assms by (metis (full_types, lifting) UN_iff covering in_mono select_index_def tfl_some)

end (* cover_of_subset *)

locale open_cover_of_subset = topological_space X is_open + cover_of_subset X U I C
for X and is_open and U and I and C +
assumes are_open_subspaces: "⋀i. i∈I ⟹ is_open (C i)"
begin

lemma cover_of_select_index_is_open:
assumes "x ∈ U"
shows "is_open (C (select_index x))"
using assms by (simp add: are_open_subspaces select_index_belongs)

end (* open_cover_of_subset *)

locale open_cover_of_open_subset = open_cover_of_subset X is_open U I C
for X and is_open and U and I and C +
assumes is_open_subset: "is_open U"

subsection ‹Induced Topology›

locale ind_topology = topological_space X is_open for X and is_open +
fixes S:: "'a set"
assumes is_subset: "S ⊆ X"
begin

definition ind_is_open:: "'a set ⇒ bool"
where "ind_is_open U ≡ U ⊆ S ∧ (∃V. V ⊆ X ∧ is_open V ∧ U = S ∩ V)"

lemma ind_is_open_S [iff]: "ind_is_open S"
by (metis ind_is_open_def inf.orderE is_subset open_space order_refl)

lemma ind_is_open_empty [iff]: "ind_is_open {}"
using ind_is_open_def by auto

lemma ind_space_is_top_space:
shows "topological_space S (ind_is_open)"
proof
fix U V
assume "ind_is_open U" then obtain UX where "UX ⊆ X" "is_open UX" "U = S ∩ UX"
using ind_is_open_def by auto
moreover
assume "ind_is_open V" then obtain VX where "VX ⊆ X" "is_open VX" "V = S ∩ VX"
using ind_is_open_def by auto
ultimately have "is_open (UX ∩ VX) ∧ (U ∩ V = S ∩ (UX ∩ VX))" using open_inter by auto
then show "ind_is_open (U ∩ V)"
by (metis ‹UX ⊆ X› ind_is_open_def le_infI1 subset_refl)
next
fix F
assume F: "⋀x. x ∈ F ⟹ ind_is_open x"
obtain F' where F': "⋀x. x ∈ F ∧ ind_is_open x ⟹ is_open (F' x) ∧ x = S ∩ (F' x)"
using ind_is_open_def by metis
have "is_open (⋃ (F' ` F))"
by (metis (mono_tags, lifting) F F' imageE image_ident open_union)
moreover
have "(⋃x∈F. x) = S ∩ ⋃ (F' ` F)"
using F' ‹⋀x. x ∈ F ⟹ ind_is_open x› by fastforce
ultimately show "ind_is_open (⋃x∈F. x)"
by (metis ind_is_open_def inf_sup_ord(1) open_imp_subset)
next
show "⋀U. ind_is_open U ⟹ U ⊆ S"
qed auto

lemma is_open_from_ind_is_open:
assumes "is_open S" and "ind_is_open U"
shows "is_open U"
using assms open_inter ind_is_open_def is_subset by auto

lemma open_cover_from_ind_open_cover:
assumes "is_open S" and "open_cover_of_open_subset S ind_is_open U I C"
shows "open_cover_of_open_subset X is_open U I C"
proof
show "is_open U"
using assms is_open_from_ind_is_open open_cover_of_open_subset.is_open_subset by blast
show "⋀i. i ∈ I ⟹ is_open (C i)"
using assms is_open_from_ind_is_open open_cover_of_open_subset_def open_cover_of_subset.are_open_subspaces by blast
show "⋀i. i ∈ I ⟹ C i ⊆ X"
using assms(2) is_subset
by (meson cover_of_subset_def open_cover_of_open_subset_def open_cover_of_subset_def subset_trans)
show "U ⊆ X"
by (simp add: ‹is_open U› open_imp_subset)
show "U ⊆ ⋃ (C ` I)"
by (meson assms(2) cover_of_subset_def open_cover_of_open_subset_def open_cover_of_subset_def)
qed

end (* induced topology *)

lemma (in topological_space) ind_topology_is_open_self [iff]: "ind_topology S is_open S"
by (simp add: ind_topology_axioms_def ind_topology_def topological_space_axioms)

lemma (in topological_space) ind_topology_is_open_empty [iff]: "ind_topology S is_open {}"
by (simp add: ind_topology_axioms_def ind_topology_def topological_space_axioms)

lemma (in topological_space) ind_is_open_iff_open:
shows "ind_topology.ind_is_open S is_open S U ⟷ is_open U ∧ U ⊆ S"
by (metis ind_topology.ind_is_open_def ind_topology_is_open_self inf.absorb_iff2)

subsection ‹Continuous Maps›

locale continuous_map = source: topological_space S is_open + target: topological_space S' is_open'
+ map f S S'
for S and is_open and S' and is_open' and f +
assumes is_continuous: "⋀U. is_open' U ⟹ is_open (f⇧¯ S U)"
begin

lemma open_cover_of_open_subset_from_target_to_source:
assumes "open_cover_of_open_subset S' is_open' U I C"
shows "open_cover_of_open_subset S is_open (f⇧¯ S U) I (λi. f⇧¯ S (C i))"
proof
show "f ⇧¯ S U ⊆ S" by simp
show "f ⇧¯ S (C i) ⊆ S" if "i ∈ I" for i
using that by simp
show "is_open (f ⇧¯ S U)"
by (meson assms is_continuous open_cover_of_open_subset.is_open_subset)
show "⋀i. i ∈ I ⟹ is_open (f ⇧¯ S (C i))"
by (meson assms is_continuous open_cover_of_open_subset_def open_cover_of_subset.are_open_subspaces)
show "f ⇧¯ S U ⊆ (⋃i∈I. f ⇧¯ S (C i))"
using assms unfolding open_cover_of_open_subset_def cover_of_subset_def open_cover_of_subset_def
by blast
qed

end (* continuous map *)

subsection ‹Homeomorphisms›

text ‹The topological isomorphisms between topological spaces are called homeomorphisms.›

locale homeomorphism =
continuous_map + bijective_map f S S' +
continuous_map S' is_open' S is_open "inverse_map f S S'"

lemma (in topological_space) id_is_homeomorphism:
shows "homeomorphism S is_open S is_open (identity S)"
proof
show "inverse_map (identity S) S S ∈ S →⇩E S"
qed (auto simp: open_inter bij_betwI')

subsection ‹Topological Filters› (* Imported from HOL.Topological_Spaces *)

definition (in topological_space) nhds :: "'a ⇒ 'a filter"
where "nhds a = (INF S∈{S. is_open S ∧ a ∈ S}. principal S)"

abbreviation (in topological_space)
tendsto :: "('b ⇒ 'a) ⇒ 'a ⇒ 'b filter ⇒ bool"  (infixr "⤏" 55)
where "(f ⤏ l) F ≡ filterlim f (nhds l) F"

definition (in t2_space) Lim :: "'f filter ⇒ ('f ⇒ 'a) ⇒ 'a"
where "Lim A f = (THE l. (f ⤏ l) A)"

end
```