Quelle  Lindelof_Spaces.thy

section‹Lindelöf spaces›

theory Lindelof_Spaces
imports T1_Spaces
begin

definition Lindelof_space where
  "Lindelof_space X ≡
        ∀U. (∀U ∈ U. openin X U) ∧ ∪U = topspace X
            ⟶ (∃V. countable V ∧ V ⊆ U ∧ ∪V = topspace X)"

lemma Lindelof_spaceD:
  "[Lindelof_space X; ∧U. U ∈ U ==> openin X U; ∪U = topspace X]
  ==> ∃V. countable V ∧ V ⊆ U ∧ ∪V = topspace X"
  by (auto simp: Lindelof_space_def)

lemma Lindelof_space_alt:
   "Lindelof_space X ⟷
        (∀U. (∀U ∈ U. openin X U) ∧ topspace X ⊆ ∪U
             ⟶ (∃V. countable V ∧ V ⊆ U ∧ topspace X ⊆ ∪V))"
  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 U: "countable U" and lin: "∧U. U ∈ U ==> Lindelof_space (subtopology X U)"
  shows "Lindelof_space (subtopology X (∪U))"
proof -
  have "∃V. countable V ∧ V ⊆ F ∧ ∪U ∩ ∪V = topspace X ∩ ∪U"
    if F: "F ⊆ Collect (openin X)" and UF: "∪U ∩ ∪F = topspace X ∩ ∪U"
    for F
  proof -
    have "∧U. [U ∈ U; U ∩ ∪F = topspace X ∩ U]
               ==> ∃V. countable V ∧ V ⊆ F ∧ U ∩ ∪V = topspace X ∩ U"
      using lin F
      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; U ∩ ∪F = topspace X ∩ U]
                               ==> countable (g U) ∧ (g U) ⊆ F ∧ U ∩ ∪(g U) = topspace X ∩ U"
      by metis
    show ?thesis
    proof (intro exI conjI)
      show "countable (∪(g ` U))"
        using Int_commute UF g  by (fastforce intro: countable_UN [OF U])
      show "∪(g ` U) ⊆ F"
        using g UF by blast
      show "∪U ∩ ∪(∪(g ` U)) = topspace X ∩ ∪U"
      proof
        show "∪U ∩ ∪(∪(g ` U)) ⊆ topspace X ∩ ∪U"
          using g UF by blast
        show "topspace X ∩ ∪U ⊆ ∪U ∩ ∪(∪(g ` U))"
        proof clarsimp
          show "∃y∈U. ∃W∈g y. x ∈ W"
            if "x ∈ topspace X" "x ∈ V" "V ∈ U" for x V
          proof -
            have "V ∩ ∪F = topspace X ∩ V"
              using UF ‹V ∈ U› by blast
            with that g [OF ‹V ∈ U›]  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. (∀U ∈ U. openin X U) ∧ topspace X ∩ S ⊆ ∪U
            ⟶ (∃V. countable V ∧ V ⊆ U ∧ topspace X ∩ S ⊆ ∪V))"
