(* Title: Examples/SML_Relativization/Topology/SML_Topological_Space.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins *) section‹Relativization of the results about simple topological spaces› theory SML_Topological_Space imports "../Simple_Orders/SML_Simple_Orders" "HOL-Analysis.Elementary_Topology" "../Foundations/Transfer_Ext" "../Foundations/Lifting_Set_Ext" begin subsection‹Definitions and common properties› text‹ Some of the entities that are presented in this subsection were copied from the theory \<^text>‹HOL-Types_To_Sets/Examples/T2_Spaces›. › locale topological_space_ow = fixes U :: "'at set" and τ :: "'at set ⇒ bool" assumes open_UNIV[simp, intro]: "τ U" assumes open_Int[intro]: "⟦ S ⊆ U; T ⊆ U; τ S; τ T ⟧ ⟹ τ (S ∩ T)" assumes open_Union[intro]: "⟦ K ⊆ Pow U; ∀S∈K. τ S ⟧ ⟹ τ (⋃K)" begin context includes lifting_syntax begin tts_register_sbts τ | U proof- assume dom_ATA: "Domainp ATA = (λx. x ∈ U)" and "bi_unique ATA" and "right_total ATA" from ‹bi_unique ATA› ‹right_total ATA› obtain Rep :: "'a ⇒ 'at" and Abs :: "'at ⇒ 'a" where td: "type_definition Rep Abs (Collect (Domainp ATA))" and ATA_Rep: "ATA b b' = (b = Rep b')" for b b' by (blast dest: ex_type_definition) define τ' where τ': "τ' = (image Rep ---> id) τ" have Domainp_scr_S: "Domainp (rel_set ATA) = (λx. x ⊆ U)" unfolding Domainp_set by (auto simp: dom_ATA) have scr_S_rep[intro, simp]: "rel_set ATA (image Rep a) a" for a unfolding rel_set_def by (auto simp: ATA_Rep) have rel_set_eq_rep_set: "rel_set ATA x y ⟷ x = image Rep y" for x y proof - have "bi_unique (rel_set ATA)" by (simp add: ‹bi_unique ATA› bi_unique_rel_set) from this show ?thesis by (auto dest: bi_uniqueDl) qed have "(rel_set ATA ===> (=)) τ τ'" unfolding τ' map_fun_apply id_def apply(intro rel_funI) unfolding rel_set_eq_rep_set apply(elim ssubst) .. then show " ∃τ'. (rel_set ATA ===> (=)) τ τ'" by auto qed end end locale topological_space_pair_ow = ts⇩_{1}: topological_space_ow U⇩_{1}τ⇩_{1}+ ts⇩_{2}: topological_space_ow U⇩_{2}τ⇩_{2}for U⇩_{1}:: "'at set" and τ⇩_{1}and U⇩_{2}:: "'bt set" and τ⇩_{2}locale topological_space_triple_ow = ts⇩_{1}: topological_space_ow U⇩_{1}τ⇩_{1}+ ts⇩_{2}: topological_space_ow U⇩_{2}τ⇩_{2}+ ts⇩_{3}: topological_space_ow U⇩_{3}τ⇩_{3}for U⇩_{1}:: "'at set" and τ⇩_{1}and U⇩_{2}:: "'bt set" and τ⇩_{2}and U⇩_{3}:: "'ct set" and τ⇩_{3}begin sublocale tsp⇩_{1}⇩_{2}: topological_space_pair_ow U⇩_{1}τ⇩_{1}U⇩_{2}τ⇩_{2}.. sublocale tsp⇩_{1}⇩_{3}: topological_space_pair_ow U⇩_{1}τ⇩_{1}U⇩_{3}τ⇩_{3}.. sublocale tsp⇩_{2}⇩_{3}: topological_space_pair_ow U⇩_{2}τ⇩_{2}U⇩_{3}τ⇩_{3}.. sublocale tsp⇩_{2}⇩_{1}: topological_space_pair_ow U⇩_{2}τ⇩_{2}U⇩_{1}τ⇩_{1}.. sublocale tsp⇩_{3}⇩_{1}: topological_space_pair_ow U⇩_{3}τ⇩_{3}U⇩_{1}τ⇩_{1}.. sublocale tsp⇩_{3}⇩_{2}: topological_space_pair_ow U⇩_{3}τ⇩_{3}U⇩_{2}τ⇩_{2}.. end inductive generate_topology_on :: "['at set set, 'at set, 'at set] ⇒ bool" ( ‹(in'_topology'_generated'_by _ on _ : «open» _)› [1000, 1000, 1000] 10 ) for S :: "'at set set" where UNIV: "(in_topology_generated_by S on U : «open» U)" | Int: "(in_topology_generated_by S on U : «open» (a ∩ b))" if "(in_topology_generated_by S on U : «open» a)" and "(in_topology_generated_by S on U : «open» b)" and "a ⊆ U" and "b ⊆ U" | UN: "(in_topology_generated_by S on U : «open» (⋃K))" if "K ⊆ Pow U" and "(⋀k. k ∈ K ⟹ (in_topology_generated_by S on U : «open» k))" | Basis: "(in_topology_generated_by S on U : «open» s)" if "s ∈ S" and "s ⊆ U" lemma gto_imp_ss: "(in_topology_generated_by S on U : «open» A) ⟹ A ⊆ U" by (induction rule: generate_topology_on.induct) auto lemma gt_eq_gto: "generate_topology = (λS. generate_topology_on S UNIV)" proof(intro ext iffI) fix S and x :: "'a set" assume "generate_topology S x" then show "in_topology_generated_by S on UNIV : «open» x" by (induction rule: generate_topology.induct) (simp_all add: UNIV Int UN Basis) next fix S and x :: "'a set" assume gto: "in_topology_generated_by S on UNIV : «open» x" define U where U: "U = (UNIV::'a set)" from gto have "generate_topology_on S U x" unfolding U . from this U show "generate_topology S x" by (induction rule: generate_topology_on.induct) ( simp_all add: generate_topology.UNIV generate_topology.Int generate_topology.UN generate_topology.Basis ) qed ud ‹topological_space.closed› (‹(with _ : «closed» _)› [1000, 1000] 10) ud closed' ‹closed› ud ‹topological_space.compact› (‹(with _ : «compact» _)› [1000, 1000] 10) ud compact' ‹compact› ud ‹topological_space.connected› (‹(with _ : «connected» _)› [1000, 1000] 10) ud connected' ‹connected› ud ‹topological_space.islimpt› (‹(with _ : _ «islimpt» _)› [1000, 1000, 1000] 60) ud islimpt' ‹topological_space_class.islimpt› ud ‹interior› (‹(with _ : «interior» _)› [1000, 1000] 10) ud ‹closure› (‹(with _ : «closure» _)› [1000, 1000] 10) ud ‹frontier› (‹(with _ : «frontier» _)› [1000, 1000] 10) ud ‹countably_compact› (‹(with _ : «countably'_compact» _)› [1000, 1000] 10) definition topological_basis_with :: "['a set ⇒ bool, 'a set set] ⇒ bool" (‹(with _ : «topological'_basis» _)› [1000, 1000] 10) where "(with τ : «topological_basis» B) = (⋃B = UNIV ∧ (∀b ∈ B. τ b) ∧ (∀q. τ q ⟶ (∃B'⊆B. ⋃B' = q)))" ctr relativization synthesis ctr_simps assumes [transfer_domain_rule, transfer_rule]: "Domainp A = (λx. x ∈ U)" and [transfer_rule]: "bi_unique A" "right_total A" trp (?'a A) in closed_ow: closed.with_def (‹(on _ with _ : «closed» _)› [1000, 1000] 10) and compact_ow: compact.with_def (‹(on _ with _ : «compact» _)› [1000, 1000, 1000] 10) and connected_ow: connected.with_def (‹(on _ with _ : «connected» _)› [1000, 1000, 1000] 10) and islimpt_ow: islimpt.with_def (‹(on _ with _ : _ «islimpt» _)› [1000, 1000, 1000, 1000] 10) and interior_ow: interior.with_def (‹(on _ with _ : «interior» _)› [1000, 1000, 1000] 10) and closure_ow: closure.with_def (‹(on _ with _ : «closure» _)› [1000, 1000, 1000] 10) and frontier_ow: frontier.with_def (‹(on _ with _ : «frontier» _)› [1000, 1000, 1000] 10) and countably_compact_ow: countably_compact.with_def (‹(on _ with _ : «countably'_compact» _)› [1000, 1000, 1000] 10) context topological_space_ow begin abbreviation closed where "closed ≡ closed_ow U τ" abbreviation compact where "compact ≡ compact_ow U τ" abbreviation connected where "connected ≡ connected_ow U τ" abbreviation islimpt (infixr ‹«islimpt»› 60) where "x «islimpt» S ≡ on U with τ : x «islimpt» S" abbreviation interior where "interior ≡ interior_ow U τ" abbreviation closure where "closure ≡ closure_ow U τ" abbreviation frontier where "frontier ≡ frontier_ow U τ" abbreviation countably_compact where "countably_compact ≡ countably_compact_ow U τ" end context includes lifting_syntax begin private lemma Domainp_fun_rel_eq_subset: fixes A :: "['a, 'c] ⇒ bool" fixes B :: "['b, 'd] ⇒ bool" assumes "bi_unique A" "bi_unique B" shows "Domainp (A ===> B) = (λf. f ` (Collect (Domainp A)) ⊆ (Collect (Domainp B)))" proof(intro ext, standard) let ?sA = "Collect (Domainp A)" and ?sB = "(Collect (Domainp B))" fix f assume "Domainp (A ===> B) f" show "f ` ?sA ⊆ ?sB" proof(clarsimp) fix x x' assume "A x x'" from ‹Domainp (A ===> B) f› obtain f' where f': "A x x' ⟹ B (f x) (f' x')" for x x' unfolding rel_fun_def by auto with ‹A x x'› have "B (f x) (f' x')" by simp thus "Domainp B (f x)" by auto qed next let ?sA = "Collect (Domainp A)" and ?sB = "(Collect (Domainp B))" fix f assume "f ` ?sA ⊆ ?sB" define f' where f': "f' = (λx'. (THE y'. ∃x. A x x' ∧ B (f x) y'))" have "(A ===> B) f f'" proof(intro rel_funI) fix x x' assume "A x x'" then have "f x ∈ ?sB" using ‹f ` ?sA ⊆ ?sB› by auto then obtain y' where y': "B (f x) y'" by clarsimp have "f' x' = y'" unfolding f' proof from ‹A x x'› y' show "∃x. A x x' ∧ B (f x) y'" by auto { fix y'' assume "∃x. A x x' ∧ B (f x) y''" then obtain x'' where x'': "A x'' x' ∧ B (f x'') y''" by clarsimp with assms(1) have "x'' = x" using ‹A x x'› by (auto dest: bi_uniqueDl) with y' x'' have "y'' = y'" using assms(2) by (auto dest: bi_uniqueDr) } thus "∃x. A x x' ∧ B (f x) y'' ⟹ y'' = y'" for y'' by simp qed thus "B (f x) (f' x')" using y' by simp qed thus "Domainp (A ===> B) f" by auto qed private lemma Ex_rt_bu_transfer[transfer_rule]: fixes A :: "['a, 'c] ⇒ bool" fixes B :: "['b, 'd] ⇒ bool" assumes [transfer_rule]: "bi_unique A" "right_total A" "bi_unique B" shows "(((B ===> A) ===> (=)) ===> (=)) (Bex (Collect (λf. f ` (Collect (Domainp B)) ⊆ (Collect (Domainp A))))) Ex" proof- from assms(3,1) have domainp_eq_ss: "Domainp (B ===> A) = (λf. f ` (Collect (Domainp B)) ⊆ (Collect (Domainp A)))" by (rule Domainp_fun_rel_eq_subset) have "right_total (B ===> A)" using assms by (simp add: bi_unique_alt_def right_total_fun) then have "(((B ===> A) ===> (=)) ===> (=)) (Bex (Collect (Domainp (B ===> A)))) Ex" by (simp add: right_total_Ex_transfer) thus ?thesis unfolding domainp_eq_ss by simp qed end definition topological_basis_ow :: "['a set, 'a set ⇒ bool, 'a set set] ⇒ bool" (‹(on _ with _ : «topological'_basis» _)› [1000, 1000, 1000] 10) where "(on U with τ : «topological_basis» B) = (⋃B = U ∧ (∀b ∈ B. τ b) ∧ (∀q ⊆ U. τ q ⟶ (∃B'⊆ B. ⋃B' = q)))" context topological_space begin lemma topological_basis_with[ud_with]: "topological_basis = topological_basis_with open" unfolding topological_basis_def topological_basis_with_def Ball_def by (intro ext) (metis Union_mono open_UNIV top.extremum_uniqueI) end subsection‹Transfer rules› text‹Some of the entities that are presented in this subsectionwere copied from \<^text>‹HOL-Types_To_Sets/Examples/T2_Spaces›.› context includes lifting_syntax begin lemmas vimage_transfer[transfer_rule] = vimage_transfer lemma topological_space_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((rel_set A ===> (=)) ===> (=)) (topological_space_ow (Collect (Domainp A))) class.topological_space" unfolding topological_space_ow_def class.topological_space_def apply transfer_prover_start apply transfer_step+ unfolding Pow_def Ball_Collect[symmetric] by auto lemma generate_topology_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((rel_set (rel_set A)) ===> (rel_set A ===> (=))) (λB. generate_topology_on B (Collect (Domainp A))) generate_topology" proof(intro rel_funI, standard) fix BL BR xl xr assume rsrsT_BLR: "rel_set (rel_set A) BL BR" and rsT_xl_xr: "rel_set A xl xr" and gto: "generate_topology_on BL (Collect (Domainp A)) xl" define CDT where CDT: "CDT = (Collect (Domainp A))" with gto have gto_CDT: "generate_topology_on BL CDT xl" by simp from gto_CDT CDT rsrsT_BLR rsT_xl_xr show "generate_topology BR xr" proof(induction arbitrary: xr rule: generate_topology_on.induct) case (UNIV S) show ?case proof - from assms UNIV.prems have "xr = UNIV" by (meson bi_uniqueDr bi_unique_rel_set right_total_UNIV_transfer) thus "generate_topology BR xr" by (simp add: generate_topology.UNIV) qed next case (Int S a b) show ?case proof - from Int.hyps(3) Int.prems(1) obtain a' where a': "rel_set A a a'" by (metis Ball_Collect Domainp_iff Domainp_set) from Int.hyps(4) Int.prems(1) obtain b' where b': "rel_set A b b'" by (metis Ball_Collect Domainp_iff Domainp_set) from Int.prems(1) Int.prems(2) a' have gt_a': "generate_topology BR a'" by (rule Int.IH(1)) from Int.prems(1) Int.prems(2) b' have gt_b': "generate_topology BR b'" by (rule Int.IH(2)) from gt_a' gt_b' have "generate_topology BR (a' ∩ b')" by (rule generate_topology.Int) also from assms(1) a' b' Int.prems(3) have "a' ∩ b' = xr" by (rule bi_unique_intersect_r) ultimately show "generate_topology BR xr" by simp qed next case (UN K S) thus ?case proof - define K' where K': "K' = {(x, y). rel_set A x y} `` K" (is "K' = ?K'") have Union_ss_CDT: "⋃K ⊆ Collect (Domainp A)" by (metis CollectI Domainp.DomainI UN.prems(3) rel_setD1 subsetI) from assms(1) Union_ss_CDT UN.prems(3) have "⋃?K' = xr" by (rule bi_unique_Union_r) then have UK_eq_xr: "⋃K' = xr" unfolding K' . have "k' ∈ K' ⟹ generate_topology BR k'" for k' proof - assume k'_in_K': "k' ∈ K'" then obtain k where k: "rel_set A k k'" unfolding K' by auto from assms(1) have "bi_unique (rel_set A)" by (rule bi_unique_rel_set) with k have "∃!k. rel_set A k k'" by (meson bi_uniqueDl) with k'_in_K' k have k_in_K: "k ∈ K" unfolding K' by auto from k_in_K UN.prems(1,2) k show "generate_topology BR k'" by (rule UN.IH) qed then have "generate_topology BR (⋃K')" by (rule generate_topology.UN) with UK_eq_xr show "generate_topology BR xr" by simp qed next case (Basis xl S) thus ?case using assms(1) by (metis Int_absorb1 bi_unique_intersect_r generate_topology.Basis rel_setD1 subset_refl) qed next fix BL BR xl xr assume rsrsT_BLR: "rel_set (rel_set A) BL BR" and rsT_xl_xr: "rel_set A xl xr" and gt: "generate_topology BR xr" from gt rsrsT_BLR rsT_xl_xr show "generate_topology_on BL (Collect (Domainp A)) xl" proof(induction arbitrary: xl rule: generate_topology.induct) case UNIV thus ?case using assms by (metis bi_uniqueDl bi_unique_rel_set generate_topology_on.simps right_total_UNIV_transfer) next case (Int a' b') show ?case proof - from assms(2) obtain a where a: "rel_set A a a'" by (meson right_totalE right_total_rel_set) from assms(2) obtain b where b: "rel_set A b b'" by (meson right_totalE right_total_rel_set) from Int.prems(1) a have gto_a: "generate_topology_on BL {x. Domainp A x} a" by (rule Int.IH(1)) from Int.prems(1) b have gto_b: "generate_topology_on BL {x. Domainp A x} b" by (rule Int.IH(2)) from a have a_ss_DT: "a ⊆ {x. Domainp A x}" by auto (meson Domainp.DomainI rel_setD1) from b have b_ss_DT: "b ⊆ {x. Domainp A x}" by auto (meson Domainp.DomainI rel_setD1) from gto_a gto_b a_ss_DT b_ss_DT have "generate_topology_on BL {x. Domainp A x} (a ∩ b)" by (rule generate_topology_on.Int) also from assms(1) a b Int.prems(2) have "a ∩ b = xl" by (rule bi_unique_intersect_l) ultimately show "generate_topology_on BL {a. Domainp A a} xl" by simp qed next case (UN K') thus ?case proof - define K where K: "K = {(x, y). rel_set (λy x. A x y) x y} `` K'" (is "K = ?K") from assms(2) have Union_ss_CRT: "⋃K' ⊆ Collect (Rangep A)" by (auto simp add: Domainp_iff right_total_def) from assms(1) Union_ss_CRT UN.prems(2) have "⋃?K = xl" by (rule bi_unique_Union_l) then have UK_eq_xr: "⋃K = xl" unfolding K . then have "K ⊆ Pow xl" by blast moreover from UN.prems(2) have "xl ⊆ {x. Domainp A x}" unfolding rel_set_def by blast ultimately have UN_prem_1: "K ⊆ Pow {x. Domainp A x}" by auto have UN_prem_2: "k ∈ K ⟹ generate_topology_on BL {x. Domainp A x} k" for k proof - assume k_in_K: "k ∈ K" with UN_prem_1 have k_ss_DT: "k ⊆ {x. Domainp A x}" by auto with k_in_K obtain k' where k': "rel_set (λy x. A x y) k' k" unfolding K Ball_Collect[symmetric] by blast from assms(1) have "bi_unique (λy x. A x y)" unfolding bi_unique_def by simp then have "bi_unique (rel_set (λy x. A x y))" by (rule bi_unique_rel_set) with k' have "∃!k'. rel_set (λy x. A x y) k' k" by (meson bi_uniqueDl) with k_in_K k' have k'_in_K': "k' ∈ K'" unfolding K by blast from k' have rsT_kk': "rel_set A k k'" unfolding rel_set_def by auto from k'_in_K' UN.prems(1) rsT_kk' show "generate_topology_on BL {x. Domainp A x} k" by (rule UN.IH) qed from UN_prem_1 UN_prem_2 have "generate_topology_on BL {x. Domainp A x} (⋃K)" by (rule generate_topology_on.UN) with UK_eq_xr show "generate_topology_on BL {a. Domainp A a} xl" by simp qed next case (Basis xr) thus ?case proof - assume xr_in_BR: "xr ∈ BR" and rsrsT_BL_BR: "rel_set (rel_set A) BL BR" and rsT_xl_xr: "rel_set A xl xr" with assms(1) have "xl ∈ BL" by (metis bi_uniqueDl bi_unique_rel_set rel_setD2) also with rsrsT_BL_BR have "xl ⊆ {a. Domainp A a}" unfolding Ball_Collect[symmetric] by (meson Domainp.DomainI rel_setD1) ultimately show "generate_topology_on BL {a. Domainp A a} xl" by (rule generate_topology_on.Basis) qed qed qed lemma topological_basis_with_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((rel_set A ===> (=)) ===> (rel_set (rel_set A)) ===> (=)) (topological_basis_ow (Collect (Domainp A))) topological_basis_with" unfolding topological_basis_ow_def topological_basis_with_def apply transfer_prover_start apply transfer_step+ unfolding Ball_Collect[symmetric] apply(clarsimp, intro ext iffI) subgoal by (metis UnionI) subgoal by metis done end subsection‹Relativization› tts_context tts: (?'a to ‹U⇩_{1}::'a set›) and (?'b to ‹U⇩_{2}::'b set›) rewriting ctr_simps begin tts_lemma generate_topology_Union: assumes "U⇩_{1}≠ {}" and "U⇩_{2}≠ {}" and "I ⊆ U⇩_{1}" and "S ⊆ Pow U⇩_{2}" and "∀x∈U⇩_{1}. K (x::'a) ⊆ U⇩_{2}" and "⋀k. ⟦k ∈ U⇩_{1}; k ∈ I⟧ ⟹ in_topology_generated_by S on U⇩_{2}: «open» (K k)" shows "in_topology_generated_by S on U⇩_{2}: «open» (⋃ (K ` I))" is generate_topology_Union. end tts_context tts: (?'a to ‹U::'a set›) rewriting ctr_simps eliminating through (unfold topological_space_ow_def; auto intro: generate_topology_on.intros) begin tts_lemma topological_space_generate_topology: shows "topological_space_ow U (generate_topology_on S U)" is topological_space_generate_topology. end context topological_space_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting topological_space_ow_axioms eliminating through (metis open_UNIV) begin tts_lemma open_empty[simp]: shows "τ {}" is topological_space_class.open_empty. end tts_context tts: (?'a to U) rewriting ctr_simps substituting topological_space_ow_axioms eliminating through ( unfold closed_ow_def compact_ow_def connected_ow_def interior_ow_def closure_ow_def frontier_ow_def, auto ) begin tts_lemma closed_empty[simp]: "closed {}" is topological_space_class.closed_empty. tts_lemma closed_UNIV[simp]: "closed U" is topological_space_class.closed_UNIV. tts_lemma compact_empty[simp]: "compact {}" is topological_space_class.compact_empty. tts_lemma connected_empty[simp]: "connected {}" is topological_space_class.connected_empty. tts_lemma interior_empty[simp]: "interior {} = {}" is interior_empty. tts_lemma closure_empty[simp]: "closure {} = {}" is closure_empty. tts_lemma closure_UNIV[simp]: "closure U = U" is closure_UNIV. tts_lemma frontier_empty[simp]: "frontier {} = {}" is frontier_empty. tts_lemma frontier_UNIV[simp]: "frontier U = {}" is frontier_UNIV. end tts_context tts: (?'a to U) rewriting ctr_simps substituting topological_space_ow_axioms eliminating through (auto simp: UNIV inj_on_def) begin tts_lemma connected_Union: assumes "S ⊆ Pow U" and "⋀s. s ∈ S ⟹ connected s" and "⋂ S ∩ U ≠ {}" shows "connected (⋃ S)" given Topological_Spaces.connected_Union by simp tts_lemma connected_Un: assumes "s ⊆ U" and "t ⊆ U" and "connected s" and "connected t" and "s ∩ t ≠ {}" shows "connected (s ∪ t)" is Topological_Spaces.connected_Un. end tts_context tts: (?'a to U) rewriting ctr_simps substituting topological_space_ow_axioms eliminating ‹?U ≠ {}› and ‹?A ⊆ ?B› through (auto simp: UNIV inj_on_def) begin tts_lemma connected_sing: assumes "x ∈ U" shows "connected {x}" is topological_space_class.connected_sing. tts_lemma topological_basisE: assumes "B ⊆ Pow U" and "O' ⊆ U" and "x ∈ U" and "on U with τ : «topological_basis» B" and "τ O'" and "x ∈ O'" and "⋀B'. ⟦B' ⊆ U; B' ∈ B; x ∈ B'; B' ⊆ O'⟧ ⟹ thesis" shows thesis is topological_space_class.topological_basisE. tts_lemma islimptE: assumes "x ∈ U" and "S ⊆ U" and "T ⊆ U" and "x «islimpt» S" and "x ∈ T" and "τ T" and "⋀y. ⟦y ∈ U; y ∈ S; y ∈ T; y ≠ x⟧ ⟹ thesis" shows thesis is Elementary_Topology.islimptE. tts_lemma islimpt_subset: assumes "x ∈ U" and "T ⊆ U" and "x «islimpt» S" and "S ⊆ T" shows "x «islimpt» T" is Elementary_Topology.islimpt_subset. tts_lemma islimpt_UNIV_iff: assumes "x ∈ U" shows "x «islimpt» U = (¬ τ {x})" is Elementary_Topology.islimpt_UNIV_iff. tts_lemma islimpt_punctured: assumes "x ∈ U" and "S ⊆ U" shows "x «islimpt» S = x «islimpt» S - {x}" is Elementary_Topology.islimpt_punctured. tts_lemma islimpt_EMPTY: assumes "x ∈ U" shows "¬ x «islimpt» {}" is Elementary_Topology.islimpt_EMPTY. tts_lemma islimpt_Un: assumes "x ∈ U" and "S ⊆ U" and "T ⊆ U" shows "x «islimpt» S ∪ T = (x «islimpt» S ∨ x «islimpt» T)" is Elementary_Topology.islimpt_Un. tts_lemma interiorI: assumes "x ∈ U" and "S ⊆ U" and "τ T" and "x ∈ T" and "T ⊆ S" shows "x ∈ interior S" is Elementary_Topology.interiorI. tts_lemma islimpt_in_closure: assumes "x ∈ U" and "S ⊆ U" shows "x «islimpt» S = (x ∈ closure (S - {x}))" is Elementary_Topology.islimpt_in_closure. tts_lemma compact_sing: assumes "a ∈ U" shows "compact {a}" is Elementary_Topology.compact_sing. tts_lemma compact_insert: assumes "s ⊆ U" and "x ∈ U" and "compact s" shows "compact (insert x s)" is Elementary_Topology.compact_insert. tts_lemma open_Un: assumes "S ⊆ U" and "T ⊆ U" and "τ S" and "τ T" shows "τ (S ∪ T)" is topological_space_class.open_Un. tts_lemma open_Inter: assumes "S ⊆ Pow U" and "finite S" and "Ball S τ" shows "τ (⋂ S ∩ U)" is topological_space_class.open_Inter. tts_lemma openI: assumes "S ⊆ U" and "⋀x. ⟦x ∈ U; x ∈ S⟧ ⟹ ∃y⊆U. τ y ∧ y ⊆ S ∧ x ∈ y" shows "τ S" given topological_space_class.openI by (meson PowI) tts_lemma closed_Un: assumes "S ⊆ U" and "T ⊆ U" and "closed S" and "closed T" shows "closed (S ∪ T)" is topological_space_class.closed_Un. tts_lemma closed_Int: assumes "S ⊆ U" and "T ⊆ U" and "closed S" and "closed T" shows "closed (S ∩ T)" is topological_space_class.closed_Int. tts_lemma open_Collect_conj: assumes "τ {x. P x ∧ x ∈ U}" and "τ {x. Q x ∧ x ∈ U}" shows "τ {x ∈ U. P x ∧ Q x}" is topological_space_class.open_Collect_conj. tts_lemma open_Collect_disj: assumes "τ {x. P x ∧ x ∈ U}" and "τ {x. Q x ∧ x ∈ U}" shows "τ {x ∈ U. P x ∨ Q x}" is topological_space_class.open_Collect_disj. tts_lemma open_Collect_imp: assumes "closed {x. P x ∧ x ∈ U}" and "τ {x. Q x ∧ x ∈ U}" shows "τ {x ∈ U. P x ⟶ Q x}" is topological_space_class.open_Collect_imp. tts_lemma open_Collect_const: "τ {x. P ∧ x ∈ U}" is topological_space_class.open_Collect_const. tts_lemma closed_Collect_conj: assumes "closed {x. P x ∧ x ∈ U}" and "closed {x. Q x ∧ x ∈ U}" shows "closed {x ∈ U. P x ∧ Q x}" is topological_space_class.closed_Collect_conj. tts_lemma closed_Collect_disj: assumes "closed {x. P x ∧ x ∈ U}" and "closed {x. Q x ∧ x ∈ U}" shows "closed {x ∈ U. P x ∨ Q x}" is topological_space_class.closed_Collect_disj. tts_lemma closed_Collect_imp: assumes "τ {x. P x ∧ x ∈ U}" and "closed {x. Q x ∧ x ∈ U}" shows "closed {x ∈ U. P x ⟶ Q x}" is topological_space_class.closed_Collect_imp. tts_lemma compact_Int_closed: assumes "S ⊆ U" and "T ⊆ U" and "compact S" and "closed T" shows "compact (S ∩ T)" is topological_space_class.compact_Int_closed. tts_lemma compact_diff: assumes "S ⊆ U" and "T ⊆ U" and "compact S" and "τ T" shows "compact (S - T)" is topological_space_class.compact_diff. tts_lemma connectedD: assumes "U ⊆ U" and "V ⊆ U" and "connected A" and "τ U" and "τ V" and "U ∩ (V ∩ A) = {}" and "A ⊆ U ∪ V" shows "U ∩ A = {} ∨ V ∩ A = {}" is topological_space_class.connectedD. tts_lemma topological_basis_open: assumes "B ⊆ Pow U" and "on U with τ : «topological_basis» B" and "X ∈ B" shows "τ X" is topological_space_class.topological_basis_open. tts_lemma topological_basis_imp_subbasis: assumes "B ⊆ Pow U" and "on U with τ : «topological_basis» B" shows "∀s⊆U. τ s = (in_topology_generated_by B on U : «open» s)" is topological_space_class.topological_basis_imp_subbasis. tts_lemma connected_closedD: assumes "A ⊆ U" and "B ⊆ U" and "connected s" and "A ∩ (B ∩ s) = {}" and "s ⊆ A ∪ B" and "closed A" and "closed B" shows "A ∩ s = {} ∨ B ∩ s = {}" is Topological_Spaces.connected_closedD. tts_lemma connected_diff_open_from_closed: assumes "u ⊆ U" and "s ⊆ t" and "t ⊆ u" and "τ s" and "closed t" and "connected u" and "connected (t - s)" shows "connected (u - s)" is Topological_Spaces.connected_diff_open_from_closed. tts_lemma interior_maximal: assumes "S ⊆ U" and "T ⊆ S" and "τ T" shows "T ⊆ interior S" is Elementary_Topology.interior_maximal. tts_lemma open_subset_interior: assumes "S ⊆ U" and "T ⊆ U" and "τ S" shows "(S ⊆ interior T) = (S ⊆ T)" is Elementary_Topology.open_subset_interior. tts_lemma interior_mono: assumes "T ⊆ U" and "S ⊆ T" shows "interior S ⊆ interior T" is Elementary_Topology.interior_mono. tts_lemma interior_Int: assumes "S ⊆ U" and "T ⊆ U" shows "interior (S ∩ T) = interior S ∩ interior T" is Elementary_Topology.interior_Int. tts_lemma interior_closed_Un_empty_interior: assumes "S ⊆ U" and "T ⊆ U" and "closed S" and "interior T = {}" shows "interior (S ∪ T) = interior S" is Elementary_Topology.interior_closed_Un_empty_interior. tts_lemma countably_compact_imp_acc_point: assumes "local.countably_compact s" and "countable t" and "infinite t" and "t ⊆ s" shows "∃x∈s. ∀U∈Pow U. τ U ∧ x ∈ U ⟶ infinite (U ∩ t)" is Elementary_Topology.countably_compact_imp_acc_point. end tts_context tts: (?'a to U) rewriting ctr_simps substituting topological_space_ow_axioms eliminating ‹?U ≠ {}› through (auto simp: UNIV inj_on_def) begin tts_lemma first_countableI: assumes "𝒜 ⊆ Pow U" and "x ∈ U" and "countable 𝒜" and "⋀A. ⟦A ∈ 𝒜⟧ ⟹ x ∈ A" and "⋀A. ⟦A ∈ 𝒜⟧ ⟹ τ A" and "⋀S. ⟦τ S; x ∈ S⟧ ⟹ ∃A∈𝒜. A ⊆ S" shows "∃𝒜∈{f. range f ⊆ Pow U}. (∀i. τ (𝒜 (i::nat)) ∧ x ∈ 𝒜 i) ∧ (∀S∈Pow U. τ S ∧ x ∈ S ⟶ (∃i. 𝒜 i ⊆ S))" given topological_space_class.first_countableI by auto tts_lemma islimptI: assumes "x ∈ U" and "S ⊆ U" and "⋀T. ⟦x ∈ T; τ T⟧ ⟹ ∃y∈S. y ∈ T ∧ y ≠ x" shows "x «islimpt» S" given Elementary_Topology.islimptI by simp tts_lemma interiorE: assumes "x ∈ U" and "S ⊆ U" and "x ∈ interior S" and "⋀T. ⟦T ⊆ U; τ T; x ∈ T; T ⊆ S⟧ ⟹ thesis" shows thesis is Elementary_Topology.interiorE. tts_lemma closure_iff_nhds_not_empty: assumes "x ∈ U" and "X ⊆ U" shows "(x ∈ closure X) = (∀y⊆U. ∀z⊆U. z ⊆ y ⟶ τ z ⟶ x ∈ z ⟶ X ∩ y ≠ {})" given Elementary_Topology.closure_iff_nhds_not_empty by auto tts_lemma basis_dense: assumes "B ⊆ Pow U" and "∀x⊆U. f x ∈ U" and "on U with τ : «topological_basis» B" and "⋀B'. ⟦B' ⊆ U; B' ≠ {}⟧ ⟹ f B' ∈ B'" shows "∀x⊆U. τ x ⟶ x ≠ {} ⟶ (∃y∈B. f y ∈ x)" given topological_space_class.basis_dense by auto tts_lemma inj_setminus: assumes "A ⊆ Pow U" shows "inj_on (λS. - S ∩ U) A" is topological_space_class.inj_setminus. end tts_context tts: (?'a to U) rewriting ctr_simps substituting topological_space_ow_axioms eliminating ‹?U ≠ {}› and ‹?S ⊆ U› through ( unfold closed_ow_def compact_ow_def connected_ow_def interior_ow_def topological_basis_ow_def closure_ow_def frontier_ow_def countably_compact_ow_def, auto ) begin tts_lemma closed_Inter: assumes "K ⊆ Pow U" and "Ball K closed" shows "closed (⋂ K ∩ U)" is topological_space_class.closed_Inter. tts_lemma closed_Union: assumes "S ⊆ Pow U" and "finite S" and "Ball S closed" shows "closed (⋃ S)" is topological_space_class.closed_Union. tts_lemma open_closed: assumes "S ⊆ U" shows "τ S = closed (- S ∩ U)" is topological_space_class.open_closed. tts_lemma closed_open: shows "closed S = τ (- S ∩ U)" is topological_space_class.closed_open. tts_lemma open_Diff: assumes "S ⊆ U" and "T ⊆ U" and "τ S" and "closed T" shows "τ (S - T)" is topological_space_class.open_Diff. tts_lemma closed_Diff: assumes "S ⊆ U" and "T ⊆ U" and "closed S" and "τ T" shows "closed (S - T)" is topological_space_class.closed_Diff. tts_lemma open_Compl: assumes "closed S" shows "τ (- S ∩ U)" is topological_space_class.open_Compl. tts_lemma closed_Compl: assumes "S ⊆ U" and "τ S" shows "closed (- S ∩ U)" is topological_space_class.closed_Compl. tts_lemma open_Collect_neg: assumes "closed {x ∈ U. P x}" shows "τ {x ∈ U. ¬ P x}" given topological_space_class.open_Collect_neg by (simp add: ctr_simps_conj_commute) tts_lemma closed_Collect_neg: assumes "τ {x∈U. P x}" shows "closed {x∈U. ¬ P x}" given topological_space_class.closed_Collect_neg by (simp add: ctr_simps_conj_commute) tts_lemma closed_Collect_const: "closed {x ∈ U. P}" given topological_space_class.closed_Collect_const by (simp add: ctr_simps_conj_commute) tts_lemma connectedI: assumes "⋀A B. ⟦ A ⊆ U; B ⊆ U; τ A; τ B; A ∩ U ≠ {}; B ∩ U ≠ {}; A ∩ (B ∩ U) = {}; U ⊆ A ∪ B ⟧ ⟹ False" shows "connected U" is topological_space_class.connectedI. tts_lemma topological_basis: assumes "B ⊆ Pow U" shows "(on U with τ : «topological_basis» B) = (∀x∈Pow U. τ x = (∃B'∈Pow (Pow U). B' ⊆ B ∧ ⋃ B' = x))" is topological_space_class.topological_basis. tts_lemma topological_basis_iff: assumes "B ⊆ Pow U" and "⋀B'. ⟦B' ⊆ U; B' ∈ B⟧ ⟹ τ B'" shows "(on U with τ : «topological_basis» B) = (∀O'∈Pow U. τ O' ⟶ (∀x∈O'. ∃B'∈B. B' ⊆ O' ∧ x ∈ B'))" is topological_space_class.topological_basis_iff. tts_lemma topological_basisI: assumes "B ⊆ Pow U" and "⋀B'. ⟦B' ⊆ U; B' ∈ B⟧ ⟹ τ B'" and "⋀O' x. ⟦O' ⊆ U; x ∈ U; τ O'; x ∈ O'⟧ ⟹ ∃y∈B. y ⊆ O' ∧ x ∈ y" shows "on U with τ : «topological_basis» B" is topological_space_class.topological_basisI. tts_lemma closed_closure: assumes "S ⊆ U" shows "closed (closure S)" is Elementary_Topology.closed_closure. tts_lemma closure_subset: "S ⊆ closure S" is Elementary_Topology.closure_subset. tts_lemma closure_eq: assumes "S ⊆ U" shows "(closure S = S) = closed S" is Elementary_Topology.closure_eq. tts_lemma closure_closed: assumes "S ⊆ U" and "closed S" shows "closure S = S" is Elementary_Topology.closure_closed. tts_lemma closure_closure: assumes "S ⊆ U" shows "closure (closure S) = closure S" is Elementary_Topology.closure_closure. tts_lemma closure_mono: assumes "T ⊆ U" and "S ⊆ T" shows "closure S ⊆ closure T" is Elementary_Topology.closure_mono. tts_lemma closure_minimal: assumes "T ⊆ U" and "S ⊆ T" and "closed T" shows "closure S ⊆ T" is Elementary_Topology.closure_minimal. tts_lemma closure_unique: assumes "T ⊆ U" and "S ⊆ T" and "closed T" and "⋀T'. ⟦T' ⊆ U; S ⊆ T'; closed T'⟧ ⟹ T ⊆ T'" shows "closure S = T" is Elementary_Topology.closure_unique. tts_lemma closure_Un: assumes "S ⊆ U" and "T ⊆ U" shows "closure (S ∪ T) = closure S ∪ closure T" is Elementary_Topology.closure_Un. tts_lemma closure_eq_empty: "(closure S = {}) = (S = {})" is Elementary_Topology.closure_eq_empty. tts_lemma closure_subset_eq: assumes "S ⊆ U" shows "(closure S ⊆ S) = closed S" is Elementary_Topology.closure_subset_eq. tts_lemma open_Int_closure_eq_empty: assumes "S ⊆ U" and "T ⊆ U" and "τ S" shows "(S ∩ closure T = {}) = (S ∩ T = {})" is Elementary_Topology.open_Int_closure_eq_empty. tts_lemma open_Int_closure_subset: assumes "S ⊆ U" and "T ⊆ U" and "τ S" shows "S ∩ closure T ⊆ closure (S ∩ T)" is Elementary_Topology.open_Int_closure_subset. tts_lemma closure_Un_frontier: "closure S = S ∪ frontier S" is Elementary_Topology.closure_Un_frontier. tts_lemma compact_imp_countably_compact: assumes "compact U" shows "countably_compact U" is Elementary_Topology.compact_imp_countably_compact. end tts_context tts: (?'a to U) rewriting ctr_simps substituting topological_space_ow_axioms eliminating through auto begin tts_lemma Heine_Borel_imp_Bolzano_Weierstrass: assumes "s ⊆ U" and "compact s" and "infinite t" and "t ⊆ s" shows "∃x∈s. x «islimpt» t" is Elementary_Topology.Heine_Borel_imp_Bolzano_Weierstrass. end tts_context tts: (?'a to U) rewriting ctr_simps substituting topological_space_ow_axioms eliminating ‹?U ≠ {}› through ( unfold closed_ow_def compact_ow_def connected_ow_def interior_ow_def topological_basis_ow_def closure_ow_def frontier_ow_def countably_compact_ow_def, auto simp: connected_iff_const ) begin tts_lemma connected_closed: assumes "s ⊆ U" shows "connected s = ( ¬(∃A∈Pow U. ∃B∈Pow U. closed A ∧ closed B ∧ s ⊆ A ∪ B ∧ A ∩ (B ∩ s) = {} ∧ A ∩ s ≠ {} ∧ B ∩ s ≠ {}) )" is Topological_Spaces.connected_closed. tts_lemma closure_complement: assumes "S ⊆ U" shows "closure (- S ∩ U) = - interior S ∩ U" is Elementary_Topology.closure_complement. tts_lemma interior_complement: assumes "S ⊆ U" shows "interior (- S ∩ U) = - closure S ∩ U" is Elementary_Topology.interior_complement. tts_lemma interior_diff: assumes "S ⊆ U" and "T ⊆ U" shows "interior (S - T) = interior S - closure T" is Elementary_Topology.interior_diff. tts_lemma connected_imp_connected_closure: assumes "S ⊆ U" and "connected S" shows "connected (closure S)" is Elementary_Topology.connected_imp_connected_closure. tts_lemma frontier_closed: assumes "S ⊆ U" shows "closed (frontier S)" is Elementary_Topology.frontier_closed. tts_lemma frontier_Int: assumes "S ⊆ U" and "T ⊆ U" shows "frontier (S ∩ T) = closure (S ∩ T) ∩ (frontier S ∪ frontier T)" is Elementary_Topology.frontier_Int. tts_lemma frontier_closures: assumes "S ⊆ U" shows "frontier S = closure S ∩ closure (- S ∩ U)" is Elementary_Topology.frontier_closures. tts_lemma frontier_Int_subset: assumes "S ⊆ U" and "T ⊆ U" shows "frontier (S ∩ T) ⊆ frontier S ∪ frontier T" is Elementary_Topology.frontier_Int_subset. tts_lemma frontier_Int_closed: assumes "S ⊆ U" and "T ⊆ U" and "closed S" and "closed T" shows "frontier (S ∩ T) = frontier S ∩ T ∪ S ∩ frontier T" is Elementary_Topology.frontier_Int_closed. tts_lemma frontier_subset_closed: assumes "S ⊆ U" and "closed S" shows "frontier S ⊆ S" is Elementary_Topology.frontier_subset_closed. tts_lemma frontier_subset_eq: assumes "S ⊆ U" shows "(frontier S ⊆ S) = closed S" is Elementary_Topology.frontier_subset_eq. tts_lemma frontier_complement: assumes "S ⊆ U" shows "frontier (- S ∩ U) = frontier S" is Elementary_Topology.frontier_complement. tts_lemma frontier_Un_subset: assumes "S ⊆ U" and "T ⊆ U" shows "frontier (S ∪ T) ⊆ frontier S ∪ frontier T" is Elementary_Topology.frontier_Un_subset. tts_lemma frontier_disjoint_eq: assumes "S ⊆ U" shows "(frontier S ∩ S = {}) = τ S" is Elementary_Topology.frontier_disjoint_eq. tts_lemma frontier_interiors: assumes "s ⊆ U" shows "frontier s = - interior s ∩ U - interior (- s ∩ U)" is Elementary_Topology.frontier_interiors. tts_lemma frontier_interior_subset: assumes "S ⊆ U" shows "frontier (interior S) ⊆ frontier S" is Elementary_Topology.frontier_interior_subset. tts_lemma compact_Un: assumes "s ⊆ U" and "t ⊆ U" and "compact s" and "compact t" shows "compact (s ∪ t)" is Elementary_Topology.compact_Un. tts_lemma closed_Int_compact: assumes "s ⊆ U" and "t ⊆ U" and "closed s" and "compact t" shows "compact (s ∩ t)" is Elementary_Topology.closed_Int_compact. tts_lemma countably_compact_imp_compact: assumes "U ⊆ U" and "B ⊆ Pow U" and "countably_compact U" and "countable B" and "Ball B τ" and "⋀T x. ⟦T ⊆ U; x ∈ U; τ T; x ∈ T; x ∈ U⟧ ⟹ ∃y∈B. x ∈ y ∧ y ∩ U ⊆ T" shows "compact U" is Elementary_Topology.countably_compact_imp_compact. end tts_context tts: (?'a to U) rewriting ctr_simps substituting topological_space_ow_axioms eliminating ‹?U ≠ {}› through (insert closure_eq_empty, blast) begin tts_lemma closure_interior: assumes "S ⊆ U" shows "closure S = - interior (- S ∩ U) ∩ U" is Elementary_Topology.closure_interior. end tts_context tts: (?'a to U) rewriting ctr_simps substituting topological_space_ow_axioms eliminating ‹?U ≠ {}› through (insert compact_empty, fastforce dest: subset_singletonD) begin tts_lemma compact_Union: assumes "S ⊆ Pow U" and "finite S" and "⋀T. ⟦T ⊆ U; T ∈ S⟧ ⟹ compact T" shows "compact (⋃ S)" is Elementary_Topology.compact_Union. end tts_context tts: (?'a to U) rewriting ctr_simps substituting topological_space_ow_axioms eliminating ‹?U ≠ {}› through ( insert interior_empty closure_ow_def closed_UNIV compact_empty compact_ow_def, auto ) begin tts_lemma compactI: assumes "s ⊆ U" and "⋀C. ⟦C ⊆ Pow U; Ball C τ; s ⊆ ⋃ C⟧ ⟹ ∃x⊆Pow U. x ⊆ C ∧ finite x ∧ s ⊆ ⋃ x" shows "compact s" given topological_space_class.compactI by (meson PowI) tts_lemma compactE: assumes "S ⊆ U" and "𝒯 ⊆ Pow U" and "compact S" and "S ⊆ ⋃ 𝒯" and "⋀B. B ∈ 𝒯 ⟹ τ B" and "⋀𝒯'. ⟦𝒯' ⊆ Pow U; 𝒯' ⊆ 𝒯; finite 𝒯'; S ⊆ ⋃ 𝒯'⟧ ⟹ thesis" shows thesis given topological_space_class.compactE by metis tts_lemma compact_fip: assumes "U ⊆ U" shows "compact U = ( ∀x⊆Pow U. Ball x closed ⟶ (∀y⊆Pow U. y ⊆ x ⟶ finite y ⟶ U ∩ (⋂ y ∩ U) ≠ {}) ⟶ U ∩ (⋂ x ∩ U) ≠ {} )" given topological_space_class.compact_fip by auto tts_lemma compact_imp_fip: assumes "S ⊆ U" and "Fa ⊆ Pow U" and "compact S" and "⋀T. ⟦T ⊆ U; T ∈ Fa⟧ ⟹ closed T" and "⋀F'. ⟦F' ⊆ Pow U; finite F'; F' ⊆ Fa⟧ ⟹ S ∩ (⋂ F' ∩ U) ≠ {}" shows "S ∩ (⋂ Fa ∩ U) ≠ {}" is topological_space_class.compact_imp_fip. tts_lemma closed_limpt: assumes "S ⊆ U" shows "closed S = (∀x∈U. x «islimpt» S ⟶ x ∈ S)" is Elementary_Topology.closed_limpt. tts_lemma open_interior: assumes "S ⊆ U" shows "τ (interior S)" is Elementary_Topology.open_interior. tts_lemma interior_subset: assumes "S ⊆ U" shows "interior S ⊆ S" is Elementary_Topology.interior_subset. tts_lemma interior_open: assumes "S ⊆ U" and "τ S" shows "interior S = S" is Elementary_Topology.interior_open. tts_lemma interior_eq: assumes "S ⊆ U" shows "(interior S = S) = τ S" is Elementary_Topology.interior_eq. tts_lemma interior_UNIV: "interior U = U" is Elementary_Topology.interior_UNIV. tts_lemma interior_interior: assumes "S ⊆ U" shows "interior (interior S) = interior S" is Elementary_Topology.interior_interior. tts_lemma interior_closure: assumes "S ⊆ U" shows "interior S = - closure (- S ∩ U) ∩ U" is Elementary_Topology.interior_closure. tts_lemma finite_imp_compact: assumes "s ⊆ U" and "finite s" shows "compact s" is Elementary_Topology.finite_imp_compact. tts_lemma countably_compactE: assumes "s ⊆ U" and "C ⊆ Pow U" and "countably_compact s" and "Ball C τ" and "s ⊆ ⋃ C" and "countable C" and "⋀C'. ⟦C' ⊆ Pow U; C' ⊆ C; finite C'; s ⊆ ⋃ C'⟧ ⟹ thesis" shows thesis is Elementary_Topology.countably_compactE. end tts_context tts: (?'a to U) rewriting ctr_simps substituting topological_space_ow_axioms eliminating ‹?U ≠ {}› and ‹?A ⊆ U› through (insert interior_empty, auto) begin tts_lemma interior_unique: assumes "S ⊆ U" and "T ⊆ S" and "τ T" and "⋀T'. ⟦T' ⊆ S; τ T'⟧ ⟹ T' ⊆ T" shows "interior S = T" given Elementary_Topology.interior_unique by auto end tts_context tts: (?'a to U) and (?'b to ‹U⇩_{2}::'b set›) rewriting ctr_simps substituting topological_space_ow_axioms eliminating ‹?U ≠ {}› through (simp add: subset_iff filterlim_iff) begin tts_lemma open_UN: assumes "A ⊆ U⇩_{2}" and "∀x∈U⇩_{2}. B x ⊆ U" and "∀x∈A. τ (B x)" shows "τ (⋃ (B ` A))" is topological_space_class.open_UN. tts_lemma open_Collect_ex: assumes "⋀i. i ∈ U⇩_{2}⟹ τ {x. P i x ∧ x ∈ U}" shows "τ {x ∈ U. ∃i∈U⇩_{2}. P i x}" is open_Collect_ex. end tts_context tts: (?'a to U) and (?'b to ‹U⇩_{2}::'b set›) rewriting ctr_simps substituting topological_space_ow_axioms eliminating ‹?U ≠ {}› through (unfold closed_ow_def finite_def, auto) begin tts_lemma open_INT: assumes "A ⊆ U⇩_{2}" and "∀x∈U⇩_{2}. B x ⊆ U" and "finite A" and "∀x∈A. τ (B x)" shows "τ (⋂ (B ` A) ∩ U)" is topological_space_class.open_INT. tts_lemma closed_INT: assumes "A ⊆ U⇩_{2}" and "∀x∈U⇩_{2}. B x ⊆ U" and "∀x∈A. closed (B x)" shows "closed (⋂ (B ` A) ∩ U)" is topological_space_class.closed_INT. tts_lemma closed_UN: assumes "A ⊆ U⇩_{2}" and "∀x∈U⇩_{2}. B x ⊆ U" and "finite A" and "∀x∈A. closed (B x)" shows "closed (⋃ (B ` A))" is topological_space_class.closed_UN. end tts_context tts: (?'a to U) and (?'b to ‹U⇩_{2}::'b set›) rewriting ctr_simps substituting topological_space_ow_axioms eliminating ‹?U ≠ {}› through (insert closed_empty, auto) begin tts_lemma closed_Collect_all: assumes "⋀i. i ∈ U⇩_{2}⟹ local.closed {x. P i x ∧ x ∈ U}" shows "local.closed {x ∈ U. ∀i∈U⇩_{2}. P i x}" is topological_space_class.closed_Collect_all. tts_lemma compactE_image: assumes "S ⊆ U" and "C ⊆ U⇩_{2}" and "∀x∈U⇩_{2}. f x ⊆ U" and "compact S" and "⋀T. ⟦T ∈ U⇩_{2}; T ∈ C⟧ ⟹ τ (f T)" and "S ⊆ ⋃ (f ` C)" and "⋀C'. ⟦C' ⊆ U⇩_{2}; C' ⊆ C; finite C'; S ⊆ ⋃ (f ` C')⟧ ⟹ thesis" shows thesis is topological_space_class.compactE_image. end tts_context tts: (?'a to U) and (?'b to ‹U⇩_{2}::'b set›) rewriting ctr_simps substituting topological_space_ow_axioms eliminating ‹?U ≠ {}› through (simp, blast | simp) begin tts_lemma ne_compact_imp_fip_image: assumes "s ⊆ U" and "I ⊆ U⇩_{2}" and "∀x∈U⇩_{2}. f x ⊆ U" and "compact s" and "⋀i. ⟦i ∈ U⇩_{2}; i ∈ I⟧ ⟹ closed (f i)" and "⋀I'. ⟦I' ⊆ U⇩_{2}; finite I'; I' ⊆ I⟧ ⟹ s ∩ (⋂ (f ` I') ∩ U) ≠ {}" shows "s ∩ (⋂ (f ` I) ∩ U) ≠ {}" is topological_space_class.compact_imp_fip_image. end end subsection‹Further results› lemma topological_basis_closed: assumes "topological_basis_ow U τ B" shows "B ⊆ Pow U" using assms unfolding topological_basis_ow_def by auto lemma ts_open_eq_ts_open: assumes "topological_space_ow U τ'" and "⋀s. s ⊆ U ⟹ τ' s = τ s" shows "topological_space_ow U τ" proof from assms(1) have "τ' U" unfolding topological_space_ow_def by simp with assms(2) show "τ U" by auto from assms(1) have "⋀S T. ⟦ S ⊆ U; T ⊆ U; τ' S; τ' T ⟧ ⟹ τ' (S ∩ T)" unfolding topological_space_ow_def by simp with assms(2) show "⋀S T. ⟦ S ⊆ U; T ⊆ U; τ S; τ T ⟧ ⟹ τ (S ∩ T)" by (meson Int_lower1 order_trans) from assms(1) have "⋀K. ⟦ K ⊆ Pow U; ∀S∈K. τ' S ⟧ ⟹ τ' (⋃K)" unfolding topological_space_ow_def by simp with assms(2) show "⋀K. ⟦ K ⊆ Pow U; ∀S∈K. τ S ⟧ ⟹ τ (⋃K)" by (metis Union_Pow_eq Union_mono ctr_simps_subset_pow_iff) qed lemma (in topological_space_ow) topological_basis_closed: assumes "topological_basis_ow U τ B" shows "B ⊆ Pow U" using assms unfolding topological_basis_with_def by (rule topological_basis_closed) text‹\newpage› end