section‹Lindel\"of spaces› theory Lindelof_Spaces imports T1_Spaces begin definition Lindelof_space where "Lindelof_space X ≡ ∀𝒰. (∀U ∈ 𝒰. openin X U) ∧ ⋃𝒰 = topspace X ⟶ (∃𝒱. countable 𝒱 ∧ 𝒱 ⊆ 𝒰 ∧ ⋃𝒱 = topspace X)" lemma Lindelof_spaceD: "⟦Lindelof_space X; ⋀U. U ∈ 𝒰 ⟹ openin X U; ⋃𝒰 = topspace X⟧ ⟹ ∃𝒱. countable 𝒱 ∧ 𝒱 ⊆ 𝒰 ∧ ⋃𝒱 = topspace X" by (auto simp: Lindelof_space_def) lemma Lindelof_space_alt: "Lindelof_space X ⟷ (∀𝒰. (∀U ∈ 𝒰. openin X U) ∧ topspace X ⊆ ⋃𝒰 ⟶ (∃𝒱. countable 𝒱 ∧ 𝒱 ⊆ 𝒰 ∧ topspace X ⊆ ⋃𝒱))" unfolding Lindelof_space_def using openin_subset by fastforce lemma compact_imp_Lindelof_space: "compact_space X ⟹ Lindelof_space X" unfolding Lindelof_space_def compact_space by (meson uncountable_infinite) lemma Lindelof_space_topspace_empty: "topspace X = {} ⟹ Lindelof_space X" using compact_imp_Lindelof_space compact_space_topspace_empty by blast lemma Lindelof_space_Union: assumes 𝒰: "countable 𝒰" and lin: "⋀U. U ∈ 𝒰 ⟹ Lindelof_space (subtopology X U)" shows "Lindelof_space (subtopology X (⋃𝒰))" proof - have "∃𝒱. countable 𝒱 ∧ 𝒱 ⊆ ℱ ∧ ⋃𝒰 ∩ ⋃𝒱 = topspace X ∩ ⋃𝒰" if ℱ: "ℱ ⊆ Collect (openin X)" and UF: "⋃𝒰 ∩ ⋃ℱ = topspace X ∩ ⋃𝒰" for ℱ proof - have "⋀U. ⟦U ∈ 𝒰; U ∩ ⋃ℱ = topspace X ∩ U⟧ ⟹ ∃𝒱. countable 𝒱 ∧ 𝒱 ⊆ ℱ ∧ U ∩ ⋃𝒱 = topspace X ∩ U" using lin ℱ unfolding Lindelof_space_def openin_subtopology_alt Ball_def subset_iff [symmetric] by (simp add: all_subset_image imp_conjL ex_countable_subset_image) then obtain g where g: "⋀U. ⟦U ∈ 𝒰; U ∩ ⋃ℱ = topspace X ∩ U⟧ ⟹ countable (g U) ∧ (g U) ⊆ ℱ ∧ U ∩ ⋃(g U) = topspace X ∩ U" by metis show ?thesis proof (intro exI conjI) show "countable (⋃(g ` 𝒰))" using Int_commute UF g by (fastforce intro: countable_UN [OF 𝒰]) show "⋃(g ` 𝒰) ⊆ ℱ" using g UF by blast show "⋃𝒰 ∩ ⋃(⋃(g ` 𝒰)) = topspace X ∩ ⋃𝒰" proof show "⋃𝒰 ∩ ⋃(⋃(g ` 𝒰)) ⊆ topspace X ∩ ⋃𝒰" using g UF by blast show "topspace X ∩ ⋃𝒰 ⊆ ⋃𝒰 ∩ ⋃(⋃(g ` 𝒰))" proof clarsimp show "∃y∈𝒰. ∃W∈g y. x ∈ W" if "x ∈ topspace X" "x ∈ V" "V ∈ 𝒰" for x V proof - have "V ∩ ⋃ℱ = topspace X ∩ V" using UF ‹V ∈ 𝒰› by blast with that g [OF ‹V ∈ 𝒰›] show ?thesis by blast qed qed qed qed qed then show ?thesis unfolding Lindelof_space_def openin_subtopology_alt Ball_def subset_iff [symmetric] by (simp add: all_subset_image imp_conjL ex_countable_subset_image) qed lemma countable_imp_Lindelof_space: assumes "countable(topspace X)" shows "Lindelof_space X" proof - have "Lindelof_space (subtopology X (⋃x ∈ topspace X. {x}))" proof (rule Lindelof_space_Union) show "countable ((λx. {x}) ` topspace X)" using assms by blast show "Lindelof_space (subtopology X U)" if "U ∈ (λx. {x}) ` topspace X" for U proof - have "compactin X U" using that by force then show ?thesis by (meson compact_imp_Lindelof_space compact_space_subtopology) qed qed then show ?thesis by simp qed lemma Lindelof_space_subtopology: "Lindelof_space(subtopology X S) ⟷ (∀𝒰. (∀U ∈ 𝒰. openin X U) ∧ topspace X ∩ S ⊆ ⋃𝒰 ⟶ (∃V. countable V ∧ V ⊆ 𝒰 ∧ topspace X ∩ S ⊆ ⋃V))" proof - have *: "(S ∩ ⋃𝒰 = topspace X ∩ S) = (topspace X ∩ S ⊆ ⋃𝒰)" if "⋀x. x ∈ 𝒰 ⟹ openin X x" for 𝒰 by (blast dest: openin_subset [OF that]) moreover have "(𝒱 ⊆ 𝒰 ∧ S ∩ ⋃𝒱 = topspace X ∩ S) = (𝒱 ⊆ 𝒰 ∧ topspace X ∩ S ⊆ ⋃𝒱)" if "∀x. x ∈ 𝒰 ⟶ openin X x" "topspace X ∩ S ⊆ ⋃𝒰" "countable 𝒱" for 𝒰 𝒱 using that * by blast ultimately show ?thesis unfolding Lindelof_space_def openin_subtopology_alt Ball_def apply (simp add: all_subset_image imp_conjL ex_countable_subset_image flip: subset_iff) apply (intro all_cong1 imp_cong ex_cong, auto) done qed lemma Lindelof_space_subtopology_subset: "S ⊆ topspace X ⟹ (Lindelof_space(subtopology X S) ⟷ (∀𝒰. (∀U ∈ 𝒰. openin X U) ∧ S ⊆ ⋃𝒰 ⟶ (∃V. countable V ∧ V ⊆ 𝒰 ∧ S ⊆ ⋃V)))" by (metis Lindelof_space_subtopology topspace_subtopology topspace_subtopology_subset) lemma Lindelof_space_closedin_subtopology: assumes X: "Lindelof_space X" and clo: "closedin X S" shows "Lindelof_space (subtopology X S)" proof - have "S ⊆ topspace X" by (simp add: clo closedin_subset) then show ?thesis proof (clarsimp simp add: Lindelof_space_subtopology_subset) show "∃V. countable V ∧ V ⊆ ℱ ∧ S ⊆ ⋃V" if "∀U∈ℱ. openin X U" and "S ⊆ ⋃ℱ" for ℱ proof - have "∃𝒱. countable 𝒱 ∧ 𝒱 ⊆ insert (topspace X - S) ℱ ∧ ⋃𝒱 = topspace X" proof (rule Lindelof_spaceD [OF X, of "insert (topspace X - S) ℱ"]) show "openin X U" if "U ∈ insert (topspace X - S) ℱ" for U using that ‹∀U∈ℱ. openin X U› clo by blast show "⋃(insert (topspace X - S) ℱ) = topspace X" apply auto apply (meson in_mono openin_closedin_eq that(1)) using UnionE ‹S ⊆ ⋃ℱ› by auto qed then obtain 𝒱 where "countable 𝒱" "𝒱 ⊆ insert (topspace X - S) ℱ" "⋃𝒱 = topspace X" by metis with ‹S ⊆ topspace X› show ?thesis by (rule_tac x="(𝒱 - {topspace X - S})" in exI) auto qed qed qed lemma Lindelof_space_continuous_map_image: assumes X: "Lindelof_space X" and f: "continuous_map X Y f" and fim: "f ` (topspace X) = topspace Y" shows "Lindelof_space Y" proof - have "∃𝒱. countable 𝒱 ∧ 𝒱 ⊆ 𝒰 ∧ ⋃𝒱 = topspace Y" if 𝒰: "⋀U. U ∈ 𝒰 ⟹ openin Y U" and UU: "⋃𝒰 = topspace Y" for 𝒰 proof - define 𝒱 where "𝒱 ≡ (λU. {x ∈ topspace X. f x ∈ U}) ` 𝒰" have "⋀V. V ∈ 𝒱 ⟹ openin X V" unfolding 𝒱_def using 𝒰 continuous_map f by fastforce moreover have "⋃𝒱 = topspace X" unfolding 𝒱_def using UU fim by fastforce ultimately have "∃𝒲. countable 𝒲 ∧ 𝒲 ⊆ 𝒱 ∧ ⋃𝒲 = topspace X" using X by (simp add: Lindelof_space_def) then obtain 𝒞 where "countable 𝒞" "𝒞 ⊆ 𝒰" and 𝒞: "(⋃U∈𝒞. {x ∈ topspace X. f x ∈ U}) = topspace X" by (metis (no_types, lifting) 𝒱_def countable_subset_image) moreover have "⋃𝒞 = topspace Y" proof show "⋃𝒞 ⊆ topspace Y" using UU 𝒞 ‹𝒞 ⊆ 𝒰› by fastforce have "y ∈ ⋃𝒞" if "y ∈ topspace Y" for y proof - obtain x where "x ∈ topspace X" "y = f x" using that fim by (metis ‹y ∈ topspace Y› imageE) with 𝒞 show ?thesis by auto qed then show "topspace Y ⊆ ⋃𝒞" by blast qed ultimately show ?thesis by blast qed then show ?thesis unfolding Lindelof_space_def by auto qed lemma Lindelof_space_quotient_map_image: "⟦quotient_map X Y q; Lindelof_space X⟧ ⟹ Lindelof_space Y" by (meson Lindelof_space_continuous_map_image quotient_imp_continuous_map quotient_imp_surjective_map) lemma Lindelof_space_retraction_map_image: "⟦retraction_map X Y r; Lindelof_space X⟧ ⟹ Lindelof_space Y" using Abstract_Topology.retraction_imp_quotient_map Lindelof_space_quotient_map_image by blast lemma locally_finite_cover_of_Lindelof_space: assumes X: "Lindelof_space X" and UU: "topspace X ⊆ ⋃𝒰" and fin: "locally_finite_in X 𝒰" shows "countable 𝒰" proof - have UU_eq: "⋃𝒰 = topspace X" by (meson UU fin locally_finite_in_def subset_antisym) obtain T where T: "⋀x. x ∈ topspace X ⟹ openin X (T x) ∧ x ∈ T x ∧ finite {U ∈ 𝒰. U ∩ T x ≠ {}}" using fin unfolding locally_finite_in_def by meson then obtain I where "countable I" "I ⊆ topspace X" and I: "topspace X ⊆ ⋃(T ` I)" using X unfolding Lindelof_space_alt by (drule_tac x="image T (topspace X)" in spec) (auto simp: ex_countable_subset_image) show ?thesis proof (rule countable_subset) have "⋀i. i ∈ I ⟹ countable {U ∈ 𝒰. U ∩ T i ≠ {}}" using T by (meson ‹I ⊆ topspace X› in_mono uncountable_infinite) then show "countable (insert {} (⋃i∈I. {U ∈ 𝒰. U ∩ T i ≠ {}}))" by (simp add: ‹countable I›) qed (use UU_eq I in auto) qed lemma Lindelof_space_proper_map_preimage: assumes f: "proper_map X Y f" and Y: "Lindelof_space Y" shows "Lindelof_space X" proof (clarsimp simp: Lindelof_space_alt) show "∃𝒱. countable 𝒱 ∧ 𝒱 ⊆ 𝒰 ∧ topspace X ⊆ ⋃𝒱" if 𝒰: "∀U∈𝒰. openin X U" and sub_UU: "topspace X ⊆ ⋃𝒰" for 𝒰 proof - have "∃𝒱. finite 𝒱 ∧ 𝒱 ⊆ 𝒰 ∧ {x ∈ topspace X. f x = y} ⊆ ⋃𝒱" if "y ∈ topspace Y" for y proof (rule compactinD) show "compactin X {x ∈ topspace X. f x = y}" using f proper_map_def that by fastforce qed (use sub_UU 𝒰 in auto) then obtain 𝒱 where 𝒱: "⋀y. y ∈ topspace Y ⟹ finite (𝒱 y) ∧ 𝒱 y ⊆ 𝒰 ∧ {x ∈ topspace X. f x = y} ⊆ ⋃(𝒱 y)" by meson define 𝒲 where "𝒲 ≡ (λy. topspace Y - image f (topspace X - ⋃(𝒱 y))) ` topspace Y" have "∀U ∈ 𝒲. openin Y U" using f 𝒰 𝒱 unfolding 𝒲_def proper_map_def closed_map_def by (simp add: closedin_diff openin_Union openin_diff subset_iff) moreover have "topspace Y ⊆ ⋃𝒲" using 𝒱 unfolding 𝒲_def by clarsimp fastforce ultimately have "∃𝒱. countable 𝒱 ∧ 𝒱 ⊆ 𝒲 ∧ topspace Y ⊆ ⋃𝒱" using Y by (simp add: Lindelof_space_alt) then obtain I where "countable I" "I ⊆ topspace Y" and I: "topspace Y ⊆ (⋃i∈I. topspace Y - f ` (topspace X - ⋃(𝒱 i)))" unfolding 𝒲_def ex_countable_subset_image by metis show ?thesis proof (intro exI conjI) have "⋀i. i ∈ I ⟹ countable (𝒱 i)" by (meson 𝒱 ‹I ⊆ topspace Y› in_mono uncountable_infinite) with ‹countable I› show "countable (⋃(𝒱 ` I))" by auto show "⋃(𝒱 ` I) ⊆ 𝒰" using 𝒱 ‹I ⊆ topspace Y› by fastforce show "topspace X ⊆ ⋃(⋃(𝒱 ` I))" proof show "x ∈ ⋃ (⋃ (𝒱 ` I))" if "x ∈ topspace X" for x proof - have "f x ∈ topspace Y" by (meson f image_subset_iff proper_map_imp_subset_topspace that) then show ?thesis using that I by auto qed qed qed qed qed lemma Lindelof_space_perfect_map_image: "⟦Lindelof_space X; perfect_map X Y f⟧ ⟹ Lindelof_space Y" using Lindelof_space_quotient_map_image perfect_imp_quotient_map by blast lemma Lindelof_space_perfect_map_image_eq: "perfect_map X Y f ⟹ Lindelof_space X ⟷ Lindelof_space Y" using Lindelof_space_perfect_map_image Lindelof_space_proper_map_preimage perfect_map_def by blast end