Quellcode-Bibliothek T1_Spaces.thy Sprache: Isabelle

section\<open>T1 and Hausdorff spaces\<close>

theory T1_Spaces
imports Product_Topology
begin

section\<open>T1 spaces with equivalences to many naturally "nice" properties. \<close>

definition t1_space where
"t1_space X \ \x \ topspace X. \y \ topspace X. x\y \ (\U. openin X U \ x \ U \ y \ U)"

lemma t1_space_expansive:
   "\topspace Y = topspace X; \U. openin X U \ openin Y U\ \ t1_space X \ t1_space Y"
  by (metis t1_space_def)

lemma t1_space_alt:
   "t1_space X \ (\x \ topspace X. \y \ topspace X. x\y \ (\U. closedin X U \ x \ U \ y \ U))"
by (metis DiffE DiffI closedin_def openin_closedin_eq t1_space_def)

lemma t1_space_empty [iff]: "t1_space trivial_topology"
  by (simp add: t1_space_def)

lemma t1_space_derived_set_of_singleton:
  "t1_space X \ (\x \ topspace X. X derived_set_of {x} = {})"
  apply (simp add: t1_space_def derived_set_of_def, safe)
   apply (metis openin_topspace)
  by force

lemma t1_space_derived_set_of_finite:
   "t1_space X \ (\S. finite S \ X derived_set_of S = {})"
proof (intro iffI allI impI)
  fix S :: "'a set"
  assume "finite S"
  then have fin: "finite ((\x. {x}) ` (topspace X \ S))"
    by blast
  assume "t1_space X"
  then have "X derived_set_of (\x \ topspace X \ S. {x}) = {}"
    unfolding derived_set_of_Union [OF fin]
    by (auto simp: t1_space_derived_set_of_singleton)
  then have "X derived_set_of (topspace X \ S) = {}"
    by simp
  then show "X derived_set_of S = {}"
    by simp
qed (auto simp: t1_space_derived_set_of_singleton)

lemma t1_space_closedin_singleton:
   "t1_space X \ (\x \ topspace X. closedin X {x})"
  apply (rule iffI)
  apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_singleton)
  using t1_space_alt by auto

lemma continuous_closed_imp_proper_map:
   "\compact_space X; t1_space Y; continuous_map X Y f; closed_map X Y f\ \ proper_map X Y f"
  unfolding proper_map_def
  by (smt (verit) closedin_compact_space closedin_continuous_map_preimage
      Collect_cong singleton_iff t1_space_closedin_singleton)

lemma t1_space_euclidean: "t1_space (euclidean :: 'a::metric_space topology)"
  by (simp add: t1_space_closedin_singleton)

lemma closedin_t1_singleton:
   "\t1_space X; a \ topspace X\ \ closedin X {a}"
  by (simp add: t1_space_closedin_singleton)

lemma t1_space_closedin_finite:
   "t1_space X \ (\S. finite S \ S \ topspace X \ closedin X S)"
  apply (rule iffI)
  apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_finite)
  by (simp add: t1_space_closedin_singleton)

lemma closure_of_singleton:
   "t1_space X \ X closure_of {a} = (if a \ topspace X then {a} else {})"
  by (simp add: closure_of_eq t1_space_closedin_singleton closure_of_eq_empty_gen)

lemma separated_in_singleton:
  assumes "t1_space X"
  shows "separatedin X {a} S \ a \ topspace X \ S \ topspace X \ (a \ X closure_of S)"
        "separatedin X S {a} \ a \ topspace X \ S \ topspace X \ (a \ X closure_of S)"
  unfolding separatedin_def
  using assms closure_of closure_of_singleton by fastforce+

lemma t1_space_openin_delete:
   "t1_space X \ (\U x. openin X U \ x \ U \ openin X (U - {x}))"
  apply (rule iffI)
  apply (meson closedin_t1_singleton in_mono openin_diff openin_subset)
  by (simp add: closedin_def t1_space_closedin_singleton)

lemma t1_space_openin_delete_alt:
   "t1_space X \ (\U x. openin X U \ openin X (U - {x}))"
  by (metis Diff_empty Diff_insert0 t1_space_openin_delete)

lemma t1_space_singleton_Inter_open:
      "t1_space X \ (\x \ topspace X. \{U. openin X U \ x \ U} = {x})" (is "?P=?Q")
  and t1_space_Inter_open_supersets:
     "t1_space X \ (\S. S \ topspace X \ \{U. openin X U \ S \ U} = S)" (is "?P=?R")
