products/Sources/formale Sprachen/Isabelle/HOL/Data_Structures/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: TestResult.vdmrt   Sprache: Isabelle

Original von: Isabelle©
section\<open>Lindel\"of spaces\<close>

theory Lindelof_Spaces
imports T1_Spaces
begin

definition Lindelof_space where
  "Lindelof_space X \
        \<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> \<Union>\<U> = topspace X
            \<longrightarrow> (\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<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> \<U> \<and> \<Union>\<V> = topspace X"
  by (auto simp: Lindelof_space_def)

lemma Lindelof_space_alt:
   "Lindelof_space X \
        (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> topspace X \<subseteq> \<Union>\<U>
             \<longrightarrow> (\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<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_topspace_empty by blast

lemma Lindelof_space_Union:
  assumes \<U>: "countable \<U>" and lin: "\<And>U. U \<in> \<U> \<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>\<U> \<inter> \<Union>\<F> = topspace X \<inter> \<Union>\<U>"
    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 \<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 \<open>V \<in> \<U>\<close> by blast
            with that g [OF \<open>V \<in> \<U>\<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>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> topspace X \<inter> S \<subseteq> \<Union>\<U>
            \<longrightarrow> (\<exists>V. countable V \<and> V \<subseteq> \<U> \<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>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> S \<subseteq> \<Union>\<U>
                 \<longrightarrow> (\<exists>V. countable V \<and> V \<subseteq> \<U> \<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 \<U>: "\<And>U. U \<in> \<U> \<Longrightarrow> openin Y U" and UU: "\<Union>\<U> = topspace Y" for \<U>
  proof -
    define \<V> where "\<V> \<equiv> (\<lambda>U. {x \<in> topspace X. f x \<in> U}) ` \<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 \<C>" "\<C> \<subseteq> \<U>" 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> \<U>\<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 metis
  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 \<U>: "\<forall>U\<in>\<U>. openin X U" and sub_UU: "topspace X \<subseteq> \<Union>\<U>" 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>: "\<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)"
      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 \<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> \<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"
            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


¤ Dauer der Verarbeitung: 0.44 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff