Quelle FSigma.thy Sprache: Isabelle

(* Author: L C Paulson, University of Cambridge [ported from HOL Light, metric.ml] *)

section \<open>$F$-Sigma and $G$-Delta sets in a Topological Space\<close>

text \<open>An $F$-sigma set is a countable union of closed sets; a $G$-delta set is the dual.\<close>

theory FSigma
 imports Abstract_Topology
begin

definition fsigma_in
 where "fsigma_in X \ countable union_of closedin X"

definition gdelta_in
 where "gdelta_in X \ (countable intersection_of openin X) relative_to topspace X"

lemma fsigma_in_ascending:
 "fsigma_in X S \ (\C. (\n. closedin X (C n)) \ (\n. C n \ C(Suc n)) \ \ (range C) = S)"
 unfolding fsigma_in_def
 by (metis closedin_Un countable_union_of_ascending closedin_empty)

lemma gdelta_in_alt:
 "gdelta_in X S \ S \ topspace X \ (countable intersection_of openin X) S"
proof -
 have "(countable intersection_of openin X) (topspace X)"
 by (simp add: countable_intersection_of_inc)
 then show ?thesis
 unfolding gdelta_in_def
 by (metis countable_intersection_of_inter relative_to_def relative_to_imp_subset relative_to_subset_inc)
qed

lemma fsigma_in_subset: "fsigma_in X S \ S \ topspace X"
 using closedin_subset by (fastforce simp: fsigma_in_def union_of_def subset_iff)

lemma gdelta_in_subset: "gdelta_in X S \ S \ topspace X"
 by (simp add: gdelta_in_alt)

lemma closed_imp_fsigma_in: "closedin X S \ fsigma_in X S"
 by (simp add: countable_union_of_inc fsigma_in_def)

lemma open_imp_gdelta_in: "openin X S \ gdelta_in X S"
 by (simp add: countable_intersection_of_inc gdelta_in_alt openin_subset)

lemma fsigma_in_empty [iff]: "fsigma_in X {}"
 by (simp add: closed_imp_fsigma_in)

lemma gdelta_in_empty [iff]: "gdelta_in X {}"
 by (simp add: open_imp_gdelta_in)

lemma fsigma_in_topspace [iff]: "fsigma_in X (topspace X)"
 by (simp add: closed_imp_fsigma_in)

lemma gdelta_in_topspace [iff]: "gdelta_in X (topspace X)"
 by (simp add: open_imp_gdelta_in)

lemma fsigma_in_Union:
 "\countable T; \S. S \ T \ fsigma_in X S\ \ fsigma_in X (\ T)"
 by (simp add: countable_union_of_Union fsigma_in_def)

lemma fsigma_in_Un:
 "\fsigma_in X S; fsigma_in X T\ \ fsigma_in X (S \ T)"
 by (simp add: countable_union_of_Un fsigma_in_def)

lemma fsigma_in_Int:
 "\fsigma_in X S; fsigma_in X T\ \ fsigma_in X (S \ T)"
 by (simp add: closedin_Int countable_union_of_Int fsigma_in_def)

lemma gdelta_in_Inter:
 "\countable T; T\{}; \S. S \ T \ gdelta_in X S\ \ gdelta_in X (\ T)"
 by (simp add: Inf_less_eq countable_intersection_of_Inter gdelta_in_alt)

lemma gdelta_in_Int:
 "\gdelta_in X S; gdelta_in X T\ \ gdelta_in X (S \ T)"
 by (simp add: countable_intersection_of_inter gdelta_in_alt le_infI2)

lemma gdelta_in_Un:
 "\gdelta_in X S; gdelta_in X T\ \ gdelta_in X (S \ T)"
 by (simp add: countable_intersection_of_union gdelta_in_alt openin_Un)

lemma fsigma_in_diff:
 assumes "fsigma_in X S" "gdelta_in X T"
 shows "fsigma_in X (S - T)"
