(* Title: Topology.thy Author: Stefan Friedrich Maintainer: Stefan Friedrich License: LGPL *) 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" by (simp add: is_open_def) 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" by (simp add: double_diff) 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 subsubsection‹Adherent points› definition adhs :: "'a top ⇒ 'a ⇒ 'a set ⇒ bool" (infix "adhı" 50) where "adhs T x A ⟷ (∀ U ∈ nhd T x. U ∩ A ≠ {})" lemma (in carrier) adhCE [elim?]: "⟦x adh A; U ∉ nhds x ⟹ R; U ∩ A ≠ {} ⟹ R⟧ ⟹ R" by (unfold adhs_def) auto lemma (in carrier) adhI [intro]: "(⋀U. U ∈ nhds x ⟹ U ∩ A ≠ {}) ⟹ x adh A" by (unfold adhs_def) simp lemma (in carrier) closure_imp_adh: assumes asub: "A ⊆ carrier" and closure: "x ∈ closure A" shows "x adh 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 lemma (in carrier) adh_imp_closure: assumes xpoint: "x ∈ carrier" and adh: "x adh A" 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 ≠ {}" by (auto elim: adhCE) with asubc show "False" by auto qed lemma (in topology) closed_adh: 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)" by (fast dest!: adh_imp_closure) 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 by (auto dest!: closure_imp_adh) qed thus "A closed" by (auto intro: closure_eq_closed) qed lemma (in carrier) adh_closure_iff: "⟦ A ⊆ carrier; x ∈ carrier ⟧ ⟹ (x adh A) = (x ∈ closure A)" by (auto dest: adh_imp_closure closure_imp_adh) subsection‹More about closure and core› 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)" hence xadh: "x adh carrier - A" by (auto intro: closure_imp_adh) moreover assume xcore: "x ∈ core A" hence "core A ∈ nhds x" by auto ultimately have "core A ∩ (carrier - A) ≠ {}" by (auto elim: adhCE) 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 by (auto dest!: closure_imp_adh elim!: adhCE) 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 by (auto dest: closure_imp_adh) 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" by (simp add: diff_diff_inter subset_closure) 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" by (simp add: diff_diff_inter subset_closure) 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" by (auto simp add: cnt_def) 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 elim!: continuousE simp add: vimage_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 (simp add: filters_def) 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) lemma ultraD: 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 ultraD = ultraD [OF ultra] 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 from asub xclosure have adhx: "x adh A" by (rule closure_imp_adh) 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 have "x adh A" 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 by (rule adh_imp_closure) 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