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∈𝒰. ∃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"
            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