proof -
 have [simp]: "S - (S \ T) = S - T" for S T :: "'a set"
 by auto
 have [simp]: "topspace X - \\ = (\T\\. topspace X - T)" for \
 by auto
 have "\\. \countable \; \ \ Collect (openin X)\ \
 (countable union_of closedin X) (\<Union> ((-) (topspace X) ` \<T>))"
 by (metis Ball_Collect countable_union_of_UN countable_union_of_inc openin_closedin_eq)
 then have "\S. gdelta_in X S \ fsigma_in X (topspace X - S)"
 by (simp add: fsigma_in_def gdelta_in_def all_relative_to all_intersection_of del: UN_simps)
 then show ?thesis
 by (metis Diff_Int2 Diff_Int_distrib2 assms fsigma_in_Int fsigma_in_subset inf.absorb_iff2)
qed

lemma gdelta_in_diff:
 assumes "gdelta_in X S" "fsigma_in X T"
 shows "gdelta_in X (S - T)"
proof -
 have [simp]: "topspace X - \\ = topspace X \ (\T\\. topspace X - T)" for \
 by auto
 have "\\. \countable \; \ \ Collect (closedin X)\
 \<Longrightarrow> (countable intersection_of openin X relative_to topspace X)
 (topspace X \<inter> \<Inter> ((-) (topspace X) ` \<T>))"
 by (metis Ball_Collect closedin_def countable_intersection_of_INT countable_intersection_of_inc relative_to_inc)
 then have "\S. fsigma_in X S \ gdelta_in X (topspace X - S)"
 by (simp add: fsigma_in_def gdelta_in_def all_union_of del: INT_simps)
 then show ?thesis
 by (metis Diff_Int2 Diff_Int_distrib2 assms gdelta_in_Int gdelta_in_alt inf.orderE inf_commute)
qed

lemma gdelta_in_fsigma_in:
 "gdelta_in X S \ S \ topspace X \ fsigma_in X (topspace X - S)"
 by (metis double_diff fsigma_in_diff fsigma_in_topspace gdelta_in_alt gdelta_in_diff gdelta_in_topspace)

lemma fsigma_in_gdelta_in:
 "fsigma_in X S \ S \ topspace X \ gdelta_in X (topspace X - S)"
 by (metis Diff_Diff_Int fsigma_in_subset gdelta_in_fsigma_in inf.absorb_iff2)

lemma gdelta_in_descending:
 "gdelta_in X S \ (\C. (\n. openin X (C n)) \ (\n. C(Suc n) \ C n) \ \(range C) = S)" (is "?lhs=?rhs")
proof
 assume ?lhs
 then obtain C where C: "S \ topspace X" "\n. closedin X (C n)"
 "\n. C n \ C(Suc n)" "\(range C) = topspace X - S"
 by (meson fsigma_in_ascending gdelta_in_fsigma_in)
 define D where "D \ \n. topspace X - C n"
 have "\n. openin X (D n) \ D (Suc n) \ D n"
 by (simp add: Diff_mono C D_def openin_diff)
 moreover have "\(range D) = S"
 by (simp add: Diff_Diff_Int Int_absorb1 C D_def)
 ultimately show ?rhs
 by metis
next
 assume ?rhs
 then obtain C where "S \ topspace X"
 and C: "\n. openin X (C n)" "\n. C(Suc n) \ C n" "\(range C) = S"
 using openin_subset by fastforce
 define D where "D \ \n. topspace X - C n"
 have "\n. closedin X (D n) \ D n \ D(Suc n)"
 by (simp add: Diff_mono C closedin_diff D_def)
 moreover have "\(range D) = topspace X - S"
 using C D_def by blast
 ultimately show ?lhs
 by (metis \<open>S \<subseteq> topspace X\<close> fsigma_in_ascending gdelta_in_fsigma_in)
qed

lemma homeomorphic_map_fsigmaness:
 assumes f: "homeomorphic_map X Y f" and "U \ topspace X"
 shows "fsigma_in Y (f ` U) \ fsigma_in X U" (is "?lhs=?rhs")
proof -
 obtain g where g: "homeomorphic_maps X Y f g" and g: "homeomorphic_map Y X g"
 and 1: "(\x \ topspace X. g(f x) = x)" and 2: "(\y \ topspace Y. f(g y) = y)"
 using assms homeomorphic_map_maps by (metis homeomorphic_maps_map)
 show ?thesis
 proof
 assume ?lhs
 then obtain \<V> where "countable \<V>" and \<V>: "\<V> \<subseteq> Collect (closedin Y)" "\<Union>\<V> = f`U"
 by (force simp: fsigma_in_def union_of_def)
 define \ where "\ \<equiv> image (image g) \<V>"
 have "countable \"
 using \_def \<open>countable \<V>\<close> by blast
 moreover have "\ \ Collect (closedin X)"
 using f g homeomorphic_map_closedness_eq \<V> unfolding \_def by blast
 moreover have "\\ \ U"
 unfolding \_def by (smt (verit) assms 1 \<V> image_Union image_iff in_mono subsetI)
 moreover have "U \ \\"
 unfolding \_def using assms \<V>
 by (smt (verit, del_insts) "1" imageI image_Union subset_iff)
 ultimately show ?rhs
 by (metis fsigma_in_def subset_antisym union_of_def)
 next
 assume ?rhs
 then obtain \<V> where "countable \<V>" and \<V>: "\<V> \<subseteq> Collect (closedin X)" "\<Union>\<V> = U"
 by (auto simp: fsigma_in_def union_of_def)
 define \ where "\ \<equiv> image (image f) \<V>"
 have "countable \"
 using \_def \<open>countable \<V>\<close> by blast
 moreover have "\ \ Collect (closedin Y)"
 using f g homeomorphic_map_closedness_eq \<V> unfolding \_def by blast
 moreover have "\\ = f`U"
 unfolding \_def using \<V> by blast
 ultimately show ?lhs
 by (metis fsigma_in_def union_of_def)
 qed
qed

lemma homeomorphic_map_fsigmaness_eq:
 "homeomorphic_map X Y f
 \<Longrightarrow> (fsigma_in X U \<longleftrightarrow> U \<subseteq> topspace X \<and> fsigma_in Y (f ` U))"
 by (metis fsigma_in_subset homeomorphic_map_fsigmaness)

lemma homeomorphic_map_gdeltaness:
 assumes "homeomorphic_map X Y f" "U \ topspace X"
 shows "gdelta_in Y (f ` U) \ gdelta_in X U"
proof -
 have "topspace Y - f ` U = f ` (topspace X - U)"
 by (metis (no_types, lifting) Diff_subset assms homeomorphic_eq_everything_map inj_on_image_set_diff)
 then show ?thesis
 using assms homeomorphic_imp_surjective_map
 by (fastforce simp: gdelta_in_fsigma_in homeomorphic_map_fsigmaness_eq)
qed

lemma homeomorphic_map_gdeltaness_eq:
 "homeomorphic_map X Y f
 \<Longrightarrow> gdelta_in X U \<longleftrightarrow> U \<subseteq> topspace X \<and> gdelta_in Y (f ` U)"
 by (meson gdelta_in_subset homeomorphic_map_gdeltaness)

lemma fsigma_in_relative_to:
 "(fsigma_in X relative_to S) = fsigma_in (subtopology X S)"
 by (simp add: fsigma_in_def countable_union_of_relative_to closedin_relative_to)

lemma fsigma_in_subtopology:
 "fsigma_in (subtopology X U) S \ (\T. fsigma_in X T \ S = T \ U)"
 by (metis fsigma_in_relative_to inf_commute relative_to_def)

lemma gdelta_in_relative_to:
 "(gdelta_in X relative_to S) = gdelta_in (subtopology X S)"
 apply (simp add: gdelta_in_def)
 by (metis countable_intersection_of_relative_to openin_relative_to subtopology_restrict)

lemma gdelta_in_subtopology:
 "gdelta_in (subtopology X U) S \ (\T. gdelta_in X T \ S = T \ U)"
 by (metis gdelta_in_relative_to inf_commute relative_to_def)

lemma fsigma_in_fsigma_subtopology:
 "fsigma_in X S \ (fsigma_in (subtopology X S) T \ fsigma_in X T \ T \ S)"
 by (metis fsigma_in_Int fsigma_in_gdelta_in fsigma_in_subtopology inf.orderE topspace_subtopology_subset)

lemma gdelta_in_gdelta_subtopology:
 "gdelta_in X S \ (gdelta_in (subtopology X S) T \ gdelta_in X T \ T \ S)"
 by (metis gdelta_in_Int gdelta_in_subset gdelta_in_subtopology inf.orderE topspace_subtopology_subset)

end

quality99%

¤ Dauer der Verarbeitung: 0.14 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.