# Theory Lindelof_Spaces

theory Lindelof_Spaces
imports T1_Spaces
```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"
then show ?thesis
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 ≠ {}}))"
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

```