Quelle Lindelof_Spaces.thy Sprache: Isabelle

section\<open>Lindelöf spaces\<close>

theory Lindelof_Spaces
imports T1_Spaces
begin

definition Lindelof_space where
 "Lindelof_space X \
 \<forall>\. (\<forall>U \<in> \. openin X U) \<and> \<Union>\ = topspace X
 \<longrightarrow> (\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \ \<and> \<Union>\<V> = topspace X)"

lemma Lindelof_spaceD:
 "\Lindelof_space X; \U. U \ \ \ openin X U; \\ = topspace X\
 \<Longrightarrow> \<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \ \<and> \<Union>\<V> = topspace X"
 by (auto simp: Lindelof_space_def)

lemma Lindelof_space_alt:
 "Lindelof_space X \
 (\<forall>\. (\<forall>U \<in> \. openin X U) \<and> topspace X \<subseteq> \<Union>\
 \<longrightarrow> (\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \ \<and> topspace X \<subseteq> \<Union>\<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 \: "countable \" and lin: "\<And>U. U \<in> \ \<Longrightarrow> Lindelof_space (subtopology X U)"
 shows "Lindelof_space (subtopology X (\\))"
proof -
 have "\\. countable \ \ \ \ \ \ \\ \ \\ = topspace X \ \\"
 if \<F>: "\<F> \<subseteq> Collect (openin X)" and UF: "\<Union>\ \<inter> \<Union>\<F> = topspace X \<inter> \<Union>\"
 for \<F>
 proof -
 have "\U. \U \ \; U \ \\ = topspace X \ U\
 \<Longrightarrow> \<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<F> \<and> U \<inter> \<Union>\<V> = topspace X \<inter> 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\
 \<Longrightarrow> countable (g U) \<and> (g U) \<subseteq> \<F> \<and> U \<inter> \<Union>(g U) = topspace X \<inter> 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 \<open>V \<in> \\<close> by blast
 with that g [OF \<open>V \<in> \\<close>] 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) \
 (\<forall>\. (\<forall>U \<in> \. openin X U) \<and> topspace X \<inter> S \<subseteq> \<Union>\
 \<longrightarrow> (\<exists>V. countable V \<and> V \<subseteq> \ \<and> topspace X \<inter> S \<subseteq> \<Union>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
 \<Longrightarrow> (Lindelof_space(subtopology X S) \<longleftrightarrow>
 (\<forall>\. (\<forall>U \<in> \. openin X U) \<and> S \<subseteq> \<Union>\
 \<longrightarrow> (\<exists>V. countable V \<and> V \<subseteq> \ \<and> S \<subseteq> \<Union>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 \<open>\<forall>U\<in>\<F>. openin X U\<close> clo by blast
 show "\(insert (topspace X - S) \) = topspace X"
 apply auto
 apply (meson in_mono openin_closedin_eq that(1))
 using UnionE \<open>S \<subseteq> \<Union>\<F>\<close> by auto
 qed
 then obtain \<V> where "countable \<V>" "\<V> \<subseteq> insert (topspace X - S) \<F>" "\<Union>\<V> = topspace X"
 by metis
 with \<open>S \<subseteq> topspace X\<close>
 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 \: "\<And>U. U \<in> \ \<Longrightarrow> openin Y U" and UU: "\<Union>\ = topspace Y" for \
 proof -
 define \<V> where "\<V> \<equiv> (\<lambda>U. {x \<in> topspace X. f x \<in> U}) ` \"
 have "\V. V \ \ \ openin X V"
 unfolding \<V>_def using \ 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 \<C>" "\<C> \<subseteq> \" and \<C>: "(\<Union>U\<in>\<C>. {x \<in> topspace X. f x \<in> U}) = topspace X"
 by (metis (no_types, lifting) \<V>_def countable_subset_image)
 moreover have "\\ = topspace Y"
 proof
 show "\\ \ topspace Y"
 using UU \<C> \<open>\<C> \<subseteq> \\<close> 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 \<open>y \<in> topspace Y\<close> 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 \<open>I \<subseteq> topspace X\<close> in_mono uncountable_infinite)
 then show "countable (insert {} (\i\I. {U \ \. U \ T i \ {}}))"
 by (simp add: \<open>countable I\<close>)
 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 \: "\<forall>U\<in>\. openin X U" and sub_UU: "topspace X \<subseteq> \<Union>\" 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 \<V> where \<V>: "\<And>y. y \<in> topspace Y \<Longrightarrow> finite (\<V> y) \<and> \<V> y \<subseteq> \ \<and> {x \<in> topspace X. f x = y} \<subseteq> \<Union>(\<V> y)"
 by meson
 define \<W> where "\<W> \<equiv> (\<lambda>y. topspace Y - image f (topspace X - \<Union>(\<V> y))) ` topspace Y"
 have "\U \ \. openin Y U"
 using f \ \<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> \<open>I \<subseteq> topspace Y\<close> in_mono uncountable_infinite)
 with \<open>countable I\<close> show "countable (\<Union>(\<V> ` I))"
 by auto
 show "\(\ ` I) \ \"
 using \<V> \<open>I \<subseteq> topspace Y\<close> 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

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.