author | desharna |
Thu, 24 Nov 2022 10:02:26 +0100 | |
changeset 76574 | 7bc934b99faf |
parent 76063 | 24c9f56aa035 |
child 78248 | 740b23f1138a |
permissions | -rw-r--r-- |
76063 | 1 |
section\<open>Lindelöf spaces\<close> |
70178
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
2 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
3 |
theory Lindelof_Spaces |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
4 |
imports T1_Spaces |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
5 |
begin |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
6 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
7 |
definition Lindelof_space where |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
8 |
"Lindelof_space X \<equiv> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
9 |
\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> \<Union>\<U> = topspace X |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
10 |
\<longrightarrow> (\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> \<Union>\<V> = topspace X)" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
11 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
12 |
lemma Lindelof_spaceD: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
13 |
"\<lbrakk>Lindelof_space X; \<And>U. U \<in> \<U> \<Longrightarrow> openin X U; \<Union>\<U> = topspace X\<rbrakk> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
14 |
\<Longrightarrow> \<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> \<Union>\<V> = topspace X" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
15 |
by (auto simp: Lindelof_space_def) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
16 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
17 |
lemma Lindelof_space_alt: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
18 |
"Lindelof_space X \<longleftrightarrow> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
19 |
(\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> topspace X \<subseteq> \<Union>\<U> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
20 |
\<longrightarrow> (\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<V>))" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
21 |
unfolding Lindelof_space_def |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
22 |
using openin_subset by fastforce |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
23 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
24 |
lemma compact_imp_Lindelof_space: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
25 |
"compact_space X \<Longrightarrow> Lindelof_space X" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
26 |
unfolding Lindelof_space_def compact_space |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
27 |
by (meson uncountable_infinite) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
28 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
29 |
lemma Lindelof_space_topspace_empty: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
30 |
"topspace X = {} \<Longrightarrow> Lindelof_space X" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
31 |
using compact_imp_Lindelof_space compact_space_topspace_empty by blast |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
32 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
33 |
lemma Lindelof_space_Union: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
34 |
assumes \<U>: "countable \<U>" and lin: "\<And>U. U \<in> \<U> \<Longrightarrow> Lindelof_space (subtopology X U)" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
35 |
shows "Lindelof_space (subtopology X (\<Union>\<U>))" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
36 |
proof - |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
37 |
have "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<F> \<and> \<Union>\<U> \<inter> \<Union>\<V> = topspace X \<inter> \<Union>\<U>" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
38 |
if \<F>: "\<F> \<subseteq> Collect (openin X)" and UF: "\<Union>\<U> \<inter> \<Union>\<F> = topspace X \<inter> \<Union>\<U>" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
39 |
for \<F> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
40 |
proof - |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
41 |
have "\<And>U. \<lbrakk>U \<in> \<U>; U \<inter> \<Union>\<F> = topspace X \<inter> U\<rbrakk> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
42 |
\<Longrightarrow> \<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<F> \<and> U \<inter> \<Union>\<V> = topspace X \<inter> U" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
43 |
using lin \<F> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
44 |
unfolding Lindelof_space_def openin_subtopology_alt Ball_def subset_iff [symmetric] |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
45 |
by (simp add: all_subset_image imp_conjL ex_countable_subset_image) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
46 |
then obtain g where g: "\<And>U. \<lbrakk>U \<in> \<U>; U \<inter> \<Union>\<F> = topspace X \<inter> U\<rbrakk> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
47 |
\<Longrightarrow> countable (g U) \<and> (g U) \<subseteq> \<F> \<and> U \<inter> \<Union>(g U) = topspace X \<inter> U" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
48 |
by metis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
49 |
show ?thesis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
50 |
proof (intro exI conjI) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
51 |
show "countable (\<Union>(g ` \<U>))" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
52 |
using Int_commute UF g by (fastforce intro: countable_UN [OF \<U>]) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
53 |
show "\<Union>(g ` \<U>) \<subseteq> \<F>" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
54 |
using g UF by blast |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
55 |
show "\<Union>\<U> \<inter> \<Union>(\<Union>(g ` \<U>)) = topspace X \<inter> \<Union>\<U>" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
56 |
proof |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
57 |
show "\<Union>\<U> \<inter> \<Union>(\<Union>(g ` \<U>)) \<subseteq> topspace X \<inter> \<Union>\<U>" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
58 |
using g UF by blast |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
59 |
show "topspace X \<inter> \<Union>\<U> \<subseteq> \<Union>\<U> \<inter> \<Union>(\<Union>(g ` \<U>))" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
60 |
proof clarsimp |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
61 |
show "\<exists>y\<in>\<U>. \<exists>W\<in>g y. x \<in> W" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
62 |
if "x \<in> topspace X" "x \<in> V" "V \<in> \<U>" for x V |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
63 |
proof - |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
64 |
have "V \<inter> \<Union>\<F> = topspace X \<inter> V" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
65 |
using UF \<open>V \<in> \<U>\<close> by blast |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
66 |
with that g [OF \<open>V \<in> \<U>\<close>] show ?thesis by blast |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
67 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
68 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
69 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
70 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
71 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
72 |
then show ?thesis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
73 |
unfolding Lindelof_space_def openin_subtopology_alt Ball_def subset_iff [symmetric] |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
74 |
by (simp add: all_subset_image imp_conjL ex_countable_subset_image) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
75 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
76 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
77 |
lemma countable_imp_Lindelof_space: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
78 |
assumes "countable(topspace X)" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
79 |
shows "Lindelof_space X" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
80 |
proof - |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
81 |
have "Lindelof_space (subtopology X (\<Union>x \<in> topspace X. {x}))" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
82 |
proof (rule Lindelof_space_Union) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
83 |
show "countable ((\<lambda>x. {x}) ` topspace X)" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
84 |
using assms by blast |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
85 |
show "Lindelof_space (subtopology X U)" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
86 |
if "U \<in> (\<lambda>x. {x}) ` topspace X" for U |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
87 |
proof - |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
88 |
have "compactin X U" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
89 |
using that by force |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
90 |
then show ?thesis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
91 |
by (meson compact_imp_Lindelof_space compact_space_subtopology) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
92 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
93 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
94 |
then show ?thesis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
95 |
by simp |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
96 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
97 |
lemma Lindelof_space_subtopology: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
98 |
"Lindelof_space(subtopology X S) \<longleftrightarrow> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
99 |
(\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> topspace X \<inter> S \<subseteq> \<Union>\<U> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
100 |
\<longrightarrow> (\<exists>V. countable V \<and> V \<subseteq> \<U> \<and> topspace X \<inter> S \<subseteq> \<Union>V))" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
101 |
proof - |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
102 |
have *: "(S \<inter> \<Union>\<U> = topspace X \<inter> S) = (topspace X \<inter> S \<subseteq> \<Union>\<U>)" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
103 |
if "\<And>x. x \<in> \<U> \<Longrightarrow> openin X x" for \<U> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
104 |
by (blast dest: openin_subset [OF that]) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
105 |
moreover have "(\<V> \<subseteq> \<U> \<and> S \<inter> \<Union>\<V> = topspace X \<inter> S) = (\<V> \<subseteq> \<U> \<and> topspace X \<inter> S \<subseteq> \<Union>\<V>)" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
106 |
if "\<forall>x. x \<in> \<U> \<longrightarrow> openin X x" "topspace X \<inter> S \<subseteq> \<Union>\<U>" "countable \<V>" for \<U> \<V> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
107 |
using that * by blast |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
108 |
ultimately show ?thesis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
109 |
unfolding Lindelof_space_def openin_subtopology_alt Ball_def |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
110 |
apply (simp add: all_subset_image imp_conjL ex_countable_subset_image flip: subset_iff) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
111 |
apply (intro all_cong1 imp_cong ex_cong, auto) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
112 |
done |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
113 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
114 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
115 |
lemma Lindelof_space_subtopology_subset: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
116 |
"S \<subseteq> topspace X |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
117 |
\<Longrightarrow> (Lindelof_space(subtopology X S) \<longleftrightarrow> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
118 |
(\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> S \<subseteq> \<Union>\<U> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
119 |
\<longrightarrow> (\<exists>V. countable V \<and> V \<subseteq> \<U> \<and> S \<subseteq> \<Union>V)))" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
120 |
by (metis Lindelof_space_subtopology topspace_subtopology topspace_subtopology_subset) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
121 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
122 |
lemma Lindelof_space_closedin_subtopology: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
123 |
assumes X: "Lindelof_space X" and clo: "closedin X S" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
124 |
shows "Lindelof_space (subtopology X S)" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
125 |
proof - |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
126 |
have "S \<subseteq> topspace X" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
127 |
by (simp add: clo closedin_subset) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
128 |
then show ?thesis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
129 |
proof (clarsimp simp add: Lindelof_space_subtopology_subset) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
130 |
show "\<exists>V. countable V \<and> V \<subseteq> \<F> \<and> S \<subseteq> \<Union>V" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
131 |
if "\<forall>U\<in>\<F>. openin X U" and "S \<subseteq> \<Union>\<F>" for \<F> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
132 |
proof - |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
133 |
have "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> insert (topspace X - S) \<F> \<and> \<Union>\<V> = topspace X" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
134 |
proof (rule Lindelof_spaceD [OF X, of "insert (topspace X - S) \<F>"]) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
135 |
show "openin X U" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
136 |
if "U \<in> insert (topspace X - S) \<F>" for U |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
137 |
using that \<open>\<forall>U\<in>\<F>. openin X U\<close> clo by blast |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
138 |
show "\<Union>(insert (topspace X - S) \<F>) = topspace X" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
139 |
apply auto |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
140 |
apply (meson in_mono openin_closedin_eq that(1)) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
141 |
using UnionE \<open>S \<subseteq> \<Union>\<F>\<close> by auto |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
142 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
143 |
then obtain \<V> where "countable \<V>" "\<V> \<subseteq> insert (topspace X - S) \<F>" "\<Union>\<V> = topspace X" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
144 |
by metis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
145 |
with \<open>S \<subseteq> topspace X\<close> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
146 |
show ?thesis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
147 |
by (rule_tac x="(\<V> - {topspace X - S})" in exI) auto |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
148 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
149 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
150 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
151 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
152 |
lemma Lindelof_space_continuous_map_image: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
153 |
assumes X: "Lindelof_space X" and f: "continuous_map X Y f" and fim: "f ` (topspace X) = topspace Y" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
154 |
shows "Lindelof_space Y" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
155 |
proof - |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
156 |
have "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> \<Union>\<V> = topspace Y" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
157 |
if \<U>: "\<And>U. U \<in> \<U> \<Longrightarrow> openin Y U" and UU: "\<Union>\<U> = topspace Y" for \<U> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
158 |
proof - |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
159 |
define \<V> where "\<V> \<equiv> (\<lambda>U. {x \<in> topspace X. f x \<in> U}) ` \<U>" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
160 |
have "\<And>V. V \<in> \<V> \<Longrightarrow> openin X V" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
161 |
unfolding \<V>_def using \<U> continuous_map f by fastforce |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
162 |
moreover have "\<Union>\<V> = topspace X" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
163 |
unfolding \<V>_def using UU fim by fastforce |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
164 |
ultimately have "\<exists>\<W>. countable \<W> \<and> \<W> \<subseteq> \<V> \<and> \<Union>\<W> = topspace X" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
165 |
using X by (simp add: Lindelof_space_def) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
166 |
then obtain \<C> where "countable \<C>" "\<C> \<subseteq> \<U>" and \<C>: "(\<Union>U\<in>\<C>. {x \<in> topspace X. f x \<in> U}) = topspace X" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
167 |
by (metis (no_types, lifting) \<V>_def countable_subset_image) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
168 |
moreover have "\<Union>\<C> = topspace Y" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
169 |
proof |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
170 |
show "\<Union>\<C> \<subseteq> topspace Y" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
171 |
using UU \<C> \<open>\<C> \<subseteq> \<U>\<close> by fastforce |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
172 |
have "y \<in> \<Union>\<C>" if "y \<in> topspace Y" for y |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
173 |
proof - |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
174 |
obtain x where "x \<in> topspace X" "y = f x" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
175 |
using that fim by (metis \<open>y \<in> topspace Y\<close> imageE) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
176 |
with \<C> show ?thesis by auto |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
177 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
178 |
then show "topspace Y \<subseteq> \<Union>\<C>" by blast |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
179 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
180 |
ultimately show ?thesis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
181 |
by blast |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
182 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
183 |
then show ?thesis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
184 |
unfolding Lindelof_space_def |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
185 |
by auto |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
186 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
187 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
188 |
lemma Lindelof_space_quotient_map_image: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
189 |
"\<lbrakk>quotient_map X Y q; Lindelof_space X\<rbrakk> \<Longrightarrow> Lindelof_space Y" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
190 |
by (meson Lindelof_space_continuous_map_image quotient_imp_continuous_map quotient_imp_surjective_map) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
191 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
192 |
lemma Lindelof_space_retraction_map_image: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
193 |
"\<lbrakk>retraction_map X Y r; Lindelof_space X\<rbrakk> \<Longrightarrow> Lindelof_space Y" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
194 |
using Abstract_Topology.retraction_imp_quotient_map Lindelof_space_quotient_map_image by blast |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
195 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
196 |
lemma locally_finite_cover_of_Lindelof_space: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
197 |
assumes X: "Lindelof_space X" and UU: "topspace X \<subseteq> \<Union>\<U>" and fin: "locally_finite_in X \<U>" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
198 |
shows "countable \<U>" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
199 |
proof - |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
200 |
have UU_eq: "\<Union>\<U> = topspace X" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
201 |
by (meson UU fin locally_finite_in_def subset_antisym) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
202 |
obtain T where T: "\<And>x. x \<in> topspace X \<Longrightarrow> openin X (T x) \<and> x \<in> T x \<and> finite {U \<in> \<U>. U \<inter> T x \<noteq> {}}" |
73005
83b114a6545f
A few more simprules for iff-reasoning
paulson <lp15@cam.ac.uk>
parents:
71031
diff
changeset
|
203 |
using fin unfolding locally_finite_in_def by metis |
70178
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
204 |
then obtain I where "countable I" "I \<subseteq> topspace X" and I: "topspace X \<subseteq> \<Union>(T ` I)" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
205 |
using X unfolding Lindelof_space_alt |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
206 |
by (drule_tac x="image T (topspace X)" in spec) (auto simp: ex_countable_subset_image) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
207 |
show ?thesis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
208 |
proof (rule countable_subset) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
209 |
have "\<And>i. i \<in> I \<Longrightarrow> countable {U \<in> \<U>. U \<inter> T i \<noteq> {}}" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
210 |
using T |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
211 |
by (meson \<open>I \<subseteq> topspace X\<close> in_mono uncountable_infinite) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
212 |
then show "countable (insert {} (\<Union>i\<in>I. {U \<in> \<U>. U \<inter> T i \<noteq> {}}))" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
213 |
by (simp add: \<open>countable I\<close>) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
214 |
qed (use UU_eq I in auto) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
215 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
216 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
217 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
218 |
lemma Lindelof_space_proper_map_preimage: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
219 |
assumes f: "proper_map X Y f" and Y: "Lindelof_space Y" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
220 |
shows "Lindelof_space X" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
221 |
proof (clarsimp simp: Lindelof_space_alt) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
222 |
show "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<V>" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
223 |
if \<U>: "\<forall>U\<in>\<U>. openin X U" and sub_UU: "topspace X \<subseteq> \<Union>\<U>" for \<U> |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
224 |
proof - |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
225 |
have "\<exists>\<V>. finite \<V> \<and> \<V> \<subseteq> \<U> \<and> {x \<in> topspace X. f x = y} \<subseteq> \<Union>\<V>" if "y \<in> topspace Y" for y |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
226 |
proof (rule compactinD) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
227 |
show "compactin X {x \<in> topspace X. f x = y}" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
228 |
using f proper_map_def that by fastforce |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
229 |
qed (use sub_UU \<U> in auto) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
230 |
then obtain \<V> where \<V>: "\<And>y. y \<in> topspace Y \<Longrightarrow> finite (\<V> y) \<and> \<V> y \<subseteq> \<U> \<and> {x \<in> topspace X. f x = y} \<subseteq> \<Union>(\<V> y)" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
231 |
by meson |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
232 |
define \<W> where "\<W> \<equiv> (\<lambda>y. topspace Y - image f (topspace X - \<Union>(\<V> y))) ` topspace Y" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
233 |
have "\<forall>U \<in> \<W>. openin Y U" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
234 |
using f \<U> \<V> unfolding \<W>_def proper_map_def closed_map_def |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
235 |
by (simp add: closedin_diff openin_Union openin_diff subset_iff) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
236 |
moreover have "topspace Y \<subseteq> \<Union>\<W>" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
237 |
using \<V> unfolding \<W>_def by clarsimp fastforce |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
238 |
ultimately have "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<W> \<and> topspace Y \<subseteq> \<Union>\<V>" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
239 |
using Y by (simp add: Lindelof_space_alt) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
240 |
then obtain I where "countable I" "I \<subseteq> topspace Y" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
241 |
and I: "topspace Y \<subseteq> (\<Union>i\<in>I. topspace Y - f ` (topspace X - \<Union>(\<V> i)))" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
242 |
unfolding \<W>_def ex_countable_subset_image by metis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
243 |
show ?thesis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
244 |
proof (intro exI conjI) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
245 |
have "\<And>i. i \<in> I \<Longrightarrow> countable (\<V> i)" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
246 |
by (meson \<V> \<open>I \<subseteq> topspace Y\<close> in_mono uncountable_infinite) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
247 |
with \<open>countable I\<close> show "countable (\<Union>(\<V> ` I))" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
248 |
by auto |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
249 |
show "\<Union>(\<V> ` I) \<subseteq> \<U>" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
250 |
using \<V> \<open>I \<subseteq> topspace Y\<close> by fastforce |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
251 |
show "topspace X \<subseteq> \<Union>(\<Union>(\<V> ` I))" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
252 |
proof |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
253 |
show "x \<in> \<Union> (\<Union> (\<V> ` I))" if "x \<in> topspace X" for x |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
254 |
proof - |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
255 |
have "f x \<in> topspace Y" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
256 |
by (meson f image_subset_iff proper_map_imp_subset_topspace that) |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
257 |
then show ?thesis |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
258 |
using that I by auto |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
259 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
260 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
261 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
262 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
263 |
qed |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
264 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
265 |
lemma Lindelof_space_perfect_map_image: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
266 |
"\<lbrakk>Lindelof_space X; perfect_map X Y f\<rbrakk> \<Longrightarrow> Lindelof_space Y" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
267 |
using Lindelof_space_quotient_map_image perfect_imp_quotient_map by blast |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
268 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
269 |
lemma Lindelof_space_perfect_map_image_eq: |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
270 |
"perfect_map X Y f \<Longrightarrow> Lindelof_space X \<longleftrightarrow> Lindelof_space Y" |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
271 |
using Lindelof_space_perfect_map_image Lindelof_space_proper_map_preimage perfect_map_def by blast |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
272 |
|
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
273 |
end |
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
274 |