Theory HOL-Analysis.FSigma

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

section ‹$F$-Sigma and $G$-Delta sets in a Topological Space›

text ‹An $F$-sigma set is a countable union of closed sets; a $G$-delta set is the dual.›

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) ( ((-) (topspace X) ` 𝒯))"
    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)
          (countable intersection_of openin X relative_to topspace X)
              (topspace X   ((-) (topspace X) ` 𝒯))"
    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 S  topspace X 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 𝒱 where "countable 𝒱" and 𝒱: "𝒱  Collect (closedin Y)" "𝒱 = f`U"
      by (force simp: fsigma_in_def union_of_def)
    define 𝒰 where "𝒰  image (image g) 𝒱"
    have "countable 𝒰"
      using 𝒰_def countable 𝒱 by blast
    moreover have "𝒰  Collect (closedin X)"
      using f g homeomorphic_map_closedness_eq 𝒱 unfolding 𝒰_def by blast
    moreover have "𝒰  U"
      unfolding 𝒰_def  by (smt (verit) assms 1 𝒱 image_Union image_iff in_mono subsetI)
    moreover have "U  𝒰"
      unfolding 𝒰_def using assms 𝒱
      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 𝒱 where "countable 𝒱" and 𝒱: "𝒱  Collect (closedin X)" "𝒱 = U"
      by (auto simp: fsigma_in_def union_of_def)
    define 𝒰 where "𝒰  image (image f) 𝒱"
    have "countable 𝒰"
      using 𝒰_def countable 𝒱 by blast
    moreover have "𝒰  Collect (closedin Y)"
      using f g homeomorphic_map_closedness_eq 𝒱 unfolding 𝒰_def by blast
    moreover have "𝒰 = f`U"
      unfolding 𝒰_def using 𝒱 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
         (fsigma_in X U  U  topspace X  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
     gdelta_in X U  U  topspace X  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