Theory 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)"
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"

lemma closed_imp_fsigma_in: "closedin X S ⟹ fsigma_in X S"

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 {}"

lemma gdelta_in_empty [iff]: "gdelta_in X {}"

lemma fsigma_in_topspace [iff]: "fsigma_in X (topspace X)"

lemma gdelta_in_topspace [iff]: "gdelta_in X (topspace X)"

lemma fsigma_in_Union:
"⟦countable T; ⋀S. S ∈ T ⟹ fsigma_in X S⟧ ⟹ fsigma_in X (⋃ T)"

lemma fsigma_in_Un:
"⟦fsigma_in X S; fsigma_in X T⟧ ⟹ fsigma_in X (S ∪ T)"

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)"
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
```