Theory HOL-Analysis.Lindelof_Spaces

section‹Lindelöf 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_trivial_topology by force

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𝒰. Wg 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 {} (iI. {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  (iI. 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"
            using f proper_map_imp_subset_topspace that by fastforce
          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