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 \ \ \ openin X 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 \" and lin:
"\U. U \ \ \ Lindelof_space (subtopology X U)"
shows "Lindelof_space (subtopology X (\\))"
proof -
have "\\. countable \ \ \ \ \ \ \\ \ \\ = topspace X \ \\"
if F:
"\ \ Collect (openin X)" and UF:
"\\ \ \\ = topspace X \ \\"
for F
proof -
have "\U. \U \ \; U \ \\ = 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 \ \\ = 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 ` \))"
using Int_commute UF g
by (fastforce intro: countable_UN [OF
U])
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
∈ 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 \ \\ = topspace X \ S) = (topspace X \ S \ \\)"
if "\x. x \ \ \ openin X x" for U
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 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_subse
t)
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 F
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∈F. 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 ⊆ ∪F› by auto
qed
then obtain V 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. U \ \ \ openin Y U" and UU: "\\ = topspace Y" for U
proof -
define V where "\ \ (\U. {x \ topspace X. f x \ U}) ` \"
have "\V. V \ \ \ openin X V"
unfolding V_def using U continuous_map f by fastforce
moreover have "\\ = topspace X"
unfolding V_def using UU fim by fastforce
ultimately have "\\. countable \ \ \ \ \ \ \\ = topspace X"
using X by (simp add: Lindelof_space_def)
then obtain C where "countable \" "\ \ \" and C: "(\U\\. {x \ topspace X. f x \ U}) = topspace X"
by (metis (no_types, lifting) V_def countable_subset_image)
moreover have "\\ = topspace Y"
proof
show "\\ \ topspace Y"
using UU C ‹C ⊆ U› 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 C 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: "\U\\. openin X U" and sub_UU: "topspace X \ \\" for U
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 U in auto)
then obtain V where V: "\y. y \ topspace Y \ finite (\ y) \ \ y \ \ \ {x \ topspace X. f x = y} \ \(\ y)"
by meson
define W where "\ \ (\y. topspace Y - image f (topspace X - \(\ y))) ` topspace Y"
have "\U \ \. 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 \ \\"
using V unfolding W_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 W_def ex_countable_subset_image by metis
show ?thesis
proof (intro exI conjI)
have "\i. i \ I \ countable (\ i)"
by (meson V ‹I ⊆ topspace Y› in_mono uncountable_infinite)
with ‹countable I› show "countable (\(\ ` I))"
by auto
show "\(\ ` I) \ \"
using V ‹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