proof -
  have *: "(S ∩ ∪U = topspace X ∩ S) = (topspace X ∩ S ⊆ ∪U)"
    if "∧x. x ∈ U ==> openin X x" for U
    by (blast dest: openin_subset [OF that])
  moreover have "(V ⊆ U ∧ S ∩ ∪V = topspace X ∩ S) = (V ⊆ U ∧ topspace X ∩ S ⊆ ∪V)"
    if "∀x. x ∈ U ⟶ openin X x" "topspace X ∩ S ⊆ ∪U" "countable V" for U V
    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. (∀U ∈ U. openin X U) ∧ S ⊆ ∪U
                 ⟶ (∃V. countable V ∧ V ⊆ U ∧ 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 ⊆ F ∧ S ⊆ ∪V"
      if "∀U∈F. openin X U" and "S ⊆ ∪F" for F
    proof -
      have "∃V. countable V ∧ V ⊆ insert (topspace X - S) F ∧ ∪V = topspace X"
      proof (rule Lindelof_spaceD [OF X, of "insert (topspace X - S) F"])
        show "openin X U"
          if "U ∈ insert (topspace X - S) F" for U
          using that ‹∀U∈F. openin X U› clo by blast
        show "∪(insert (topspace X - S) F) = topspace X"
          apply auto
          apply (meson in_mono openin_closedin_eq that(1))
          using UnionE ‹S ⊆ ∪F› by auto
      qed
      then obtain V where "countable V" "V ⊆ insert (topspace X - S) F" "∪V = topspace X"
        by metis
      with ‹S ⊆ topspace X›
      show ?thesis
        by (rule_tac x="(V - {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 "∃V. countable V ∧ V ⊆ U ∧ ∪V = topspace Y"
    if U: "∧U. U ∈ U ==> openin Y U" and UU: "∪U = topspace Y" for U
  proof -
    define V where "V ≡ (λU. {x ∈ topspace X. f x ∈ U}) ` U"
    have "∧V. V ∈ V ==> openin X V"
      unfolding V_def using U continuous_map f by fastforce
    moreover have "∪V = topspace X"
      unfolding V_def using UU fim by fastforce
    ultimately have "∃W. countable W ∧ W ⊆ V ∧ ∪W = topspace X"
      using X by (simp add: Lindelof_space_def)
    then obtain C where "countable C" "C ⊆ U" and C: "(∪U∈C. {x ∈ topspace X. f x ∈ U}) = topspace X"
      by (metis (no_types, lifting) V_def countable_subset_image)
    moreover have "∪C = topspace Y"
    proof
      show "∪C ⊆ topspace Y"
        using UU C ‹C ⊆ U› by fastforce
      have "y ∈ ∪C" 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 C show ?thesis by auto
      qed
      then show "topspace Y ⊆ ∪C" 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 ⊆ ∪U" and fin: "locally_finite_in X U"
  shows "countable U"
proof -
  have UU_eq: "∪U = 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. 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. U ∩ T i ≠ {}}"
      using T
      by (meson ‹I ⊆ topspace X› in_mono uncountable_infinite)
    then show "countable (insert {} (∪i∈I. {U ∈ 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 "∃V. countable V ∧ V ⊆ U ∧ topspace X ⊆ ∪V"
    if U: "∀U∈U. openin X U" and sub_UU: "topspace X ⊆ ∪U" for U
  proof -
    have "∃V. finite V ∧ V ⊆ U ∧ {x ∈ topspace X. f x = y} ⊆ ∪V" 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 U in auto)
    then obtain V where V: "∧y. y ∈ topspace Y ==> finite (V y) ∧ V y ⊆ U ∧ {x ∈ topspace X. f x = y} ⊆ ∪(V y)"
      by meson
    define W where "W ≡ (λy. topspace Y - image f (topspace X - ∪(V y))) ` topspace Y"
    have "∀U ∈ W. openin Y U"
      using f U V unfolding W_def proper_map_def closed_map_def
      by (simp add: closedin_diff openin_Union openin_diff subset_iff)
    moreover have "topspace Y ⊆ ∪W"
      using V unfolding W_def by clarsimp fastforce
    ultimately have "∃V. countable V ∧ V ⊆ W ∧ topspace Y ⊆ ∪V"
      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 - ∪(V i)))"
      unfolding W_def ex_countable_subset_image by metis
    show ?thesis
    proof (intro exI conjI)
      have "∧i. i ∈ I ==> countable (V i)"
        by (meson V ‹I ⊆ topspace Y› in_mono uncountable_infinite)
      with ‹countable I› show "countable (∪(V ` I))"
        by auto
      show "∪(V ` I) ⊆ U"
        using V ‹I ⊆ topspace Y› by fastforce
      show "topspace X ⊆ ∪(∪(V ` I))"
      proof
        show "x ∈ ∪ (∪ (V ` 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