proof -
  have "?R \ ?Q"
    apply clarify
    apply (drule_tac x="{x}" in spec, simp)
    done
  moreover have "?Q \ ?P"
    apply (clarsimp simp add: t1_space_def)
    apply (drule_tac x=x in bspec)
     apply (simp_all add: set_eq_iff)
    by (metis (no_types, lifting))
  moreover have "?P \ ?R"
  proof (clarsimp simp add: t1_space_closedin_singleton, rule subset_antisym)
    fix S
    assume S: "\x\topspace X. closedin X {x}" "S \ topspace X"
    then show "\ {U. openin X U \ S \ U} \ S"
      apply clarsimp
      by (metis Diff_insert_absorb Set.set_insert closedin_def openin_topspace subset_insert)
  qed force
  ultimately show "?P=?Q" "?P=?R"
    by auto
qed

lemma t1_space_derived_set_of_infinite_openin:
   "t1_space X \
        (\<forall>S. X derived_set_of S =
             {x \<in> topspace X. \<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite(S \<inter> U)})"
         (is "_ = ?rhs")
proof
  assume "t1_space X"
  show ?rhs
  proof safe
    fix S x U
    assume "x \ X derived_set_of S" "x \ U" "openin X U" "finite (S \ U)"
    with \<open>t1_space X\<close> show "False"
      apply (simp add: t1_space_derived_set_of_finite)
      by (metis IntI empty_iff empty_subsetI inf_commute openin_Int_derived_set_of_subset subset_antisym)
  next
    fix S x
    have eq: "(\y. (y \ x) \ y \ S \ y \ T) \ ~((S \ T) \ {x})" for x S T
      by blast
    assume "x \ topspace X" "\U. x \ U \ openin X U \ infinite (S \ U)"
    then show "x \ X derived_set_of S"
      apply (clarsimp simp add: derived_set_of_def eq)
      by (meson finite.emptyI finite.insertI finite_subset)
  qed (auto simp: in_derived_set_of)
qed (auto simp: t1_space_derived_set_of_singleton)

lemma finite_t1_space_imp_discrete_topology:
   "\topspace X = U; finite U; t1_space X\ \ X = discrete_topology U"
  by (metis discrete_topology_unique_derived_set t1_space_derived_set_of_finite)

lemma t1_space_subtopology: "t1_space X \ t1_space(subtopology X U)"
  by (simp add: derived_set_of_subtopology t1_space_derived_set_of_finite)

lemma closedin_derived_set_of_gen:
   "t1_space X \ closedin X (X derived_set_of S)"
  apply (clarsimp simp add: in_derived_set_of closedin_contains_derived_set derived_set_of_subset_topspace)
  by (metis DiffD2 insert_Diff insert_iff t1_space_openin_delete)

lemma derived_set_of_derived_set_subset_gen:
   "t1_space X \ X derived_set_of (X derived_set_of S) \ X derived_set_of S"
  by (meson closedin_contains_derived_set closedin_derived_set_of_gen)

lemma subtopology_eq_discrete_topology_gen_finite:
   "\t1_space X; finite S\ \ subtopology X S = discrete_topology(topspace X \ S)"
  by (simp add: subtopology_eq_discrete_topology_gen t1_space_derived_set_of_finite)

lemma subtopology_eq_discrete_topology_finite:
   "\t1_space X; S \ topspace X; finite S\
        \<Longrightarrow> subtopology X S = discrete_topology S"
  by (simp add: subtopology_eq_discrete_topology_eq t1_space_derived_set_of_finite)

lemma t1_space_closed_map_image:
   "\closed_map X Y f; f ` (topspace X) = topspace Y; t1_space X\ \ t1_space Y"
  by (metis closed_map_def finite_subset_image t1_space_closedin_finite)

lemma homeomorphic_t1_space: "X homeomorphic_space Y \ (t1_space X \ t1_space Y)"
  apply (clarsimp simp add: homeomorphic_space_def)
  by (meson homeomorphic_eq_everything_map homeomorphic_maps_map t1_space_closed_map_image)

proposition t1_space_product_topology:
   "t1_space (product_topology X I)
\<longleftrightarrow> (product_topology X I) = trivial_topology \<or> (\<forall>i \<in> I. t1_space (X i))"
proof (cases "(product_topology X I) = trivial_topology")
  case True
  then show ?thesis
    using True t1_space_empty by force
next
  case False
  then obtain f where f: "f \ (\\<^sub>E i\I. topspace(X i))"
    using discrete_topology_unique by (fastforce iff: null_topspace_iff_trivial)
  have "t1_space (product_topology X I) \ (\i\I. t1_space (X i))"
  proof (intro iffI ballI)
    show "t1_space (X i)" if "t1_space (product_topology X I)" and "i \ I" for i
    proof -
      have clo: "\h. h \ (\\<^sub>E i\I. topspace (X i)) \ closedin (product_topology X I) {h}"
        using that by (simp add: t1_space_closedin_singleton)
      show ?thesis
        unfolding t1_space_closedin_singleton
      proof clarify
        show "closedin (X i) {xi}" if "xi \ topspace (X i)" for xi
          using clo [of "\j \ I. if i=j then xi else f j"] f that \i \ I\
          by (fastforce simp add: closedin_product_topology_singleton)
      qed
    qed
  next
  next
    show "t1_space (product_topology X I)" if "\i\I. t1_space (X i)"
      using that
      by (simp add: t1_space_closedin_singleton Ball_def PiE_iff closedin_product_topology_singleton)
  qed
  then show ?thesis
    using False by blast
