(* Author: L C Paulson, University of Cambridge Author: Amine Chaieb, University of Cambridge Author: Robert Himmelmann, TU Muenchen Author: Brian Huffman, Portland State University *) section ‹Abstract Topology 2› theory Abstract_Topology_2 imports Elementary_Topology Abstract_Topology Continuum_Not_Denumerable "HOL-Library.Indicator_Function" "HOL-Library.Equipollence" begin text ‹Combination of Elementary and Abstract Topology› lemma approachable_lt_le2: "(∃(d::real) > 0. ∀x. Q x ⟶ f x < d ⟶ P x) ⟷ (∃d>0. ∀x. f x ≤ d ⟶ Q x ⟶ P x)" by (meson dense less_eq_real_def order_le_less_trans) lemma triangle_lemma: fixes x y z :: real assumes x: "0 ≤ x" and y: "0 ≤ y" and z: "0 ≤ z" and xy: "x⇧^{2}≤ y⇧^{2}+ z⇧^{2}" shows "x ≤ y + z" proof - have "y⇧^{2}+ z⇧^{2}≤ y⇧^{2}+ 2 * y * z + z⇧^{2}" using z y by simp with xy have th: "x⇧^{2}≤ (y + z)⇧^{2}" by (simp add: power2_eq_square field_simps) from y z have yz: "y + z ≥ 0" by arith from power2_le_imp_le[OF th yz] show ?thesis . qed lemma isCont_indicator: fixes x :: "'a::t2_space" shows "isCont (indicator A :: 'a ⇒ real) x = (x ∉ frontier A)" proof auto fix x assume cts_at: "isCont (indicator A :: 'a ⇒ real) x" and fr: "x ∈ frontier A" with continuous_at_open have 1: "∀V::real set. open V ∧ indicator A x ∈ V ⟶ (∃U::'a set. open U ∧ x ∈ U ∧ (∀y∈U. indicator A y ∈ V))" by auto show False proof (cases "x ∈ A") assume x: "x ∈ A" hence "indicator A x ∈ ({0<..<2} :: real set)" by simp with 1 obtain U where U: "open U" "x ∈ U" "∀y∈U. indicator A y ∈ ({0<..<2} :: real set)" using open_greaterThanLessThan by metis hence "∀y∈U. indicator A y > (0::real)" unfolding greaterThanLessThan_def by auto hence "U ⊆ A" using indicator_eq_0_iff by force hence "x ∈ interior A" using U interiorI by auto thus ?thesis using fr unfolding frontier_def by simp next assume x: "x ∉ A" hence "indicator A x ∈ ({-1<..<1} :: real set)" by simp with 1 obtain U where U: "open U" "x ∈ U" "∀y∈U. indicator A y ∈ ({-1<..<1} :: real set)" using 1 open_greaterThanLessThan by metis hence "∀y∈U. indicator A y < (1::real)" unfolding greaterThanLessThan_def by auto hence "U ⊆ -A" by auto hence "x ∈ interior (-A)" using U interiorI by auto thus ?thesis using fr interior_complement unfolding frontier_def by auto qed next assume nfr: "x ∉ frontier A" hence "x ∈ interior A ∨ x ∈ interior (-A)" by (auto simp: frontier_def closure_interior) thus "isCont ((indicator A)::'a ⇒ real) x" proof assume int: "x ∈ interior A" then obtain U where U: "open U" "x ∈ U" "U ⊆ A" unfolding interior_def by auto hence "∀y∈U. indicator A y = (1::real)" unfolding indicator_def by auto hence "continuous_on U (indicator A)" by (simp add: indicator_eq_1_iff) thus ?thesis using U continuous_on_eq_continuous_at by auto next assume ext: "x ∈ interior (-A)" then obtain U where U: "open U" "x ∈ U" "U ⊆ -A" unfolding interior_def by auto then have "continuous_on U (indicator A)" using continuous_on_topological by (auto simp: subset_iff) thus ?thesis using U continuous_on_eq_continuous_at by auto qed qed lemma islimpt_closure: "⟦S ⊆ T; ⋀x. ⟦x islimpt S; x ∈ T⟧ ⟹ x ∈ S⟧ ⟹ S = T ∩ closure S" using closure_def by fastforce lemma closedin_limpt: "closedin (top_of_set T) S ⟷ S ⊆ T ∧ (∀x. x islimpt S ∧ x ∈ T ⟶ x ∈ S)" proof - have "⋀U x. ⟦closed U; S = T ∩ U; x islimpt S; x ∈ T⟧ ⟹ x ∈ S" by (meson IntI closed_limpt inf_le2 islimpt_subset) then show ?thesis by (metis closed_closure closedin_closed closedin_imp_subset islimpt_closure) qed lemma closedin_closed_eq: "closed S ⟹ closedin (top_of_set S) T ⟷ closed T ∧ T ⊆ S" by (meson closedin_limpt closed_subset closedin_closed_trans) lemma connected_closed_set: "closed S ⟹ connected S ⟷ (∄A B. closed A ∧ closed B ∧ A ≠ {} ∧ B ≠ {} ∧ A ∪ B = S ∧ A ∩ B = {})" unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast text ‹If a connnected set is written as the union of two nonempty closed sets, then these sets have to intersect.› lemma connected_as_closed_union: assumes "connected C" "C = A ∪ B" "closed A" "closed B" "A ≠ {}" "B ≠ {}" shows "A ∩ B ≠ {}" by (metis assms closed_Un connected_closed_set) lemma closedin_subset_trans: "closedin (top_of_set U) S ⟹ S ⊆ T ⟹ T ⊆ U ⟹ closedin (top_of_set T) S" by (meson closedin_limpt subset_iff) lemma openin_subset_trans: "openin (top_of_set U) S ⟹ S ⊆ T ⟹ T ⊆ U ⟹ openin (top_of_set T) S" by (auto simp: openin_open) lemma closedin_compact: "⟦compact S; closedin (top_of_set S) T⟧ ⟹ compact T" by (metis closedin_closed compact_Int_closed) lemma closedin_compact_eq: fixes S :: "'a::t2_space set" shows "compact S ⟹ (closedin (top_of_set S) T ⟷ compact T ∧ T ⊆ S)" by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed) subsection ‹Closure› lemma euclidean_closure_of [simp]: "euclidean closure_of S = closure S" by (auto simp: closure_of_def closure_def islimpt_def) lemma closure_openin_Int_closure: assumes ope: "openin (top_of_set U) S" and "T ⊆ U" shows "closure(S ∩ closure T) = closure(S ∩ T)" proof obtain V where "open V" and S: "S = U ∩ V" using ope using openin_open by metis show "closure (S ∩ closure T) ⊆ closure (S ∩ T)" proof (clarsimp simp: S) fix x assume "x ∈ closure (U ∩ V ∩ closure T)" then have "V ∩ closure T ⊆ A ⟹ x ∈ closure A" for A by (metis closure_mono subsetD inf.coboundedI2 inf_assoc) then have "x ∈ closure (T ∩ V)" by (metis ‹open V› closure_closure inf_commute open_Int_closure_subset) then show "x ∈ closure (U ∩ V ∩ T)" by (metis ‹T ⊆ U› inf.absorb_iff2 inf_assoc inf_commute) qed next show "closure (S ∩ T) ⊆ closure (S ∩ closure T)" by (meson Int_mono closure_mono closure_subset order_refl) qed corollary infinite_openin: fixes S :: "'a :: t1_space set" shows "⟦openin (top_of_set U) S; x ∈ S; x islimpt U⟧ ⟹ infinite S" by (clarsimp simp add: openin_open islimpt_eq_acc_point inf_commute) lemma closure_Int_ballI: assumes "⋀U. ⟦openin (top_of_set S) U; U ≠ {}⟧ ⟹ T ∩ U ≠ {}" shows "S ⊆ closure T" proof (clarsimp simp: closure_iff_nhds_not_empty) fix x and A and V assume "x ∈ S" "V ⊆ A" "open V" "x ∈ V" "T ∩ A = {}" then have "openin (top_of_set S) (A ∩ V ∩ S)" by (simp add: inf_absorb2 openin_subtopology_Int) moreover have "A ∩ V ∩ S ≠ {}" using ‹x ∈ V› ‹V ⊆ A› ‹x ∈ S› by auto ultimately show False using ‹T ∩ A = {}› assms by fastforce qed subsection ‹Frontier› lemma euclidean_interior_of [simp]: "euclidean interior_of S = interior S" by (auto simp: interior_of_def interior_def) lemma euclidean_frontier_of [simp]: "euclidean frontier_of S = frontier S" by (auto simp: frontier_of_def frontier_def) lemma connected_Int_frontier: "⟦connected S; S ∩ T ≠ {}; S - T ≠ {}⟧ ⟹ S ∩ frontier T ≠ {}" apply (simp add: frontier_interiors connected_openin, safe) apply (drule_tac x="S ∩ interior T" in spec, safe) apply (drule_tac [2] x="S ∩ interior (-T)" in spec) apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD]) done subsection ‹Compactness› lemma openin_delete: fixes a :: "'a :: t1_space" shows "openin (top_of_set u) S ⟹ openin (top_of_set u) (S - {a})" by (metis Int_Diff open_delete openin_open) lemma compact_eq_openin_cover: "compact S ⟷ (∀C. (∀c∈C. openin (top_of_set S) c) ∧ S ⊆ ⋃C ⟶ (∃D⊆C. finite D ∧ S ⊆ ⋃D))" proof safe fix C assume "compact S" and "∀c∈C. openin (top_of_set S) c" and "S ⊆ ⋃C" then have "∀c∈{T. open T ∧ S ∩ T ∈ C}. open c" and "S ⊆ ⋃{T. open T ∧ S ∩ T ∈ C}" unfolding openin_open by force+ with ‹compact S› obtain D where "D ⊆ {T. open T ∧ S ∩ T ∈ C}" and "finite D" and "S ⊆ ⋃D" by (meson compactE) then have "image (λT. S ∩ T) D ⊆ C ∧ finite (image (λT. S ∩ T) D) ∧ S ⊆ ⋃(image (λT. S ∩ T) D)" by auto then show "∃D⊆C. finite D ∧ S ⊆ ⋃D" .. next assume 1: "∀C. (∀c∈C. openin (top_of_set S) c) ∧ S ⊆ ⋃C ⟶ (∃D⊆C. finite D ∧ S ⊆ ⋃D)" show "compact S" proof (rule compactI) fix C let ?C = "image (λT. S ∩ T) C" assume "∀t∈C. open t" and "S ⊆ ⋃C" then have "(∀c∈?C. openin (top_of_set S) c) ∧ S ⊆ ⋃?C" unfolding openin_open by auto with 1 obtain D where "D ⊆ ?C" and "finite D" and "S ⊆ ⋃D" by metis let ?D = "inv_into C (λT. S ∩ T) ` D" have "?D ⊆ C ∧ finite ?D ∧ S ⊆ ⋃?D" proof (intro conjI) from ‹D ⊆ ?C› show "?D ⊆ C" by (fast intro: inv_into_into) from ‹finite D› show "finite ?D" by (rule finite_imageI) from ‹S ⊆ ⋃D› show "S ⊆ ⋃?D" by (metis ‹D ⊆ (∩) S ` C› image_inv_into_cancel inf_Sup le_infE) qed then show "∃D⊆C. finite D ∧ S ⊆ ⋃D" .. qed qed subsection ‹Continuity› lemma interior_image_subset: assumes "inj f" "⋀x. continuous (at x) f" shows "interior (f ` S) ⊆ f ` (interior S)" proof fix x assume "x ∈ interior (f ` S)" then obtain T where as: "open T" "x ∈ T" "T ⊆ f ` S" .. then have "x ∈ f ` S" by auto then obtain y where y: "y ∈ S" "x = f y" by auto have "open (f -` T)" using assms ‹open T› by (simp add: continuous_at_imp_continuous_on open_vimage) moreover have "y ∈ vimage f T" using ‹x = f y› ‹x ∈ T› by simp moreover have "vimage f T ⊆ S" using ‹T ⊆ image f S› ‹inj f› unfolding inj_on_def subset_eq by auto ultimately have "y ∈ interior S" .. with ‹x = f y› show "x ∈ f ` interior S" .. qed subsection✐‹tag unimportant› ‹Equality of continuous functions on closure and related results› lemma continuous_closedin_preimage_constant: fixes f :: "_ ⇒ 'b::t1_space" shows "continuous_on S f ⟹ closedin (top_of_set S) {x ∈ S. f x = a}" using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq) lemma continuous_closed_preimage_constant: fixes f :: "_ ⇒ 'b::t1_space" shows "continuous_on S f ⟹ closed S ⟹ closed {x ∈ S. f x = a}" using continuous_closed_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq) lemma continuous_constant_on_closure: fixes f :: "_ ⇒ 'b::t1_space" assumes "continuous_on (closure S) f" and "⋀x. x ∈ S ⟹ f x = a" and "x ∈ closure S" shows "f x = a" using continuous_closed_preimage_constant[of "closure S" f a] assms closure_minimal[of S "{x ∈ closure S. f x = a}"] closure_subset unfolding subset_eq by auto lemma image_closure_subset: assumes contf: "continuous_on (closure S) f" and "closed T" and "(f ` S) ⊆ T" shows "f ` (closure S) ⊆ T" proof - have "S ⊆ {x ∈ closure S. f x ∈ T}" using assms(3) closure_subset by auto moreover have "closed (closure S ∩ f -` T)" using continuous_closed_preimage[OF contf] ‹closed T› by auto ultimately have "closure S = (closure S ∩ f -` T)" using closure_minimal[of S "(closure S ∩ f -` T)"] by auto then show ?thesis by auto qed subsection✐‹tag unimportant› ‹A function constant on a set› definition constant_on (infixl "(constant'_on)" 50) where "f constant_on A ≡ ∃y. ∀x∈A. f x = y" lemma constant_on_subset: "⟦f constant_on A; B ⊆ A⟧ ⟹ f constant_on B" unfolding constant_on_def by blast lemma injective_not_constant: fixes S :: "'a::{perfect_space} set" shows "⟦open S; inj_on f S; f constant_on S⟧ ⟹ S = {}" unfolding constant_on_def by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def) lemma constant_on_compose: assumes "f constant_on A" shows "g ∘ f constant_on A" using assms by (auto simp: constant_on_def) lemma not_constant_onI: "f x ≠ f y ⟹ x ∈ A ⟹ y ∈ A ⟹ ¬f constant_on A" unfolding constant_on_def by metis lemma constant_onE: assumes "f constant_on S" and "⋀x. x∈S ⟹ f x = g x" shows "g constant_on S" using assms unfolding constant_on_def by simp lemma constant_on_closureI: fixes f :: "_ ⇒ 'b::t1_space" assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f" shows "f constant_on (closure S)" using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def by metis subsection✐‹tag unimportant› ‹Continuity relative to a union.› lemma continuous_on_Un_local: "⟦closedin (top_of_set (S ∪ T)) S; closedin (top_of_set (S ∪ T)) T; continuous_on S f; continuous_on T f⟧ ⟹ continuous_on (S ∪ T) f" unfolding continuous_on closedin_limpt by (metis Lim_trivial_limit Lim_within_Un Un_iff trivial_limit_within) lemma continuous_on_cases_local: "⟦closedin (top_of_set (S ∪ T)) S; closedin (top_of_set (S ∪ T)) T; continuous_on S f; continuous_on T g; ⋀x. ⟦x ∈ S ∧ ¬P x ∨ x ∈ T ∧ P x⟧ ⟹ f x = g x⟧ ⟹ continuous_on (S ∪ T) (λx. if P x then f x else g x)" by (rule continuous_on_Un_local) (auto intro: continuous_on_eq) lemma continuous_on_cases_le: fixes h :: "'a :: topological_space ⇒ real" assumes "continuous_on {x ∈ S. h x ≤ a} f" and "continuous_on {x ∈ S. a ≤ h x} g" and h: "continuous_on S h" and "⋀x. ⟦x ∈ S; h x = a⟧ ⟹ f x = g x" shows "continuous_on S (λx. if h x ≤ a then f(x) else g(x))" proof - have S: "S = (S ∩ h -` atMost a) ∪ (S ∩ h -` atLeast a)" by force have 1: "closedin (top_of_set S) (S ∩ h -` atMost a)" by (rule continuous_closedin_preimage [OF h closed_atMost]) have 2: "closedin (top_of_set S) (S ∩ h -` atLeast a)" by (rule continuous_closedin_preimage [OF h closed_atLeast]) have [simp]: "S ∩ h -` {..a} = {x ∈ S. h x ≤ a}" "S ∩ h -` {a..} = {x ∈ S. a ≤ h x}" by auto have "continuous_on (S ∩ h -` {..a} ∪ S ∩ h -` {a..}) (λx. if h x ≤ a then f x else g x)" by (intro continuous_on_cases_local) (use 1 2 S assms in auto) then show ?thesis using S by force qed lemma continuous_on_cases_1: fixes S :: "real set" assumes "continuous_on {t ∈ S. t ≤ a} f" and "continuous_on {t ∈ S. a ≤ t} g" and "a ∈ S ⟹ f a = g a" shows "continuous_on S (λt. if t ≤ a then f(t) else g(t))" using assms by (auto intro: continuous_on_cases_le [where h = id, simplified]) subsection✐‹tag unimportant›‹Inverse function property for open/closed maps› lemma continuous_on_inverse_open_map: assumes contf: "continuous_on S f" and imf: "f ` S = T" and injf: "⋀x. x ∈ S ⟹ g (f x) = x" and oo: "⋀U. openin (top_of_set S) U ⟹ openin (top_of_set T) (f ` U)" shows "continuous_on T g" proof - from imf injf have gTS: "g ` T = S" by force from imf injf have fU: "U ⊆ S ⟹ (f ` U) = T ∩ g -` U" for U by force show ?thesis by (simp add: continuous_on_open [of T g] gTS) (metis openin_imp_subset fU oo) qed lemma continuous_on_inverse_closed_map: assumes contf: "continuous_on S f" and imf: "f ` S = T" and injf: "⋀x. x ∈ S ⟹ g(f x) = x" and oo: "⋀U. closedin (top_of_set S) U ⟹ closedin (top_of_set T) (f ` U)" shows "continuous_on T g" proof - from imf injf have gTS: "g ` T = S" by force from imf injf have fU: "U ⊆ S ⟹ (f ` U) = T ∩ g -` U" for U by force show ?thesis by (simp add: continuous_on_closed [of T g] gTS) (metis closedin_imp_subset fU oo) qed lemma homeomorphism_injective_open_map: assumes contf: "continuous_on S f" and imf: "f ` S = T" and injf: "inj_on f S" and oo: "⋀U. openin (top_of_set S) U ⟹ openin (top_of_set T) (f ` U)" obtains g where "homeomorphism S T f g" proof have "continuous_on T (inv_into S f)" by (metis contf continuous_on_inverse_open_map imf injf inv_into_f_f oo) with imf injf contf show "homeomorphism S T f (inv_into S f)" by (auto simp: homeomorphism_def) qed lemma homeomorphism_injective_closed_map: assumes contf: "continuous_on S f" and imf: "f ` S = T" and injf: "inj_on f S" and oo: "⋀U. closedin (top_of_set S) U ⟹ closedin (top_of_set T) (f ` U)" obtains g where "homeomorphism S T f g" proof have "continuous_on T (inv_into S f)" by (metis contf continuous_on_inverse_closed_map imf injf inv_into_f_f oo) with imf injf contf show "homeomorphism S T f (inv_into S f)" by (auto simp: homeomorphism_def) qed lemma homeomorphism_imp_open_map: assumes hom: "homeomorphism S T f g" and oo: "openin (top_of_set S) U" shows "openin (top_of_set T) (f ` U)" proof - from hom oo have [simp]: "f ` U = T ∩ g -` U" using openin_subset by (fastforce simp: homeomorphism_def rev_image_eqI) from hom have "continuous_on T g" unfolding homeomorphism_def by blast moreover have "g ` T = S" by (metis hom homeomorphism_def) ultimately show ?thesis by (simp add: continuous_on_open oo) qed lemma homeomorphism_imp_closed_map: assumes hom: "homeomorphism S T f g" and oo: "closedin (top_of_set S) U" shows "closedin (top_of_set T) (f ` U)" proof - from hom oo have [simp]: "f ` U = T ∩ g -` U" using closedin_subset by (fastforce simp: homeomorphism_def rev_image_eqI) from hom have "continuous_on T g" unfolding homeomorphism_def by blast moreover have "g ` T = S" by (metis hom homeomorphism_def) ultimately show ?thesis by (simp add: continuous_on_closed oo) qed subsection✐‹tag unimportant› ‹Seperability› lemma subset_second_countable: obtains ℬ :: "'a:: second_countable_topology set set" where "countable ℬ" "{} ∉ ℬ" "⋀C. C ∈ ℬ ⟹ openin(top_of_set S) C" "⋀T. openin(top_of_set S) T ⟹ ∃𝒰. 𝒰 ⊆ ℬ ∧ T = ⋃𝒰" proof - obtain ℬ :: "'a set set" where "countable ℬ" and opeB: "⋀C. C ∈ ℬ ⟹ openin(top_of_set S) C" and ℬ: "⋀T. openin(top_of_set S) T ⟹ ∃𝒰. 𝒰 ⊆ ℬ ∧ T = ⋃𝒰" proof - obtain 𝒞 :: "'a set set" where "countable 𝒞" and ope: "⋀C. C ∈ 𝒞 ⟹ open C" and 𝒞: "⋀S. open S ⟹ ∃U. U ⊆ 𝒞 ∧ S = ⋃U" by (metis univ_second_countable that) show ?thesis proof show "countable ((λC. S ∩ C) ` 𝒞)" by (simp add: ‹countable 𝒞›) show "⋀C. C ∈ (∩) S ` 𝒞 ⟹ openin (top_of_set S) C" using ope by auto show "⋀T. openin (top_of_set S) T ⟹ ∃𝒰⊆(∩) S ` 𝒞. T = ⋃𝒰" by (metis 𝒞 image_mono inf_Sup openin_open) qed qed show ?thesis proof show "countable (ℬ - {{}})" using ‹countable ℬ› by blast show "⋀C. ⟦C ∈ ℬ - {{}}⟧ ⟹ openin (top_of_set S) C" by (simp add: ‹⋀C. C ∈ ℬ ⟹ openin (top_of_set S) C›) show "∃𝒰⊆ℬ - {{}}. T = ⋃𝒰" if "openin (top_of_set S) T" for T using ℬ [OF that] apply clarify by (rule_tac x="𝒰 - {{}}" in exI, auto) qed auto qed lemma Lindelof_openin: fixes ℱ :: "'a::second_countable_topology set set" assumes "⋀S. S ∈ ℱ ⟹ openin (top_of_set U) S" obtains ℱ' where "ℱ' ⊆ ℱ" "countable ℱ'" "⋃ℱ' = ⋃ℱ" proof - have "⋀S. S ∈ ℱ ⟹ ∃T. open T ∧ S = U ∩ T" using assms by (simp add: openin_open) then obtain tf where tf: "⋀S. S ∈ ℱ ⟹ open (tf S) ∧ (S = U ∩ tf S)" by metis have [simp]: "⋀ℱ'. ℱ' ⊆ ℱ ⟹ ⋃ℱ' = U ∩ ⋃(tf ` ℱ')" using tf by fastforce obtain 𝒢 where "countable 𝒢 ∧ 𝒢 ⊆ tf ` ℱ" "⋃𝒢 = ⋃(tf ` ℱ)" using tf by (force intro: Lindelof [of "tf ` ℱ"]) then obtain ℱ' where ℱ': "ℱ' ⊆ ℱ" "countable ℱ'" "⋃ℱ' = ⋃ℱ" by (clarsimp simp add: countable_subset_image) then show ?thesis .. qed subsection✐‹tag unimportant›‹Closed Maps› lemma continuous_imp_closed_map: fixes f :: "'a::t2_space ⇒ 'b::t2_space" assumes "closedin (top_of_set S) U" "continuous_on S f" "f ` S = T" "compact S" shows "closedin (top_of_set T) (f ` U)" by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff) lemma closed_map_restrict: assumes cloU: "closedin (top_of_set (S ∩ f -` T')) U" and cc: "⋀U. closedin (top_of_set S) U ⟹ closedin (top_of_set T) (f ` U)" and "T' ⊆ T" shows "closedin (top_of_set T') (f ` U)" proof - obtain V where "closed V" "U = S ∩ f -` T' ∩ V" using cloU by (auto simp: closedin_closed) with cc [of "S ∩ V"] ‹T' ⊆ T› show ?thesis by (fastforce simp add: closedin_closed) qed subsection✐‹tag unimportant›‹Open Maps› lemma open_map_restrict: assumes opeU: "openin (top_of_set (S ∩ f -` T')) U" and oo: "⋀U. openin (top_of_set S) U ⟹ openin (top_of_set T) (f ` U)" and "T' ⊆ T" shows "openin (top_of_set T') (f ` U)" proof - obtain V where "open V" "U = S ∩ f -` T' ∩ V" using opeU by (auto simp: openin_open) with oo [of "S ∩ V"] ‹T' ⊆ T› show ?thesis by (fastforce simp add: openin_open) qed subsection✐‹tag unimportant›‹Quotient maps› lemma quotient_map_imp_continuous_open: assumes T: "f ∈ S → T" and ope: "⋀U. U ⊆ T ⟹ (openin (top_of_set S) (S ∩ f -` U) ⟷ openin (top_of_set T) U)" shows "continuous_on S f" proof - have [simp]: "S ∩ f -` f ` S = S" by auto show ?thesis by (meson T continuous_on_open_gen ope openin_imp_subset) qed lemma quotient_map_imp_continuous_closed: assumes T: "f ∈ S → T" and ope: "⋀U. U ⊆ T ⟹ (closedin (top_of_set S) (S ∩ f -` U) ⟷ closedin (top_of_set T) U)" shows "continuous_on S f" proof - have [simp]: "S ∩ f -` f ` S = S" by auto show ?thesis by (meson T closedin_imp_subset continuous_on_closed_gen ope) qed lemma open_map_imp_quotient_map: assumes contf: "continuous_on S f" and T: "T ⊆ f ` S" and ope: "⋀T. openin (top_of_set S) T ⟹ openin (top_of_set (f ` S)) (f ` T)" shows "openin (top_of_set S) (S ∩ f -` T) = openin (top_of_set (f ` S)) T" proof - have "T = f ` (S ∩ f -` T)" using T by blast then show ?thesis using "ope" contf continuous_on_open by metis qed lemma closed_map_imp_quotient_map: assumes contf: "continuous_on S f" and T: "T ⊆ f ` S" and ope: "⋀T. closedin (top_of_set S) T ⟹ closedin (top_of_set (f ` S)) (f ` T)" shows "openin (top_of_set S) (S ∩ f -` T) ⟷ openin (top_of_set (f ` S)) T" (is "?lhs = ?rhs") proof assume ?lhs then have *: "closedin (top_of_set S) (S - (S ∩ f -` T))" using closedin_diff by fastforce have [simp]: "(f ` S - f ` (S - (S ∩ f -` T))) = T" using T by blast show ?rhs using ope [OF *, unfolded closedin_def] by auto next assume ?rhs with contf show ?lhs by (auto simp: continuous_on_open) qed lemma continuous_right_inverse_imp_quotient_map: assumes contf: "continuous_on S f" and imf: "f ∈ S → T" and contg: "continuous_on T g" and img: "g ∈ T → S" and fg [simp]: "⋀y. y ∈ T ⟹ f(g y) = y" and U: "U ⊆ T" shows "openin (top_of_set S) (S ∩ f -` U) ⟷ openin (top_of_set T) U" (is "?lhs = ?rhs") proof - have f: "⋀Z. openin (top_of_set (f ` S)) Z ⟹ openin (top_of_set S) (S ∩ f -` Z)" and g: "⋀Z. openin (top_of_set (g ` T)) Z ⟹ openin (top_of_set T) (T ∩ g -` Z)" using contf contg by (auto simp: continuous_on_open) show ?thesis proof have "T ∩ g -` (g ` T ∩ (S ∩ f -` U)) = {x ∈ T. f (g x) ∈ U}" using imf img by blast also have "... = U" using U by auto finally have eq: "T ∩ g -` (g ` T ∩ (S ∩ f -` U)) = U" . assume ?lhs then have *: "openin (top_of_set (g ` T)) (g ` T ∩ (S ∩ f -` U))" by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self image_subset_iff_funcset) show ?rhs using g [OF *] eq by auto next assume rhs: ?rhs show ?lhs using assms continuous_openin_preimage rhs by blast qed qed lemma continuous_left_inverse_imp_quotient_map: assumes "continuous_on S f" and "continuous_on (f ` S) g" and "⋀x. x ∈ S ⟹ g(f x) = x" and "U ⊆ f ` S" shows "openin (top_of_set S) (S ∩ f -` U) ⟷ openin (top_of_set (f ` S)) U" using assms by (intro continuous_right_inverse_imp_quotient_map) auto lemma continuous_imp_quotient_map: fixes f :: "'a::t2_space ⇒ 'b::t2_space" assumes "continuous_on S f" "f ` S = T" "compact S" "U ⊆ T" shows "openin (top_of_set S) (S ∩ f -` U) ⟷ openin (top_of_set T) U" by (simp add: assms closed_map_imp_quotient_map continuous_imp_closed_map) subsection✐‹tag unimportant›‹Pasting lemmas for functions, for of casewise definitions› subsubsection‹on open sets› lemma pasting_lemma: assumes ope: "⋀i. i ∈ I ⟹ openin X (T i)" and cont: "⋀i. i ∈ I ⟹ continuous_map(subtopology X (T i)) Y (f i)" and f: "⋀i j x. ⟦i ∈ I; j ∈ I; x ∈ topspace X ∩ T i ∩ T j⟧ ⟹ f i x = f j x" and g: "⋀x. x ∈ topspace X ⟹ ∃j. j ∈ I ∧ x ∈ T j ∧ g x = f j x" shows "continuous_map X Y g" unfolding continuous_map_openin_preimage_eq proof (intro conjI allI impI) show "g ∈ topspace X → topspace Y" using g cont continuous_map_image_subset_topspace by fastforce next fix U assume Y: "openin Y U" have T: "T i ⊆ topspace X" if "i ∈ I" for i using ope by (simp add: openin_subset that) have *: "topspace X ∩ g -` U = (⋃i ∈ I. T i ∩ f i -` U)" using f g T by fastforce have "⋀i. i ∈ I ⟹ openin X (T i ∩ f i -` U)" using cont unfolding continuous_map_openin_preimage_eq by (metis Y T inf.commute inf_absorb1 ope topspace_subtopology openin_trans_full) then show "openin X (topspace X ∩ g -` U)" by (auto simp: *) qed lemma pasting_lemma_exists: assumes X: "topspace X ⊆ (⋃i ∈ I. T i)" and ope: "⋀i. i ∈ I ⟹ openin X (T i)" and cont: "⋀i. i ∈ I ⟹ continuous_map (subtopology X (T i)) Y (f i)" and f: "⋀i j x. ⟦i ∈ I; j ∈ I; x ∈ topspace X ∩ T i ∩ T j⟧ ⟹ f i x = f j x" obtains g where "continuous_map X Y g" "⋀x i. ⟦i ∈ I; x ∈ topspace X ∩ T i⟧ ⟹ g x = f i x" proof let ?h = "λx. f (SOME i. i ∈ I ∧ x ∈ T i) x" show "continuous_map X Y ?h" apply (rule pasting_lemma [OF ope cont]) apply (blast intro: f)+ by (metis (no_types, lifting) UN_E X subsetD someI_ex) show "f (SOME i. i ∈ I ∧ x ∈ T i) x = f i x" if "i ∈ I" "x ∈ topspace X ∩ T i" for i x by (metis (no_types, lifting) IntD2 IntI f someI_ex that) qed lemma pasting_lemma_locally_finite: assumes fin: "⋀x. x ∈ topspace X ⟹ ∃V. openin X V ∧ x ∈ V ∧ finite {i ∈ I. T i ∩ V ≠ {}}" and clo: "⋀i. i ∈ I ⟹ closedin X (T i)" and cont: "⋀i. i ∈ I ⟹ continuous_map(subtopology X (T i)) Y (f i)" and f: "⋀i j x. ⟦i ∈ I; j ∈ I; x ∈ topspace X ∩ T i ∩ T j⟧ ⟹ f i x = f j x" and g: "⋀x. x ∈ topspace X ⟹ ∃j. j ∈ I ∧ x ∈ T j ∧ g x = f j x" shows "continuous_map X Y g" unfolding continuous_map_closedin_preimage_eq proof (intro conjI allI impI) show "g ∈ topspace X → topspace Y" using g cont continuous_map_image_subset_topspace by fastforce next fix U assume Y: "closedin Y U" have T: "T i ⊆ topspace X" if "i ∈ I" for i using clo by (simp add: closedin_subset that) have *: "topspace X ∩ g -` U = (⋃i ∈ I. T i ∩ f i -` U)" using f g T by fastforce have cTf: "⋀i. i ∈ I ⟹ closedin X (T i ∩ f i -` U)" using cont unfolding continuous_map_closedin_preimage_eq topspace_subtopology by (simp add: Int_absorb1 T Y clo closedin_closed_subtopology) have sub: "{Z ∈ (λi. T i ∩ f i -` U) ` I. Z ∩ V ≠ {}} ⊆ (λi. T i ∩ f i -` U) ` {i ∈ I. T i ∩ V ≠ {}}" for V by auto have 1: "(⋃i∈I. T i ∩ f i -` U) ⊆ topspace X" using T by blast then have "locally_finite_in X ((λi. T i ∩ f i -` U) ` I)" unfolding locally_finite_in_def using finite_subset [OF sub] fin by force then show "closedin X (topspace X ∩ g -` U)" by (smt (verit, best) * cTf closedin_locally_finite_Union image_iff) qed subsubsection‹Likewise on closed sets, with a finiteness assumption› lemma pasting_lemma_closed: assumes fin: "finite I" and clo: "⋀i. i ∈ I ⟹ closedin X (T i)" and cont: "⋀i. i ∈ I ⟹ continuous_map(subtopology X (T i)) Y (f i)" and f: "⋀i j x. ⟦i ∈ I; j ∈ I; x ∈ topspace X ∩ T i ∩ T j⟧ ⟹ f i x = f j x" and g: "⋀x. x ∈ topspace X ⟹ ∃j. j ∈ I ∧ x ∈ T j ∧ g x = f j x" shows "continuous_map X Y g" using pasting_lemma_locally_finite [OF _ clo cont f g] fin by auto lemma pasting_lemma_exists_locally_finite: assumes fin: "⋀x. x ∈ topspace X ⟹ ∃V. openin X V ∧ x ∈ V ∧ finite {i ∈ I. T i ∩ V ≠ {}}" and X: "topspace X ⊆ ⋃(T ` I)" and clo: "⋀i. i ∈ I ⟹ closedin X (T i)" and cont: "⋀i. i ∈ I ⟹ continuous_map(subtopology X (T i)) Y (f i)" and f: "⋀i j x. ⟦i ∈ I; j ∈ I; x ∈ topspace X ∩ T i ∩ T j⟧ ⟹ f i x = f j x" and g: "⋀x. x ∈ topspace X ⟹ ∃j. j ∈ I ∧ x ∈ T j ∧ g x = f j x" obtains g where "continuous_map X Y g" "⋀x i. ⟦i ∈ I; x ∈ topspace X ∩ T i⟧ ⟹ g x = f i x" proof show "continuous_map X Y (λx. f(@i. i ∈ I ∧ x ∈ T i) x)" apply (rule pasting_lemma_locally_finite [OF fin]) apply (blast intro: assms)+ by (metis (no_types, lifting) UN_E X set_rev_mp someI_ex) next fix x i assume "i ∈ I" and "x ∈ topspace X ∩ T i" then show "f (SOME i. i ∈ I ∧ x ∈ T i) x = f i x" by (metis (mono_tags, lifting) IntE IntI f someI2) qed lemma pasting_lemma_exists_closed: assumes fin: "finite I" and X: "topspace X ⊆ ⋃(T ` I)" and clo: "⋀i. i ∈ I ⟹ closedin X (T i)" and cont: "⋀i. i ∈ I ⟹ continuous_map(subtopology X (T i)) Y (f i)" and f: "⋀i j x. ⟦i ∈ I; j ∈ I; x ∈ topspace X ∩ T i ∩ T j⟧ ⟹ f i x = f j x" obtains g where "continuous_map X Y g" "⋀x i. ⟦i ∈ I; x ∈ topspace X ∩ T i⟧ ⟹ g x = f i x" proof show "continuous_map X Y (λx. f (SOME i. i ∈ I ∧ x ∈ T i) x)" apply (rule pasting_lemma_closed [OF ‹finite I› clo cont]) apply (blast intro: f)+ by (metis (mono_tags, lifting) UN_iff X someI_ex subset_iff) next fix x i assume "i ∈ I" "x ∈ topspace X ∩ T i" then show "f (SOME i. i ∈ I ∧ x ∈ T i) x = f i x" by (metis (no_types, lifting) IntD2 IntI f someI_ex) qed lemma continuous_map_cases: assumes f: "continuous_map (subtopology X (X closure_of {x. P x})) Y f" and g: "continuous_map (subtopology X (X closure_of {x. ¬ P x})) Y g" and fg: "⋀x. x ∈ X frontier_of {x. P x} ⟹ f x = g x" shows "continuous_map X Y (λx. if P x then f x else g x)" proof (rule pasting_lemma_closed) let ?f = "λb. if b then f else g" let ?g = "λx. if P x then f x else g x" let ?T = "λb. if b then X closure_of {x. P x} else X closure_of {x. ~P x}" show "finite {True,False}" by auto have eq: "topspace X - Collect P = topspace X ∩ {x. ¬ P x}" by blast show "?f i x = ?f j x" if "i ∈ {True,False}" "j ∈ {True,False}" and x: "x ∈ topspace X ∩ ?T i ∩ ?T j" for i j x proof - have "f x = g x" if "i" "¬ j" by (smt (verit, best) Diff_Diff_Int closure_of_interior_of closure_of_restrict eq fg frontier_of_closures interior_of_complement that x) moreover have "g x = f x" if "x ∈ X closure_of {x. ¬ P x}" "x ∈ X closure_of Collect P" "¬ i" "j" for x by (metis IntI closure_of_restrict eq fg frontier_of_closures that) ultimately show ?thesis using that by (auto simp flip: closure_of_restrict) qed show "∃j. j ∈ {True,False} ∧ x ∈ ?T j ∧ (if P x then f x else g x) = ?f j x" if "x ∈ topspace X" for x by simp (metis in_closure_of mem_Collect_eq that) qed (auto simp: f g) lemma continuous_map_cases_alt: assumes f: "continuous_map (subtopology X (X closure_of {x ∈ topspace X. P x})) Y f" and g: "continuous_map (subtopology X (X closure_of {x ∈ topspace X. ~P x})) Y g" and fg: "⋀x. x ∈ X frontier_of {x ∈ topspace X. P x} ⟹ f x = g x" shows "continuous_map X Y (λx. if P x then f x else g x)" apply (rule continuous_map_cases) using assms apply (simp_all add: Collect_conj_eq closure_of_restrict [symmetric] frontier_of_restrict [symmetric]) done lemma continuous_map_cases_function: assumes contp: "continuous_map X Z p" and contf: "continuous_map (subtopology X {x ∈ topspace X. p x ∈ Z closure_of U}) Y f" and contg: "continuous_map (subtopology X {x ∈ topspace X. p x ∈ Z closure_of (topspace Z - U)}) Y g" and fg: "⋀x. ⟦x ∈ topspace X; p x ∈ Z frontier_of U⟧ ⟹ f x = g x" shows "continuous_map X Y (λx. if p x ∈ U then f x else g x)" proof (rule continuous_map_cases_alt) show "continuous_map (subtopology X (X closure_of {x ∈ topspace X. p x ∈ U})) Y f" proof (rule continuous_map_from_subtopology_mono) let ?T = "{x ∈ topspace X. p x ∈ Z closure_of U}" show "continuous_map (subtopology X ?T) Y f" by (simp add: contf) show "X closure_of {x ∈ topspace X. p x ∈ U} ⊆ ?T" by (rule continuous_map_closure_preimage_subset [OF contp]) qed show "continuous_map (subtopology X (X closure_of {x ∈ topspace X. p x ∉ U})) Y g" proof (rule continuous_map_from_subtopology_mono) let ?T = "{x ∈ topspace X. p x ∈ Z closure_of (topspace Z - U)}" show "continuous_map (subtopology X ?T) Y g" by (simp add: contg) have "X closure_of {x ∈ topspace X. p x ∉ U} ⊆ X closure_of {x ∈ topspace X. p x ∈ topspace Z - U}" by (smt (verit) Collect_mono_iff DiffI closure_of_mono continuous_map contp image_subset_iff) then show "X closure_of {x ∈ topspace X. p x ∉ U} ⊆ ?T" by (rule order_trans [OF _ continuous_map_closure_preimage_subset [OF contp]]) qed next show "f x = g x" if "x ∈ X frontier_of {x ∈ topspace X. p x ∈ U}" for x using that continuous_map_frontier_frontier_preimage_subset [OF contp, of U] fg by blast qed subsection ‹Retractions› definition✐‹tag important› retraction :: "('a::topological_space) set ⇒ 'a set ⇒ ('a ⇒ 'a) ⇒ bool" where "retraction S T r ⟷ T ⊆ S ∧ continuous_on S r ∧ r ∈ S → T ∧ (∀x∈T. r x = x)" definition✐‹tag important› retract_of (infixl "retract'_of" 50) where "T retract_of S ⟷ (∃r. retraction S T r)" lemma retraction_idempotent: "retraction S T r ⟹ x ∈ S ⟹ r (r x) = r x" unfolding retraction_def by auto text ‹Preservation of fixpoints under (more general notion of) retraction› lemma invertible_fixpoint_property: fixes S :: "'a::topological_space set" and T :: "'b::topological_space set" assumes contt: "continuous_on T i" and "i ∈ T → S" and contr: "continuous_on S r" and "r ∈ S → T" and ri: "⋀y. y ∈ T ⟹ r (i y) = y" and FP: "⋀f. ⟦continuous_on S f; f ∈ S → S⟧ ⟹ ∃x∈S. f x = x" and contg: "continuous_on T g" and "g ∈ T → T" obtains y where "y ∈ T" and "g y = y" proof - have "∃x∈S. (i ∘ g ∘ r) x = x" proof (rule FP) show "continuous_on S (i ∘ g ∘ r)" by (metis assms(4) assms(8) contg continuous_on_compose continuous_on_subset contr contt funcset_image) show "(i ∘ g ∘ r) ∈ S → S" using assms(2,4,8) by force qed then obtain x where x: "x ∈ S" "(i ∘ g ∘ r) x = x" .. then have *: "g (r x) ∈ T" using assms(4,8) by auto have "r ((i ∘ g ∘ r) x) = r x" using x by auto then show ?thesis using "*" ri that by auto qed lemma homeomorphic_fixpoint_property: fixes S :: "'a::topological_space set" and T :: "'b::topological_space set" assumes "S homeomorphic T" shows "(∀f. continuous_on S f ∧ f ∈ S → S ⟶ (∃x∈S. f x = x)) ⟷ (∀g. continuous_on T g ∧ g ∈ T → T ⟶ (∃y∈T. g y = y))" (is "?lhs = ?rhs") proof - obtain r i where r: "∀x∈S. i (r x) = x" "r ` S = T" "continuous_on S r" "∀y∈T. r (i y) = y" "i ` T = S" "continuous_on T i" using assms unfolding homeomorphic_def homeomorphism_def by blast show ?thesis proof assume ?lhs with r show ?rhs by (smt (verit, del_insts) Pi_iff image_eqI invertible_fixpoint_property[of T i S r]) next assume ?rhs with r show ?lhs by (smt (verit, del_insts) Pi_iff image_eqI invertible_fixpoint_property[of S r T i]) qed qed lemma retract_fixpoint_property: fixes f :: "'a::topological_space ⇒ 'b::topological_space" and S :: "'a set" assumes "T retract_of S" and FP: "⋀f. ⟦continuous_on S f; f ∈ S → S⟧ ⟹ ∃x∈S. f x = x" and contg: "continuous_on T g" and "g ∈ T → T" obtains y where "y ∈ T" and "g y = y" proof - obtain h where "retraction S T h" using assms(1) unfolding retract_of_def .. then show ?thesis unfolding retraction_def using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP] by (smt (verit, del_insts) Pi_iff assms(4) contg subsetD that) qed lemma retraction: "retraction S T r ⟷ T ⊆ S ∧ continuous_on S r ∧ r ` S = T ∧ (∀x ∈ T. r x = x)" by (force simp: retraction_def simp flip: image_subset_iff_funcset) lemma retractionE: ― ‹yields properties normalized wrt. simp -- less likely to loop› assumes "retraction S T r" obtains "T = r ` S" "r ∈ S → S" "continuous_on S r" "⋀x. x ∈ S ⟹ r (r x) = r x" proof (rule that) from retraction [of S T r] assms have "T ⊆ S" "continuous_on S r" "r ` S = T" and "∀x ∈ T. r x = x" by simp_all then show "r ∈ S → S" "continuous_on S r" by auto then show "T = r ` S" using ‹r ` S = T› by blast from ‹∀x ∈ T. r x = x› have "r x = x" if "x ∈ T" for x using that by simp with ‹r ` S = T› show "r (r x) = r x" if "x ∈ S" for x using that by auto qed lemma retract_ofE: ― ‹yields properties normalized wrt. simp -- less likely to loop› assumes "T retract_of S" obtains r where "T = r ` S" "r ∈ S → S" "continuous_on S r" "⋀x. x ∈ S ⟹ r (r x) = r x" proof - from assms obtain r where "retraction S T r" by (auto simp add: retract_of_def) with that show thesis by (auto elim: retractionE) qed lemma retract_of_imp_extensible: assumes "S retract_of T" and "continuous_on S f" and "f ∈ S → U" obtains g where "continuous_on T g" "g ∈ T → U" "⋀x. x ∈ S ⟹ g x = f x" proof - from ‹S retract_of T› obtain r where "retraction T S r" by (auto simp add: retract_of_def) then have "continuous_on T (f ∘ r)" by (metis assms(2) continuous_on_compose retraction) then show thesis by (smt (verit, best) Pi_iff ‹retraction T S r› assms(3) comp_apply retraction_def that) qed lemma idempotent_imp_retraction: assumes "continuous_on S f" and "f ∈ S → S" and "⋀x. x ∈ S ⟹ f(f x) = f x" shows "retraction S (f ` S) f" by (simp add: assms funcset_image retraction) lemma retraction_subset: assumes "retraction S T r" and "T ⊆ S'" and "S' ⊆ S" shows "retraction S' T r" unfolding retraction_def by (metis assms continuous_on_subset image_mono image_subset_iff_funcset retraction) lemma retract_of_subset: assumes "T retract_of S" and "T ⊆ S'" and "S' ⊆ S" shows "T retract_of S'" by (meson assms retract_of_def retraction_subset) lemma retraction_refl [simp]: "retraction S S (λx. x)" by (simp add: retraction) lemma retract_of_refl [iff]: "S retract_of S" unfolding retract_of_def retraction_def using continuous_on_id by blast lemma retract_of_imp_subset: "S retract_of T ⟹ S ⊆ T" by (simp add: retract_of_def retraction_def) lemma retract_of_empty [simp]: "({} retract_of S) ⟷ S = {}" "(S retract_of {}) ⟷ S = {}" by (auto simp: retract_of_def retraction_def) lemma retract_of_singleton [iff]: "({x} retract_of S) ⟷ x ∈ S" unfolding retract_of_def retraction_def by force lemma retraction_comp: "⟦retraction S T f; retraction T U g⟧ ⟹ retraction S U (g ∘ f)" by (smt (verit, best) comp_apply continuous_on_compose image_comp retraction subset_iff) lemma retract_of_trans [trans]: assumes "S retract_of T" and "T retract_of U" shows "S retract_of U" using assms by (auto simp: retract_of_def intro: retraction_comp) lemma closedin_retract: fixes S :: "'a :: t2_space set" assumes "S retract_of T" shows "closedin (top_of_set T) S" proof - obtain r where r: "S ⊆ T" "continuous_on T r" "r ∈ T → S" "⋀x. x ∈ S ⟹ r x = x" using assms by (auto simp: retract_of_def retraction_def) have "S = {x∈T. x = r x}" using r by force also have "… = T ∩ ((λx. (x, r x)) -` ({y. ∃x. y = (x, x)}))" unfolding vimage_def mem_Times_iff fst_conv snd_conv using r by auto also have "closedin (top_of_set T) …" by (rule continuous_closedin_preimage) (auto intro!: closed_diagonal continuous_on_Pair r) finally show ?thesis . qed lemma closedin_self [simp]: "closedin (top_of_set S) S" by simp lemma retract_of_closed: fixes S :: "'a :: t2_space set" shows "⟦closed T; S retract_of T⟧ ⟹ closed S" by (metis closedin_retract closedin_closed_eq) lemma retract_of_compact: "⟦compact T; S retract_of T⟧ ⟹ compact S" by (metis compact_continuous_image retract_of_def retraction) lemma retract_of_connected: "⟦connected T; S retract_of T⟧ ⟹ connected S" by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction) lemma retraction_openin_vimage_iff: assumes r: "retraction S T r" and "U ⊆ T" shows "openin (top_of_set S) (S ∩ r -` U) ⟷ openin (top_of_set T) U" (is "?lhs = ?rhs") proof show "?lhs ⟹ ?rhs" using r by (smt (verit, del_insts) assms(2) continuous_right_inverse_imp_quotient_map image_subset_iff_funcset r retractionE retraction_def retraction_subset) show "?rhs ⟹ ?lhs" by (metis continuous_on_open r retraction) qed lemma retract_of_Times: "⟦S retract_of S'; T retract_of T'⟧ ⟹ (S × T) retract_of (S' × T')" apply (simp add: retract_of_def retraction_def Sigma_mono, clarify) apply (rename_tac f g) apply (rule_tac x="λz. ((f ∘ fst) z, (g ∘ snd) z)" in exI) apply (rule conjI continuous_intros | erule continuous_on_subset | force)+ done subsection‹Retractions on a topological space› definition retract_of_space :: "'a set ⇒ 'a topology ⇒ bool" (infix "retract'_of'_space" 50) where "S retract_of_space X ≡ S ⊆ topspace X ∧ (∃r. continuous_map X (subtopology X S) r ∧ (∀x ∈ S. r x = x))" lemma retract_of_space_retraction_maps: "S retract_of_space X ⟷ S ⊆ topspace X ∧ (∃r. retraction_maps X (subtopology X S) r id)" by (auto simp: retract_of_space_def retraction_maps_def) lemma retract_of_space_section_map: "S retract_of_space X ⟷ S ⊆ topspace X ∧ section_map (subtopology X S) X id" unfolding retract_of_space_def retraction_maps_def section_map_def by (auto simp: continuous_map_from_subtopology) lemma retract_of_space_imp_subset: "S retract_of_space X ⟹ S ⊆ topspace X" by (simp add: retract_of_space_def) lemma retract_of_space_topspace: "topspace X retract_of_space X" using retract_of_space_def by force lemma retract_of_space_empty [simp]: "{} retract_of_space X ⟷ X = trivial_topology" by (auto simp: retract_of_space_def) lemma retract_of_space_singleton [simp]: "{a} retract_of_space X ⟷ a ∈ topspace X" proof - have "continuous_map X (subtopology X {a}) (λx. a) ∧ (λx. a) a = a" if "a ∈ topspace X" using that by simp then show ?thesis by (force simp: retract_of_space_def) qed lemma retract_of_space_trans: assumes "S retract_of_space X" "T retract_of_space subtopology X S" shows "T retract_of_space X" using assms apply (simp add: retract_of_space_retraction_maps) by (metis id_comp inf.absorb_iff2 retraction_maps_compose subtopology_subtopology) lemma retract_of_space_subtopology: assumes "S retract_of_space X" "S ⊆ U" shows "S retract_of_space subtopology X U" using assms apply (clarsimp simp: retract_of_space_def) by (metis continuous_map_from_subtopology inf.absorb2 subtopology_subtopology) lemma retract_of_space_clopen: assumes "openin X S" "closedin X S" "S = {} ⟹ X = trivial_topology" shows "S retract_of_space X" proof (cases "S = {}") case False then obtain a where "a ∈ S" by blast show ?thesis unfolding retract_of_space_def proof (intro exI conjI) show "S ⊆ topspace X" by (simp add: assms closedin_subset) have "continuous_map X X (λx. if x ∈ S then x else a)" proof (rule continuous_map_cases) show "continuous_map (subtopology X (X closure_of {x. x ∈ S})) X (λx. x)" by (simp add: continuous_map_from_subtopology) show "continuous_map (subtopology X (X closure_of {x. x ∉ S})) X (λx. a)" using ‹S ⊆ topspace X› ‹a ∈ S› by force show "x = a" if "x ∈ X frontier_of {x. x ∈ S}" for x using assms that clopenin_eq_frontier_of by fastforce qed then show "continuous_map X (subtopology X S) (λx. if x ∈ S then x else a)" using ‹S ⊆ topspace X› ‹a ∈ S› by (auto simp: continuous_map_in_subtopology) qed auto qed (use assms in auto) lemma retract_of_space_disjoint_union: assumes "openin X S" "openin X T" and ST: "disjnt S T" "S ∪ T = topspace X" and "S = {} ⟹ X = trivial_topology" shows "S retract_of_space X" proof (rule retract_of_space_clopen) have "S ∩ T = {}" by (meson ST disjnt_def) then have "S = topspace X - T" using ST by auto then show "closedin X S" using ‹openin X T› by blast qed (auto simp: assms) lemma retraction_maps_section_image1: assumes "retraction_maps X Y r s" shows "s ` (topspace Y) retract_of_space X" unfolding retract_of_space_section_map proof show "s ` topspace Y ⊆ topspace X" using assms continuous_map_image_subset_topspace retraction_maps_def by blast show "section_map (subtopology X (s ` topspace Y)) X id" unfolding section_map_def using assms retraction_maps_to_retract_maps by blast qed lemma retraction_maps_section_image2: "retraction_maps X Y r s ⟹ subtopology X (s ` (topspace Y)) homeomorphic_space Y" using embedding_map_imp_homeomorphic_space homeomorphic_space_sym section_imp_embedding_map section_map_def by blast lemma hereditary_imp_retractive_property: assumes "⋀X S. P X ⟹ P(subtopology X S)" "⋀X X'. X homeomorphic_space X' ⟹ (P X ⟷ Q X')" assumes "retraction_map X X' r" "P X" shows "Q X'" by (meson assms retraction_map_def retraction_maps_section_image2) subsection‹Paths and path-connectedness› definition pathin :: "'a topology ⇒ (real ⇒ 'a) ⇒ bool" where "pathin X g ≡ continuous_map (subtopology euclideanreal {0..1}) X g" lemma pathin_compose: "⟦pathin X g; continuous_map X Y f⟧ ⟹ pathin Y (f ∘ g)" by (simp add: continuous_map_compose pathin_def) lemma pathin_subtopology: "pathin (subtopology X S) g ⟷ pathin X g ∧ (∀x ∈ {0..1}. g x ∈ S)" by (auto simp: pathin_def continuous_map_in_subtopology) lemma pathin_const [simp]: "pathin X (λx. a) ⟷ a ∈ topspace X" using pathin_subtopology by (fastforce simp add: pathin_def) lemma path_start_in_topspace: "pathin X g ⟹ g 0 ∈ topspace X" by (force simp: pathin_def continuous_map) lemma path_finish_in_topspace: "pathin X g ⟹ g 1 ∈ topspace X" by (force simp: pathin_def continuous_map) lemma path_image_subset_topspace: "pathin X g ⟹ g ∈ ({0..1}) → topspace X" by (force simp: pathin_def continuous_map) definition path_connected_space :: "'a topology ⇒ bool" where "path_connected_space X ≡ ∀x ∈ topspace X. ∀ y ∈ topspace X. ∃g. pathin X g ∧ g 0 = x ∧ g 1 = y" definition path_connectedin :: "'a topology ⇒ 'a set ⇒ bool" where "path_connectedin X S ≡ S ⊆ topspace X ∧ path_connected_space(subtopology X S)" lemma path_connectedin_absolute [simp]: "path_connectedin (subtopology X S) S ⟷ path_connectedin X S" by (simp add: path_connectedin_def subtopology_subtopology) lemma path_connectedin_subset_topspace: "path_connectedin X S ⟹ S ⊆ topspace X" by (simp add: path_connectedin_def) lemma path_connectedin_subtopology: "path_connectedin (subtopology X S) T ⟷ path_connectedin X T ∧ T ⊆ S" by (auto simp: path_connectedin_def subtopology_subtopology inf.absorb2) lemma path_connectedin: "path_connectedin X S ⟷ S ⊆ topspace X ∧ (∀x ∈ S. ∀y ∈ S. ∃g. pathin X g ∧ g ∈ {0..1} → S ∧ g 0 = x ∧ g 1 = y)" unfolding path_connectedin_def path_connected_space_def pathin_def continuous_map_in_subtopology by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2 flip: image_subset_iff_funcset) lemma path_connectedin_topspace: "path_connectedin X (topspace X) ⟷ path_connected_space X" by (simp add: path_connectedin_def) lemma path_connected_imp_connected_space: assumes "path_connected_space X" shows "connected_space X" proof - have *: "∃S. connectedin X S ∧ g 0 ∈ S ∧ g 1 ∈ S" if "pathin X g" for g proof (intro exI conjI) have "continuous_map (subtopology euclideanreal {0..1}) X g" using connectedin_absolute that by (simp add: pathin_def) then show "connectedin X (g ` {0..1})" by (rule connectedin_continuous_map_image) auto qed auto show ?thesis using assms by (auto intro: * simp add: path_connected_space_def connected_space_subconnected Ball_def) qed lemma path_connectedin_imp_connectedin: "path_connectedin X S ⟹ connectedin X S" by (simp add: connectedin_def path_connected_imp_connected_space path_connectedin_def) lemma path_connected_space_topspace_empty: "path_connected_space trivial_topology" by (simp add: path_connected_space_def) lemma path_connectedin_empty [simp]: "path_connectedin X {}" by (simp add: path_connectedin) lemma path_connectedin_singleton [simp]: "path_connectedin X {a} ⟷ a ∈ topspace X" proof show "path_connectedin X {a} ⟹ a ∈ topspace X" by (simp add: path_connectedin) show "a ∈ topspace X ⟹ path_connectedin X {a}" unfolding path_connectedin using pathin_const by fastforce qed lemma path_connectedin_continuous_map_image: assumes f: "continuous_map X Y f" and S: "path_connectedin X S" shows "path_connectedin Y (f ` S)" proof - have fX: "f ∈ (topspace X) → topspace Y" using continuous_map_def f by fastforce show ?thesis unfolding path_connectedin proof (intro conjI ballI; clarify?) fix x assume "x ∈ S" show "f x ∈ topspace Y" using S ‹x ∈ S› fX path_connectedin_subset_topspace by fastforce next fix x y assume "x ∈ S" and "y ∈ S" then obtain g where g: "pathin X g" "g ∈ {0..1} → S" "g 0 = x" "g 1 = y" using S by (force simp: path_connectedin) show "∃g. pathin Y g ∧ g ∈ {0..1} → f ` S ∧ g 0 = f x ∧ g 1 = f y" proof (intro exI conjI) show "pathin Y (f ∘ g)" using ‹pathin X g› f pathin_compose by auto qed (use g in auto) qed qed lemma path_connectedin_discrete_topology: "path_connectedin (discrete_topology U) S ⟷ S ⊆ U ∧ (∃a. S ⊆ {a})" (is "?lhs = ?rhs") proof show "?lhs ⟹ ?rhs" by (meson connectedin_discrete_topology path_connectedin_imp_connectedin) show "?rhs ⟹ ?lhs" using subset_singletonD by fastforce qed lemma path_connected_space_discrete_topology: "path_connected_space (discrete_topology U) ⟷ (∃a. U ⊆ {a})" by (metis path_connectedin_discrete_topology path_connectedin_topspace path_connected_space_topspace_empty subset_singletonD topspace_discrete_topology) lemma homeomorphic_path_connected_space_imp: "⟦path_connected_space X; X homeomorphic_space Y⟧ ⟹ path_connected_space Y" unfolding homeomorphic_space_def homeomorphic_maps_def by (smt (verit, ccfv_threshold) homeomorphic_imp_surjective_map homeomorphic_maps_def homeomorphic_maps_map path_connectedin_continuous_map_image path_connectedin_topspace) lemma homeomorphic_path_connected_space: "X homeomorphic_space Y ⟹ path_connected_space X ⟷ path_connected_space Y" by (meson homeomorphic_path_connected_space_imp homeomorphic_space_sym) lemma homeomorphic_map_path_connectedness: assumes "homeomorphic_map X Y f" "U ⊆ topspace X" shows "path_connectedin Y (f ` U) ⟷ path_connectedin X U" unfolding path_connectedin_def proof (intro conj_cong homeomorphic_path_connected_space) show "f ` U ⊆ topspace Y ⟷ (U ⊆ topspace X)" using assms homeomorphic_imp_surjective_map by blast next assume "U ⊆ topspace X" show "subtopology Y (f ` U) homeomorphic_space subtopology X U" using assms unfolding homeomorphic_eq_everything_map by (metis (no_types, opaque_lifting) assms homeomorphic_map_subtopologies homeomorphic_space homeomorphic_space_sym image_mono inf.absorb_iff2) qed lemma homeomorphic_map_path_connectedness_eq: "homeomorphic_map X Y f ⟹ path_connectedin X U ⟷ U ⊆ topspace X ∧ path_connectedin Y (f ` U)" by (meson homeomorphic_map_path_connectedness path_connectedin_def) subsection‹Connected components› definition connected_component_of :: "'a topology ⇒ 'a ⇒ 'a ⇒ bool" where "connected_component_of X x y ≡ ∃T. connectedin X T ∧ x ∈ T ∧ y ∈ T" abbreviation connected_component_of_set where "connected_component_of_set X x ≡ Collect (connected_component_of X x)" definition connected_components_of :: "'a topology ⇒ ('a set) set" where "connected_components_of X ≡ connected_component_of_set X ` topspace X" lemma connected_component_in_topspace: "connected_component_of X x y ⟹ x ∈ topspace X ∧ y ∈ topspace X" by (meson connected_component_of_def connectedin_subset_topspace in_mono) lemma connected_component_of_refl: "connected_component_of X x x ⟷ x ∈ topspace X" by (meson connected_component_in_topspace connected_component_of_def connectedin_sing insertI1) lemma connected_component_of_sym: "connected_component_of X x y ⟷ connected_component_of X y x" by (meson connected_component_of_def) lemma connected_component_of_trans: "⟦connected_component_of X x y; connected_component_of X y z⟧ ⟹ connected_component_of X x z" unfolding connected_component_of_def using connectedin_Un by blast lemma connected_component_of_mono: "⟦connected_component_of (subtopology X S) x y; S ⊆ T⟧ ⟹ connected_component_of (subtopology X T) x y" by (metis connected_component_of_def connectedin_subtopology inf.absorb_iff2 subtopology_subtopology) lemma connected_component_of_set: "connected_component_of_set X x = {y. ∃T. connectedin X T ∧ x ∈ T ∧ y ∈ T}" by (meson connected_component_of_def) lemma connected_component_of_subset_topspace: "connected_component_of_set X x ⊆ topspace X" using connected_component_in_topspace by force lemma connected_component_of_eq_empty: "connected_component_of_set X x = {} ⟷ (x ∉ topspace X)" using connected_component_in_topspace connected_component_of_refl by fastforce lemma connected_space_iff_connected_component: "connected_space X ⟷ (∀x ∈ topspace X. ∀y ∈ topspace X. connected_component_of X x y)" by (simp add: connected_component_of_def connected_space_subconnected) lemma connected_space_imp_connected_component_of: "⟦connected_space X; a ∈ topspace X; b ∈ topspace X⟧ ⟹ connected_component_of X a b" by (simp add: connected_space_iff_connected_component) lemma connected_space_connected_component_set: "connected_space X ⟷ (∀x ∈ topspace X. connected_component_of_set X x = topspace X)" using connected_component_of_subset_topspace connected_space_iff_connected_component by fastforce lemma connected_component_of_maximal: "⟦connectedin X S; x ∈ S⟧ ⟹ S ⊆ connected_component_of_set X x" by (meson Ball_Collect connected_component_of_def) lemma connected_component_of_equiv: "connected_component_of X x y ⟷ x ∈ topspace X ∧ y ∈ topspace X ∧ connected_component_of X x = connected_component_of X y" apply (simp add: connected_component_in_topspace fun_eq_iff) by (meson connected_component_of_refl connected_component_of_sym connected_component_of_trans) lemma connected_component_of_disjoint: "disjnt (connected_component_of_set X x) (connected_component_of_set X y) ⟷ ~(connected_component_of X x y)" using connected_component_of_equiv unfolding disjnt_iff by force lemma connected_component_of_eq: "connected_component_of X x = connected_component_of X y ⟷ (x ∉ topspace X) ∧ (y ∉ topspace X) ∨ x ∈ topspace X ∧ y ∈ topspace X ∧ connected_component_of X x y" by (metis Collect_empty_eq_bot connected_component_of_eq_empty connected_component_of_equiv) lemma connectedin_connected_component_of: "connectedin X (connected_component_of_set X x)" proof - have "connected_component_of_set X x = ⋃ {T. connectedin X T ∧ x ∈ T}" by (auto simp: connected_component_of_def) then show ?thesis by (metis (no_types, lifting) InterI connectedin_Union emptyE mem_Collect_eq) qed lemma Union_connected_components_of: "⋃(connected_components_of X) = topspace X" unfolding connected_components_of_def using connected_component_in_topspace connected_component_of_refl by fastforce lemma connected_components_of_maximal: "⟦C ∈ connected_components_of X; connectedin X S; ~disjnt C S⟧ ⟹ S ⊆ C" unfolding connected_components_of_def disjnt_def apply clarify by (metis Int_emptyI connected_component_of_def connected_component_of_trans mem_Collect_eq) lemma pairwise_disjoint_connected_components_of: "pairwise disjnt (connected_components_of X)" unfolding connected_components_of_def pairwise_def by (smt (verit, best) connected_component_of_disjoint connected_component_of_eq imageE) lemma complement_connected_components_of_Union: "C ∈ connected_components_of X ⟹ topspace X - C = ⋃ (connected_components_of X - {C})" by (metis Union_connected_components_of bot.extremum ccpo_Sup_singleton diff_Union_pairwise_disjoint insert_subset pairwise_disjoint_connected_components_of) lemma nonempty_connected_components_of: "C ∈ connected_components_of X ⟹ C ≠ {}" unfolding connected_components_of_def by (metis (no_types, lifting) connected_component_of_eq_empty imageE) lemma connected_components_of_subset: "C ∈ connected_components_of X ⟹ C ⊆ topspace X" using Union_connected_components_of by fastforce lemma connectedin_connected_components_of: assumes "C ∈ connected_components_of X" shows "connectedin X C" proof - have "C ∈ connected_component_of_set X ` topspace X" using assms connected_components_of_def by blast then show ?thesis using connectedin_connected_component_of by fastforce qed lemma