qed

lemma t1_space_prod_topology:
   "t1_space(prod_topology X Y) \ (prod_topology X Y) = trivial_topology \ t1_space X \ t1_space Y"
proof (cases "(prod_topology X Y) = trivial_topology")
  case True then show ?thesis
  by auto
next
  case False
  have eq: "{(x,y)} = {x} \ {y}" for x::'a and y::'b
    by simp
  have "t1_space (prod_topology X Y) \ (t1_space X \ t1_space Y)"
    using False
    apply(simp add: t1_space_closedin_singleton closedin_prod_Times_iff eq
               del: insert_Times_insert flip: null_topspace_iff_trivial ex_in_conv)
    by blast
  with False show ?thesis
    by simp
qed

subsection\<open>Hausdorff Spaces\<close>

definition Hausdorff_space
  where
"Hausdorff_space X \
        \<forall>x y. x \<in> topspace X \<and> y \<in> topspace X \<and> (x \<noteq> y)
              \<longrightarrow> (\<exists>U V. openin X U \<and> openin X V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V)"

lemma Hausdorff_space_expansive:
   "\Hausdorff_space X; topspace X = topspace Y; \U. openin X U \ openin Y U\ \ Hausdorff_space Y"
  by (metis Hausdorff_space_def)

lemma Hausdorff_space_topspace_empty [iff]: "Hausdorff_space trivial_topology"
  by (simp add: Hausdorff_space_def)

lemma Hausdorff_imp_t1_space:
   "Hausdorff_space X \ t1_space X"
  by (metis Hausdorff_space_def disjnt_iff t1_space_def)

lemma closedin_derived_set_of:
   "Hausdorff_space X \ closedin X (X derived_set_of S)"
  by (simp add: Hausdorff_imp_t1_space closedin_derived_set_of_gen)

lemma t1_or_Hausdorff_space:
   "t1_space X \ Hausdorff_space X \ t1_space X"
  using Hausdorff_imp_t1_space by blast

lemma Hausdorff_space_sing_Inter_opens:
   "\Hausdorff_space X; a \ topspace X\ \ \{u. openin X u \ a \ u} = {a}"
  using Hausdorff_imp_t1_space t1_space_singleton_Inter_open by force

lemma Hausdorff_space_subtopology:
  assumes "Hausdorff_space X" shows "Hausdorff_space(subtopology X S)"
proof -
  have *: "disjnt U V \ disjnt (S \ U) (S \ V)" for U V
    by (simp add: disjnt_iff)
  from assms show ?thesis
    apply (simp add: Hausdorff_space_def openin_subtopology_alt)
    apply (fast intro: * elim!: all_forward)
    done
qed

lemma Hausdorff_space_compact_separation:
  assumes X: "Hausdorff_space X" and S: "compactin X S" and T: "compactin X T" and "disjnt S T"
  obtains U V where "openin X U" "openin X V" "S \ U" "T \ V" "disjnt U V"
proof (cases "S = {}")
  case True
  then show thesis
    by (metis \<open>compactin X T\<close> compactin_subset_topspace disjnt_empty1 empty_subsetI openin_empty openin_topspace that)
next
  case False
  have "\x \ S. \U V. openin X U \ openin X V \ x \ U \ T \ V \ disjnt U V"
  proof
    fix a
    assume "a \ S"
    then have "a \ T"
      by (meson assms(4) disjnt_iff)
    have a: "a \ topspace X"
      using S \<open>a \<in> S\<close> compactin_subset_topspace by blast
    show "\U V. openin X U \ openin X V \ a \ U \ T \ V \ disjnt U V"
    proof (cases "T = {}")
      case True
      then show ?thesis
        using a disjnt_empty2 openin_empty by blast
    next
      case False
      have "\x \ topspace X - {a}. \U V. openin X U \ openin X V \ x \ U \ a \ V \ disjnt U V"
        using X a by (simp add: Hausdorff_space_def)
      then obtain U V where UV: "\x \ topspace X - {a}. openin X (U x) \ openin X (V x) \ x \ U x \ a \ V x \ disjnt (U x) (V x)"
        by metis
      with \<open>a \<notin> T\<close> compactin_subset_topspace [OF T]
      have Topen: "\W \ U ` T. openin X W" and Tsub: "T \ \ (U ` T)"
        by auto
      then obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> U ` T" and "T \<subseteq> \<Union>\<F>"
        using T unfolding compactin_def by meson
      then obtain F where F: "finite F" "F \ T" "\ = U ` F" and SUF: "T \ \(U ` F)" and "a \ F"
        using finite_subset_image [OF \<F>] \<open>a \<notin> T\<close> by (metis subsetD)
      have U: "\x. \x \ topspace X; x \ a\ \ openin X (U x)"
        and V: "\x. \x \ topspace X; x \ a\ \ openin X (V x)"
        and disj: "\x. \x \ topspace X; x \ a\ \ disjnt (U x) (V x)"
        using UV by blast+
      show ?thesis
      proof (intro exI conjI)
        have "F \ {}"
          using False SUF by blast
        with \<open>a \<notin> F\<close> show "openin X (\<Inter>(V ` F))"
          using F compactin_subset_topspace [OF T] by (force intro: V)
        show "openin X (\(U ` F))"
          using F Topen Tsub by (force intro: U)
        show "disjnt (\(V ` F)) (\(U ` F))"
          using disj
          apply (auto simp: disjnt_def)
          using \<open>F \<subseteq> T\<close> \<open>a \<notin> F\<close> compactin_subset_topspace [OF T] by blast
        show "a \ (\(V ` F))"
          using \<open>F \<subseteq> T\<close> T UV \<open>a \<notin> T\<close> compactin_subset_topspace by blast
      qed (auto simp: SUF)
    qed
  qed
  then obtain U V where UV: "\x \ S. openin X (U x) \ openin X (V x) \ x \ U x \ T \ V x \ disjnt (U x) (V x)"
    by metis
  then have "S \ \ (U ` S)"
    by auto
  moreover have "\W \ U ` S. openin X W"
    using UV by blast
  ultimately obtain I where I: "S \ \ (U ` I)" "I \ S" "finite I"
    by (metis S compactin_def finite_subset_image)
  show thesis
  proof
    show "openin X (\(U ` I))"
      using \<open>I \<subseteq> S\<close> UV by blast
    show "openin X (\ (V ` I))"
      using False UV \<open>I \<subseteq> S\<close> \<open>S \<subseteq> \<Union> (U ` I)\<close> \<open>finite I\<close> by blast
    show "disjnt (\(U ` I)) (\ (V ` I))"
      by simp (meson UV \<open>I \<subseteq> S\<close> disjnt_subset2 in_mono le_INF_iff order_refl)
  qed (use UV I in auto)
qed

lemma Hausdorff_space_compact_sets:
  "Hausdorff_space X \
    (\<forall>S T. compactin X S \<and> compactin X T \<and> disjnt S T
           \<longrightarrow> (\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V))"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (meson Hausdorff_space_compact_separation)
next
  assume R [rule_format]: ?rhs
  show ?lhs
  proof (clarsimp simp add: Hausdorff_space_def)
    fix x y
    assume "x \ topspace X" "y \ topspace X" "x \ y"
    then show "\U. openin X U \ (\V. openin X V \ x \ U \ y \ V \ disjnt U V)"
      using R [of "{x}" "{y}"] by auto
  qed
qed

lemma compactin_imp_closedin:
  assumes X: "Hausdorff_space X" and S: "compactin X S" shows "closedin X S"
proof -
  have "S \ topspace X"
    by (simp add: assms compactin_subset_topspace)
  moreover
  have "\T. openin X T \ x \ T \ T \ topspace X - S" if "x \ topspace X" "x \ S" for x
    using Hausdorff_space_compact_separation [OF X _ S, of "{x}"] that
    apply (simp add: disjnt_def)
    by (metis Diff_mono Diff_triv openin_subset)
  ultimately show ?thesis
    using closedin_def openin_subopen by force
qed

lemma closedin_Hausdorff_singleton:
   "\Hausdorff_space X; x \ topspace X\ \ closedin X {x}"
  by (simp add: Hausdorff_imp_t1_space closedin_t1_singleton)

lemma closedin_Hausdorff_sing_eq:
   "Hausdorff_space X \ closedin X {x} \ x \ topspace X"
  by (meson closedin_Hausdorff_singleton closedin_subset insert_subset)

lemma Hausdorff_space_discrete_topology [simp]:
   "Hausdorff_space (discrete_topology U)"
  unfolding Hausdorff_space_def
  by (metis Hausdorff_space_compact_sets Hausdorff_space_def compactin_discrete_topology equalityE openin_discrete_topology)

lemma compactin_Int:
   "\Hausdorff_space X; compactin X S; compactin X T\ \ compactin X (S \ T)"
  by (simp add: closed_Int_compactin compactin_imp_closedin)

lemma finite_topspace_imp_discrete_topology:
   "\topspace X = U; finite U; Hausdorff_space X\ \ X = discrete_topology U"
  using Hausdorff_imp_t1_space finite_t1_space_imp_discrete_topology by blast

lemma derived_set_of_finite:
   "\Hausdorff_space X; finite S\ \ X derived_set_of S = {}"
  using Hausdorff_imp_t1_space t1_space_derived_set_of_finite by auto

lemma infinite_perfect_set:
   "\Hausdorff_space X; S \ X derived_set_of S; S \ {}\ \ infinite S"
  using derived_set_of_finite by blast

lemma derived_set_of_singleton:
   "Hausdorff_space X \ X derived_set_of {x} = {}"
  by (simp add: derived_set_of_finite)

lemma closedin_Hausdorff_finite:
   "\Hausdorff_space X; S \ topspace X; finite S\ \ closedin X S"
  by (simp add: compactin_imp_closedin finite_imp_compactin_eq)

lemma open_in_Hausdorff_delete:
   "\Hausdorff_space X; openin X S\ \ openin X (S - {x})"
  using Hausdorff_imp_t1_space t1_space_openin_delete_alt by auto

lemma closedin_Hausdorff_finite_eq:
   "\Hausdorff_space X; finite S\ \ closedin X S \ S \ topspace X"
  by (meson closedin_Hausdorff_finite closedin_def)

lemma derived_set_of_infinite_openin:
   "Hausdorff_space X
        \<Longrightarrow> X derived_set_of S =
            {x \<in> topspace X. \<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite(S \<inter> U)}"
  using Hausdorff_imp_t1_space t1_space_derived_set_of_infinite_openin by fastforce

lemma Hausdorff_space_discrete_compactin:
   "Hausdorff_space X
        \<Longrightarrow> S \<inter> X derived_set_of S = {} \<and> compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> finite S"
  using derived_set_of_finite discrete_compactin_eq_finite by fastforce

lemma Hausdorff_space_finite_topspace:
   "Hausdorff_space X \ X derived_set_of (topspace X) = {} \ compact_space X \ finite(topspace X)"
  using derived_set_of_finite discrete_compact_space_eq_finite by auto

lemma derived_set_of_derived_set_subset:
   "Hausdorff_space X \ X derived_set_of (X derived_set_of S) \ X derived_set_of S"
  by (simp add: Hausdorff_imp_t1_space derived_set_of_derived_set_subset_gen)

lemma Hausdorff_space_injective_preimage:
  assumes "Hausdorff_space Y" and cmf: "continuous_map X Y f" and "inj_on f (topspace X)"
  shows "Hausdorff_space X"
  unfolding Hausdorff_space_def
proof clarify
  fix x y
  assume x: "x \ topspace X" and y: "y \ topspace X" and "x \ y"
  then obtain U V where "openin Y U" "openin Y V" "f x \ U" "f y \ V" "disjnt U V"
    using assms
    by (smt (verit, ccfv_threshold) Hausdorff_space_def continuous_map image_subset_iff inj_on_def)
  show "\U V. openin X U \ openin X V \ x \ U \ y \ V \ disjnt U V"
  proof (intro exI conjI)
    show "openin X {x \ topspace X. f x \ U}"
      using \<open>openin Y U\<close> cmf continuous_map by fastforce
    show "openin X {x \ topspace X. f x \ V}"
      using \<open>openin Y V\<close> cmf openin_continuous_map_preimage by blast
    show "disjnt {x \ topspace X. f x \ U} {x \ topspace X. f x \ V}"
      using \<open>disjnt U V\<close> by (auto simp add: disjnt_def)
  qed (use x \<open>f x \<in> U\<close> y \<open>f y \<in> V\<close> in auto)
qed

lemma homeomorphic_Hausdorff_space:
   "X homeomorphic_space Y \ Hausdorff_space X \ Hausdorff_space Y"
  unfolding homeomorphic_space_def homeomorphic_maps_map
  by (auto simp: homeomorphic_eq_everything_map Hausdorff_space_injective_preimage)

lemma Hausdorff_space_retraction_map_image:
   "\retraction_map X Y r; Hausdorff_space X\ \ Hausdorff_space Y"
  unfolding retraction_map_def
  using Hausdorff_space_subtopology homeomorphic_Hausdorff_space retraction_maps_section_image2 by blast

lemma compact_Hausdorff_space_optimal:
  assumes eq: "topspace Y = topspace X" and XY: "\U. openin X U \ openin Y U"
      and "Hausdorff_space X" "compact_space Y"
    shows "Y = X"
proof -
  have "\U. closedin X U \ closedin Y U"
    using XY using topology_finer_closedin [OF eq]
    by metis
  have "openin Y S = openin X S" for S
    by (metis XY assms(3) assms(4) closedin_compact_space compactin_contractive compactin_imp_closedin eq openin_closedin_eq)
  then show ?thesis
    by (simp add: topology_eq)
qed

lemma continuous_map_imp_closed_graph:
  assumes f: "continuous_map X Y f" and Y: "Hausdorff_space Y"
  shows "closedin (prod_topology X Y) ((\x. (x,f x)) ` topspace X)"
  unfolding closedin_def
proof
  show "(\x. (x, f x)) ` topspace X \ topspace (prod_topology X Y)"
    using continuous_map_def f by fastforce
  show "openin (prod_topology X Y) (topspace (prod_topology X Y) - (\x. (x, f x)) ` topspace X)"
    unfolding openin_prod_topology_alt
  proof (intro allI impI)
    show "\U V. openin X U \ openin Y V \ x \ U \ y \ V \ U \ V \ topspace (prod_topology X Y) - (\x. (x, f x)) ` topspace X"
      if "(x,y) \ topspace (prod_topology X Y) - (\x. (x, f x)) ` topspace X"
      for x y
    proof -
      have "x \ topspace X" and y: "y \ topspace Y" "y \ f x"
        using that by auto
      then have "f x \ topspace Y"
        using continuous_map_image_subset_topspace f by blast
      then obtain U V where UV: "openin Y U" "openin Y V" "f x \ U" "y \ V" "disjnt U V"
        using Y y Hausdorff_space_def by metis
      show ?thesis
      proof (intro exI conjI)
        show "openin X {x \ topspace X. f x \ U}"
          using \<open>openin Y U\<close> f openin_continuous_map_preimage by blast
        show "{x \ topspace X. f x \ U} \ V \ topspace (prod_topology X Y) - (\x. (x, f x)) ` topspace X"
          using UV by (auto simp: disjnt_iff dest: openin_subset)
      qed (use UV \<open>x \<in> topspace X\<close> in auto)
    qed
  qed
qed

lemma continuous_imp_closed_map:
   "\continuous_map X Y f; compact_space X; Hausdorff_space Y\ \ closed_map X Y f"
  by (meson closed_map_def closedin_compact_space compactin_imp_closedin image_compactin)

lemma continuous_imp_quotient_map:
   "\continuous_map X Y f; compact_space X; Hausdorff_space Y; f ` (topspace X) = topspace Y\
        \<Longrightarrow> quotient_map X Y f"
  by (simp add: continuous_imp_closed_map continuous_closed_imp_quotient_map)

lemma continuous_imp_homeomorphic_map:
   "\continuous_map X Y f; compact_space X; Hausdorff_space Y;
     f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
        \<Longrightarrow> homeomorphic_map X Y f"
  by (simp add: continuous_imp_closed_map bijective_closed_imp_homeomorphic_map)

lemma continuous_imp_embedding_map:
   "\continuous_map X Y f; compact_space X; Hausdorff_space Y; inj_on f (topspace X)\
        \<Longrightarrow> embedding_map X Y f"
  by (simp add: continuous_imp_closed_map injective_closed_imp_embedding_map)

lemma continuous_inverse_map:
  assumes "compact_space X" "Hausdorff_space Y"
    and cmf: "continuous_map X Y f" and gf: "\x. x \ topspace X \ g(f x) = x"
    and Sf:  "S \ f ` (topspace X)"
  shows "continuous_map (subtopology Y S) X g"
proof (rule continuous_map_from_subtopology_mono [OF _ \<open>S \<subseteq> f ` (topspace X)\<close>])
  show "continuous_map (subtopology Y (f ` (topspace X))) X g"
    unfolding continuous_map_closedin
  proof (intro conjI ballI allI impI)
    show "g \ topspace (subtopology Y (f ` topspace X)) \ topspace X"
      using gf by auto
  next
    fix C
    assume C: "closedin X C"
    show "closedin (subtopology Y (f ` topspace X))
           {x \<in> topspace (subtopology Y (f ` topspace X)). g x \<in> C}"
    proof (rule compactin_imp_closedin)
      show "Hausdorff_space (subtopology Y (f ` topspace X))"
        using Hausdorff_space_subtopology [OF \<open>Hausdorff_space Y\<close>] by blast
      have "compactin Y (f ` C)"
        using C cmf image_compactin closedin_compact_space [OF \<open>compact_space X\<close>] by blast
      moreover have "{x \ topspace Y. x \ f ` topspace X \ g x \ C} = f ` C"
        using closedin_subset [OF C] cmf by (auto simp: gf continuous_map_def)
      ultimately have "compactin Y {x \ topspace Y. x \ f ` topspace X \ g x \ C}"
        by simp
      then show "compactin (subtopology Y (f ` topspace X))
              {x \<in> topspace (subtopology Y (f ` topspace X)). g x \<in> C}"
        by (auto simp add: compactin_subtopology)
    qed
  qed
qed

lemma closed_map_paired_continuous_map_right:
   "\continuous_map X Y f; Hausdorff_space Y\ \ closed_map X (prod_topology X Y) (\x. (x,f x))"
  by (simp add: continuous_map_imp_closed_graph embedding_map_graph embedding_imp_closed_map)

lemma closed_map_paired_continuous_map_left:
  assumes f: "continuous_map X Y f" and Y: "Hausdorff_space Y"
  shows "closed_map X (prod_topology Y X) (\x. (f x,x))"
proof -
  have eq: "(\x. (f x,x)) = (\(a,b). (b,a)) \ (\x. (x,f x))"
    by auto
  show ?thesis
    unfolding eq
  proof (rule closed_map_compose)
    show "closed_map X (prod_topology X Y) (\x. (x, f x))"
      using Y closed_map_paired_continuous_map_right f by blast
    show "closed_map (prod_topology X Y) (prod_topology Y X) (\(a, b). (b, a))"
      by (metis homeomorphic_map_swap homeomorphic_imp_closed_map)
  qed
qed

lemma proper_map_paired_continuous_map_right:
   "\continuous_map X Y f; Hausdorff_space Y\
        \<Longrightarrow> proper_map X (prod_topology X Y) (\<lambda>x. (x,f x))"
  using closed_injective_imp_proper_map closed_map_paired_continuous_map_right
  by (metis (mono_tags, lifting) Pair_inject inj_onI)

lemma proper_map_paired_continuous_map_left:
   "\continuous_map X Y f; Hausdorff_space Y\
        \<Longrightarrow> proper_map X (prod_topology Y X) (\<lambda>x. (f x,x))"
  using closed_injective_imp_proper_map closed_map_paired_continuous_map_left
  by (metis (mono_tags, lifting) Pair_inject inj_onI)

lemma Hausdorff_space_prod_topology:
  "Hausdorff_space(prod_topology X Y) \ (prod_topology X Y) = trivial_topology \ Hausdorff_space X \ Hausdorff_space Y"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (rule topological_property_of_prod_component) (auto simp: Hausdorff_space_subtopology homeomorphic_Hausdorff_space)
next
  assume R: ?rhs
  show ?lhs
  proof (cases "(topspace X \ topspace Y) = {}")
    case False
    with R have ne: "topspace X \ {}" "topspace Y \ {}" and X: "Hausdorff_space X" and Y: "Hausdorff_space Y"
      by auto
    show ?thesis
      unfolding Hausdorff_space_def
    proof clarify
      fix x y x' y'
      assume xy: "(x, y) \ topspace (prod_topology X Y)"
        and xy': "(x',y') \ topspace (prod_topology X Y)"
        and *: "\U V. openin (prod_topology X Y) U \ openin (prod_topology X Y) V
               \<and> (x, y) \<in> U \<and> (x', y') \<in> V \<and> disjnt U V"
      have False if "x \ x' \ y \ y'"
        using that
      proof
        assume "x \ x'"
        then obtain U V where "openin X U" "openin X V" "x \ U" "x' \ V" "disjnt U V"
          by (metis Hausdorff_space_def X mem_Sigma_iff topspace_prod_topology xy xy')
        let ?U = "U \ topspace Y"
        let ?V = "V \ topspace Y"
        have "openin (prod_topology X Y) ?U" "openin (prod_topology X Y) ?V"
          by (simp_all add: openin_prod_Times_iff \<open>openin X U\<close> \<open>openin X V\<close>)
        moreover have "disjnt ?U ?V"
          by (simp add: \<open>disjnt U V\<close>)
        ultimately show False
          using * \<open>x \<in> U\<close> \<open>x' \<in> V\<close> xy xy' by (metis SigmaD2 SigmaI topspace_prod_topology)
      next
        assume "y \ y'"
        then obtain U V where "openin Y U" "openin Y V" "y \ U" "y' \ V" "disjnt U V"
          by (metis Hausdorff_space_def Y mem_Sigma_iff topspace_prod_topology xy xy')
        let ?U = "topspace X \ U"
        let ?V = "topspace X \ V"
        have "openin (prod_topology X Y) ?U" "openin (prod_topology X Y) ?V"
          by (simp_all add: openin_prod_Times_iff \<open>openin Y U\<close> \<open>openin Y V\<close>)
        moreover have "disjnt ?U ?V"
          by (simp add: \<open>disjnt U V\<close>)
        ultimately show False
          using "*" \<open>y \<in> U\<close> \<open>y' \<in> V\<close> xy xy' by (metis SigmaD1 SigmaI topspace_prod_topology)
      qed
      then show "x = x' \ y = y'"
        by blast
    qed
  qed force
qed

lemma Hausdorff_space_product_topology:
   "Hausdorff_space (product_topology X I) \ (\\<^sub>E i\I. topspace(X i)) = {} \ (\i \ I. Hausdorff_space (X i))"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (simp add: Hausdorff_space_subtopology PiE_eq_empty_iff homeomorphic_Hausdorff_space
                  topological_property_of_product_component)
next
  assume R: ?rhs
  show ?lhs
  proof (cases "(\\<^sub>E i\I. topspace(X i)) = {}")
    case True
    then show ?thesis
      by (simp add: Hausdorff_space_def)
  next
    case False
    have "\U V. openin (product_topology X I) U \ openin (product_topology X I) V \ f \ U \ g \ V \ disjnt U V"
      if f: "f \ (\\<^sub>E i\I. topspace (X i))" and g: "g \ (\\<^sub>E i\I. topspace (X i))" and "f \ g"
      for f g :: "'a \ 'b"
    proof -
      obtain m where "f m \ g m"
        using \<open>f \<noteq> g\<close> by blast
      then have "m \ I"
        using f g by fastforce
      then have "Hausdorff_space (X m)"
        using False that R by blast
      then obtain U V where U: "openin (X m) U" and V: "openin (X m) V" and "f m \ U" "g m \ V" "disjnt U V"
        by (metis Hausdorff_space_def PiE_mem \<open>f m \<noteq> g m\<close> \<open>m \<in> I\<close> f g)
      show ?thesis
      proof (intro exI conjI)
        let ?U = "(\\<^sub>E i\I. topspace(X i)) \ {x. x m \ U}"
        let ?V = "(\\<^sub>E i\I. topspace(X i)) \ {x. x m \ V}"
        show "openin (product_topology X I) ?U" "openin (product_topology X I) ?V"
          using \<open>m \<in> I\<close> U V
          by (force simp add: openin_product_topology intro: arbitrary_union_of_inc relative_to_inc finite_intersection_of_inc)+
        show "f \ ?U"
          using \<open>f m \<in> U\<close> f by blast
        show "g \ ?V"
          using \<open>g m \<in> V\<close> g by blast
        show "disjnt ?U ?V"
          using \<open>disjnt U V\<close> by (auto simp: PiE_def Pi_def disjnt_def)
        qed
    qed
    then show ?thesis
      by (simp add: Hausdorff_space_def)
  qed
qed

lemma Hausdorff_space_closed_neighbourhood:
   "Hausdorff_space X \
    (\<forall>x \<in> topspace X. \<exists>U C. openin X U \<and> closedin X C \<and>
                      Hausdorff_space(subtopology X C) \<and> x \<in> U \<and> U \<subseteq> C)" (is "_ = ?rhs")
proof
  assume R: ?rhs
  show "Hausdorff_space X"
    unfolding Hausdorff_space_def
  proof clarify
    fix x y
    assume x: "x \ topspace X" and y: "y \ topspace X" and "x \ y"
    obtain T C where *: "openin X T" "closedin X C" "x \ T" "T \ C"
                 and C: "Hausdorff_space (subtopology X C)"
      by (meson R \<open>x \<in> topspace X\<close>)
    show "\U V. openin X U \ openin X V \ x \ U \ y \ V \ disjnt U V"
    proof (cases "y \ C")
      case True
      with * C obtain U V where U: "openin (subtopology X C) U"
                        and V: "openin (subtopology X C) V"
                        and "x \ U" "y \ V" "disjnt U V"
        unfolding Hausdorff_space_def
        by (smt (verit, best) \<open>x \<noteq> y\<close> closedin_subset subsetD topspace_subtopology_subset)
      then obtain U' V' where UV': "U = U' \<inter> C" "openin X U'" "V = V' \<inter> C" "openin X V'"
        by (meson openin_subtopology)
      have "disjnt (T \ U') V'"
        using \<open>disjnt U V\<close> UV' \<open>T \<subseteq> C\<close> by (force simp: disjnt_iff)
      with \<open>T \<subseteq> C\<close> have "disjnt (T \<inter> U') (V' \<union> (topspace X - C))"
        unfolding disjnt_def by blast
      moreover
      have "openin X (T \ U')"
        by (simp add: \<open>openin X T\<close> \<open>openin X U'\<close> openin_Int)
      moreover have "openin X (V' \ (topspace X - C))"
        using \<open>closedin X C\<close> \<open>openin X V'\<close> by auto
      ultimately show ?thesis
        using UV' \x \ T\ \x \ U\ \y \ V\ by blast
    next
      case False
      with * y show ?thesis
        by (force simp: closedin_def disjnt_def)
    qed
  qed
qed fastforce

end

quality100%

¤ 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.0.19Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.