Theory Lemmas_StandardBorel

(*  Title:   Lemmas_StandardBorel.thy
    Author:  Michikazu Hirata, Tokyo Institute of Technology
*)

text ‹ We refer to the HOL-Analysis library,
       the textbooks by Matsuzaka~\cite{topology} and Srivastava~\cite{borelsets},
       and the lecture note by Biskup~\cite{standardborel}.›

section  ‹Lemmas›
theory Lemmas_StandardBorel
  imports "HOL-Probability.Probability"
begin

subsection ‹Lemmas for Abstract Topology›

subsubsection ‹ Generated By ›
lemma topology_generated_by_sub:
  assumes "⋀U. U ∈ 𝒰 ⟹ (openin X U)"
      and "openin (topology_generated_by 𝒰) U"
    shows "openin X U"
proof -
  have "generate_topology_on 𝒰 U"
    by (simp add: assms(2) openin_topology_generated_by)
  then show ?thesis
    by induction (use assms(1) in auto)
qed

lemma topology_generated_by_open:
 "S = topology_generated_by {U | U . openin S U}"
  unfolding topology_eq
proof standard+
  fix U
  assume "openin (topology_generated_by {U |U. openin S U}) U"
  note this[simplified openin_topology_generated_by_iff]
  then show "openin S U"
    by induction auto
qed(simp add: openin_topology_generated_by_iff generate_topology_on.Basis)

lemma topology_generated_by_eq:
  assumes "⋀U. U ∈ 𝒰 ⟹ (openin (topology_generated_by 𝒪) U)"
      and "⋀U. U ∈ 𝒪 ⟹ (openin (topology_generated_by 𝒰) U)"
    shows "topology_generated_by 𝒪 = topology_generated_by 𝒰"
  using topology_generated_by_sub[of 𝒰, OF assms(1)] topology_generated_by_sub[of 𝒪,OF assms(2)]
  by(auto simp: topology_eq)

lemma topology_generated_by_homeomorphic_spaces:
  assumes "homeomorphic_map X Y f" "X = topology_generated_by 𝒪"
  shows "Y = topology_generated_by ((`) f ` 𝒪)"
  unfolding topology_eq
proof
  have f:"open_map X Y f" "inj_on f (topspace X)"
    using assms(1) by (simp_all add: homeomorphic_imp_open_map perfect_injective_eq_homeomorphic_map[symmetric])
  obtain g where g: "⋀x. x ∈ topspace X ⟹ g (f x) = x" "⋀y. y ∈ topspace Y ⟹ f (g y) = y" "open_map Y X g" "inj_on g (topspace Y)"
    using homeomorphic_map_maps[of X Y f,simplified assms(1)] homeomorphic_imp_open_map homeomorphic_maps_map[of X Y f] homeomorphic_imp_injective_map[of Y X] by blast
  show "⋀S. openin Y S = openin (topology_generated_by ((`) f ` 𝒪)) S"
  proof safe
    fix S
    assume "openin Y S"
    then have "openin X (g ` S)"
      using g(3) by (simp add: open_map_def)
    hence h:"generate_topology_on 𝒪 (g ` S)"
      by(simp add: assms(2) openin_topology_generated_by_iff)
    have "S = f ` (g `  S)"
      using openin_subset[OF ‹openin Y S›] g(2) by(fastforce simp: image_def)
    also have "openin (topology_generated_by ((`) f ` 𝒪)) ..."
      using h
    proof induction
      case Empty
      then show ?case by simp
    next
      case (Int a b)
      with inj_on_image_Int[OF f(2),of a b] show ?case
        by (metis assms(2) openin_Int openin_subset openin_topology_generated_by_iff)
    next
      case (UN K)
      then show ?case
        by(auto simp: image_Union)
    next
      case (Basis s)
      then show ?case
        by(auto intro!: generate_topology_on.Basis simp: openin_topology_generated_by_iff)
    qed
    finally show "openin (topology_generated_by ((`) f ` 𝒪)) S" .
  next
    fix S
    assume "openin (topology_generated_by ((`) f ` 𝒪)) S"
    then have "generate_topology_on ((`) f ` 𝒪) S"
      by(simp add: openin_topology_generated_by_iff)
    thus "openin Y S"
    proof induction
      case (Basis s)
      then obtain U where u:"U ∈ 𝒪" "s = f ` U" by auto
      then show ?case
        using assms(1) assms(2) homeomorphic_map_openness_eq topology_generated_by_Basis by blast
    qed auto
  qed
qed

lemma open_map_generated_topo:
  assumes "⋀u. u ∈ U ⟹ openin S (f ` u)" "inj_on f (topspace (topology_generated_by U))"
  shows "open_map (topology_generated_by U) S f"
  unfolding open_map_def
proof safe
  fix u
  assume "openin (topology_generated_by U) u"
  then have "generate_topology_on U u" 
    by(simp add: openin_topology_generated_by_iff)
  thus "openin S (f ` u)"
  proof induction
    case (Int a b)
    then have [simp]:"f ` (a ∩ b) = f ` a ∩ f ` b"
      by (meson assms(2) inj_on_image_Int openin_subset openin_topology_generated_by_iff)
    from Int show ?case by auto
  qed (simp_all add: image_Union openin_clauses(3) assms)
qed

lemma subtopology_generated_by:
 "subtopology (topology_generated_by 𝒪) T = topology_generated_by {T ∩ U | U. U ∈ 𝒪}"
  unfolding topology_eq openin_subtopology openin_topology_generated_by_iff
proof safe
  fix A
  assume "generate_topology_on 𝒪 A"
  then show "generate_topology_on {T ∩ U |U. U ∈ 𝒪} (A ∩ T)"
  proof induction
    case Empty
    then show ?case
      by (simp add: generate_topology_on.Empty)
  next
    case (Int a b)
    moreover have "a ∩ b ∩ T = (a ∩ T) ∩ (b ∩ T)" by auto
    ultimately show ?case
      by(auto intro!: generate_topology_on.Int)
  next
    case (UN K)
    moreover have "(⋃ K ∩ T) = (⋃ { k ∩ T | k. k ∈ K})" by auto
    ultimately show ?case
      by(auto intro!: generate_topology_on.UN)
  next
    case (Basis s)
    then show ?case
      by(auto intro!: generate_topology_on.Basis)
  qed
next
  fix A
  assume "generate_topology_on {T ∩ U |U. U ∈ 𝒪} A"
  then show "∃L. generate_topology_on 𝒪 L ∧ A = L ∩ T"
  proof induction
    case Empty
    show ?case
      by(auto intro!: exI[where x="{}"] generate_topology_on.Empty)
  next
    case ih:(Int a b)
    then obtain La Lb where
     "generate_topology_on 𝒪 La" "a = La ∩ T" "generate_topology_on 𝒪 Lb" "b = Lb ∩ T"
      by auto
    thus ?case
      using ih by(auto intro!: exI[where x="La ∩ Lb"] generate_topology_on.Int)
  next
    case ih:(UN K)
    then obtain L where
    "⋀k. k ∈ K ⟹ generate_topology_on 𝒪 (L k) " "⋀k. k ∈ K ⟹ k = (L k) ∩ T"
      by metis
    thus ?case
      using ih by(auto intro!: exI[where x="⋃k∈K. L k"] generate_topology_on.UN)
  next
    case (Basis s)
    then show ?case
      using generate_topology_on.Basis by fastforce
  qed
qed

lemma prod_topology_generated_by:
  "topology_generated_by { U × V | U V. U ∈ 𝒪 ∧ V ∈ 𝒰} = prod_topology (topology_generated_by 𝒪) (topology_generated_by 𝒰)"
  unfolding topology_eq
proof safe
  fix U
  assume h:"openin (topology_generated_by {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒰}) U"
  show "openin (prod_topology (topology_generated_by 𝒪) (topology_generated_by 𝒰)) U"
    by(auto simp: openin_prod_Times_iff[of "topology_generated_by 𝒪" "topology_generated_by 𝒰"]
          intro!: topology_generated_by_Basis topology_generated_by_sub[OF _ h])
next
  fix U
  assume "openin (prod_topology (topology_generated_by 𝒪) (topology_generated_by 𝒰)) U"
  then have "∀z∈U. ∃V1 V2. openin (topology_generated_by 𝒪) V1 ∧ openin (topology_generated_by 𝒰) V2 ∧ fst z ∈ V1 ∧ snd z ∈ V2 ∧ V1 × V2 ⊆ U"
    by(auto simp: openin_prod_topology_alt)
  hence "∃V1. ∀z∈U. ∃V2. openin (topology_generated_by 𝒪) (V1 z) ∧ openin (topology_generated_by 𝒰) V2 ∧ fst z ∈ (V1 z) ∧ snd z ∈ V2 ∧ (V1 z) × V2 ⊆ U"
    by(rule bchoice)
  then obtain V1 where "∀z∈U. ∃V2. openin (topology_generated_by 𝒪) (V1 z) ∧ openin (topology_generated_by 𝒰) V2 ∧ fst z ∈ (V1 z) ∧ snd z ∈ V2 ∧ (V1 z) × V2 ⊆ U"
    by auto
  hence "∃V2. ∀z∈U. openin (topology_generated_by 𝒪) (V1 z) ∧ openin (topology_generated_by 𝒰) (V2 z) ∧ fst z ∈ (V1 z) ∧ snd z ∈ (V2 z) ∧ (V1 z) × (V2 z) ⊆ U"
    by(rule bchoice)
  then obtain V2 where hv12:"⋀z. z∈U ⟹ openin (topology_generated_by 𝒪) (V1 z) ∧ openin (topology_generated_by 𝒰) (V2 z) ∧ fst z ∈ (V1 z) ∧ snd z ∈ (V2 z) ∧ (V1 z) × (V2 z) ⊆ U"
    by auto
  hence 1:"U = (⋃z∈U. (V1 z) × (V2 z))"
    by auto
  have "openin (topology_generated_by {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒰}) (⋃z∈U. (V1 z) × (V2 z))"
  proof(rule openin_Union)
    show "⋀S. S ∈ (λz. V1 z × V2 z) ` U ⟹ openin (topology_generated_by {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒰}) S"
    proof safe
      fix x y
      assume h:"(x,y) ∈ U"
      then have "generate_topology_on 𝒪 (V1 (x,y))"
        using hv12 by(auto simp: openin_topology_generated_by_iff)
      thus "openin (topology_generated_by {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒰}) (V1 (x, y) × V2 (x, y))"
      proof induction
        case Empty
        then show ?case by auto
      next
        case (Int a b)
        thus ?case
          by (auto simp: Sigma_Int_distrib1) 
      next
        case (UN K)
        then have "openin (topology_generated_by {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒰}) (⋃{ k × V2 (x, y) | k. k ∈ K})"
          by auto
        moreover have "(⋃ {k × V2 (x, y) |k. k ∈ K}) = (⋃ K × V2 (x, y))"
          by blast
        ultimately show ?case by simp
      next
        case ho:(Basis s)
        have "generate_topology_on 𝒰 (V2 (x,y))"
          using h hv12 by(auto simp: openin_topology_generated_by_iff)
        thus ?case
        proof induction
          case Empty
          then show ?case by auto
        next
          case (Int a b)
          then show ?case
            by (auto simp: Sigma_Int_distrib2) 
        next
          case (UN K)
          then have "openin (topology_generated_by {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒰}) (⋃ { s × k | k. k ∈K})"
            by auto
          moreover have "(⋃ { s × k | k. k ∈K}) = s × ⋃K"
            by blast
          ultimately show ?case by simp
        next
          case (Basis s')
          then show ?case
            using ho by(auto intro!: topology_generated_by_Basis)
        qed
      qed
    qed
  qed
  thus "openin (topology_generated_by {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒰}) U"
    using 1 by auto
qed

lemma prod_topology_generated_by_open:
 "prod_topology S S' = topology_generated_by {U × V | U V. openin S U ∧ openin S' V}"
  using prod_topology_generated_by[of " {U |U. openin S U}" "{U |U. openin S' U}"] topology_generated_by_open[of S,symmetric] topology_generated_by_open[of S']
  by auto

lemma product_topology_cong:
  assumes "⋀i. i ∈ I ⟹ S i = K i"
  shows "product_topology S I = product_topology K I"
proof -
  have 1:"{Π⇩E i∈I. X i |X. (∀i. openin (S i) (X i)) ∧ finite {i. X i ≠ topspace (S i)}} ⊆ {Π⇩E i∈I. X i |X. (∀i. openin (K i) (X i)) ∧ finite {i. X i ≠ topspace (K i)}}" if "⋀i. i ∈ I ⟹ S i = K i" for S K :: "_ ⇒ 'b topology"
  proof
    fix x
    assume hx:"x ∈ {Π⇩E i∈I. X i |X. (∀i. openin (S i) (X i)) ∧ finite {i. X i ≠ topspace (S i)}}"
    then obtain X where hX:
     "x = (Π⇩E i∈I. X i)" "⋀i. openin (S i) (X i)" "finite {i. X i ≠ topspace (S i)}"
      by auto
    define X' where "X' ≡ (λi. if i ∈ I then X i else topspace (K i))"
    have "x = (Π⇩E i∈I. X' i)"
      by(auto simp: hX(1) X'_def PiE_def Pi_def)
    moreover have "finite {i. X' i ≠ topspace (K i)}"
      using that by(auto intro!: finite_subset[OF _ hX(3)] simp: X'_def)
    moreover have "openin (K i) (X' i)" for i
      using hX(2)[of i] that[of i] by(auto simp: X'_def)
    ultimately show "x ∈ {Π⇩E i∈I. X i |X. (∀i. openin (K i) (X i)) ∧ finite {i. X i ≠ topspace (K i)}}"
      by(auto intro!: exI[where x="X'"])
  qed
  have "{Π⇩E i∈I. X i |X. (∀i. openin (S i) (X i)) ∧ finite {i. X i ≠ topspace (S i)}} = {Π⇩E i∈I. X i |X. (∀i. openin (K i) (X i)) ∧ finite {i. X i ≠ topspace (K i)}}"
    using 1[of S K] 1[of K S] assms by auto
  thus ?thesis
    by(simp add: product_topology_def)
qed

lemma topology_generated_by_without_empty:
 "topology_generated_by 𝒪 = topology_generated_by { U ∈ 𝒪. U ≠ {}}"
proof(rule topology_generated_by_eq)
  fix U
  show "U ∈ 𝒪 ⟹ openin (topology_generated_by { U ∈ 𝒪. U ≠ {}}) U"
    by(cases "U = {}") (simp_all add: topology_generated_by_Basis)
qed (simp add: topology_generated_by_Basis)

lemma topology_from_bij:
  assumes "bij_betw f A (topspace S)"
  shows "homeomorphic_map (pullback_topology A f S) S f" "topspace (pullback_topology A f S) = A"
proof -
  note h = bij_betw_imp_surj_on[OF assms] bij_betw_inv_into_left[OF assms] bij_betw_inv_into_right[OF assms]
  then show [simp]:"topspace (pullback_topology A f S) = A"
    by(auto simp: topspace_pullback_topology)
  show "homeomorphic_map (pullback_topology A f S) S f"
    by(auto simp: homeomorphic_map_maps homeomorphic_maps_def h continuous_map_pullback[OF continuous_map_id,simplified] inv_into_into intro!: exI[where x="inv_into A f"] continuous_map_pullback'[where f=f]) (metis (mono_tags, opaque_lifting) comp_apply continuous_map_eq continuous_map_id h(3) id_apply)
qed

lemma openin_pullback_topology':
  assumes "bij_betw f A (topspace S)"
  shows "openin (pullback_topology A f S) u ⟷ (openin S (f ` u)) ∧ u ⊆ A"
  unfolding openin_pullback_topology
proof safe
  fix U
  assume h:"openin S U" "u = f -` U ∩ A"
  from openin_subset[OF this(1)] assms
  have [simp]:"f ` (f -` U ∩ A) = U"
    by(auto simp: image_def vimage_def bij_betw_def)
  show "openin S (f ` (f -` U ∩ A))"
    by(simp add: h)
next
  assume "openin S (f ` u)" "u ⊆ A"
  with assms show "∃U. openin S U ∧ u = f -` U ∩ A"
    by(auto intro!: exI[where x="f ` u"] simp: bij_betw_def inj_on_def)
qed

subsubsection ‹ Isolated Point ›    
definition isolated_points_of :: "'a topology ⇒ 'a set ⇒ 'a set" (infixr "isolated'_points'_of" 80) where
"X isolated_points_of A ≡ {x∈topspace X ∩ A. x ∉ X derived_set_of A}"

lemma isolated_points_of_eq:
 "X isolated_points_of A = {x∈topspace X ∩ A. ∃U. x ∈ U ∧ openin X U ∧ U ∩ (A - {x}) = {}}"
  unfolding isolated_points_of_def by(auto simp: in_derived_set_of)

lemma in_isolated_points_of:
 "x ∈ X isolated_points_of A ⟷ x ∈ topspace X ∧ x ∈ A ∧ (∃U. x ∈ U ∧ openin X U ∧ U ∩ (A - {x}) = {})"
  by(simp add: isolated_points_of_eq)

lemma derived_set_of_eq:
 "x ∈ X derived_set_of A ⟷ x ∈ X closure_of (A - {x})"
  by(auto simp: in_derived_set_of in_closure_of)

subsubsection ‹ Perfect Set ›
definition perfect_set :: "'a topology ⇒ 'a set ⇒ bool" where
"perfect_set X A ⟷ closedin X A ∧ X isolated_points_of A = {}"

abbreviation "perfect_space X ≡ perfect_set X (topspace X)"

lemma perfect_space_euclidean: "perfect_space (euclidean :: 'a :: perfect_space topology)"
  by(auto simp: isolated_points_of_def perfect_set_def derived_set_of_eq closure_interior)

lemma perfect_setI:
  assumes "closedin X A"
      and "⋀x T. ⟦x ∈ A; x ∈ T; openin X T⟧ ⟹ ∃y≠x. y ∈ T ∧ y ∈ A"
    shows "perfect_set X A"
  using assms by(simp add: perfect_set_def isolated_points_of_def in_derived_set_of) blast

lemma perfect_spaceI:
  assumes "⋀x T. ⟦x ∈ T; openin X T⟧ ⟹ ∃y≠x. y ∈ T"
  shows "perfect_space X"
  using assms by(auto intro!: perfect_setI) (meson in_mono openin_subset)

lemma perfect_setD:
  assumes "perfect_set X A"
  shows "closedin X A" "A ⊆ topspace X" "⋀x T. ⟦x ∈ A; x ∈ T; openin X T⟧ ⟹ ∃y≠x. y ∈ T ∧ y ∈ A"
  using assms closedin_subset[of X A] by(simp_all add: perfect_set_def isolated_points_of_def in_derived_set_of) blast

lemma perfect_space_perfect:
  "perfect_set euclidean (UNIV :: 'a :: perfect_space set)"
  by(auto simp: perfect_set_def in_isolated_points_of) (metis Int_Diff inf_top.right_neutral insert_Diff not_open_singleton)

lemma perfect_set_subtopology:
  assumes "perfect_set X A"
  shows "perfect_space (subtopology X A)"
  using perfect_setD[OF assms] by(auto intro!: perfect_setI simp: inf.absorb_iff2 openin_subtopology)

subsubsection ‹ Bases and Sub-Bases in Abstract Topology›
definition subbase_in :: "['a topology, 'a set set] ⇒ bool" where
"subbase_in S 𝒪 ⟷ S = topology_generated_by 𝒪"

definition base_in :: "['a topology, 'a set set] ⇒ bool" where
"base_in S 𝒪 ⟷ (∀U. openin S U ⟷ (∃𝒰. U = ⋃𝒰 ∧ 𝒰 ⊆ 𝒪))"

lemma second_countable_base_in: "second_countable S ⟷ (∃𝒪. countable 𝒪 ∧ base_in S 𝒪)"
proof -
  have [simp]:"⋀ℬ. (openin S = arbitrary union_of (λx. x ∈ ℬ)) ⟷ (∀U. openin S U ⟷ (∃𝒰. U = ⋃𝒰 ∧ 𝒰 ⊆ ℬ))"
    by(simp add: arbitrary_def union_of_def fun_eq_iff) metis
  show ?thesis
    by(auto simp: second_countable base_in_def)
qed

definition zero_dimensional :: "'a topology ⇒ bool" where
"zero_dimensional S ⟷ (∃𝒪. base_in S 𝒪 ∧ (∀u∈𝒪. openin S u ∧ closedin S u))"

lemma openin_base:
  assumes "base_in S 𝒪 " "U = ⋃𝒰" and "𝒰 ⊆ 𝒪"
  shows "openin S U"
  using assms by(auto simp: base_in_def)

lemma base_is_subbase:
  assumes "base_in S 𝒪"
  shows "subbase_in S 𝒪"
  unfolding subbase_in_def topology_eq openin_topology_generated_by_iff
proof safe
  fix U
  assume "openin S U"
  then obtain 𝒰 where hu:"U = ⋃𝒰" "𝒰 ⊆ 𝒪"
    using assms by(auto simp: base_in_def)
  thus "generate_topology_on 𝒪 U"
    by(auto intro!: generate_topology_on.UN) (auto intro!:  generate_topology_on.Basis)
next
  fix U
  assume "generate_topology_on 𝒪 U"
  then show "openin S U"
  proof induction
    case (Basis s)
    then show ?case
      using openin_base[OF assms,of s "{s}"]
      by auto
  qed auto
qed

lemma subbase_in_subset:
  assumes "subbase_in S 𝒪" and "U ∈ 𝒪"
  shows "U ⊆ topspace S"
  using assms(1)[simplified subbase_in_def] topology_generated_by_topspace assms
  by auto

lemma subbase_in_openin:
  assumes "subbase_in S 𝒪" and "U ∈ 𝒪"
  shows "openin S U"
  using assms by(simp add: subbase_in_def openin_topology_generated_by_iff generate_topology_on.Basis)

lemma base_in_subset:
  assumes "base_in S 𝒪" and "U ∈ 𝒪"
  shows "U ⊆ topspace S"
  using subbase_in_subset[OF base_is_subbase[OF assms(1)] assms(2)] .

lemma base_in_openin:
  assumes "base_in S 𝒪" and "U ∈ 𝒪"
  shows "openin S U"
  using subbase_in_openin[OF base_is_subbase[OF assms(1)] assms(2)] .

lemma base_in_def2:
  assumes "⋀U. U ∈ 𝒪 ⟹ openin S U"
  shows "base_in S 𝒪 ⟷ (∀U. openin S U ⟶ (∀x∈U. ∃W∈𝒪. x ∈ W ∧ W ⊆ U))"
proof
  assume h:"base_in S 𝒪"
  show "∀U. openin S U ⟶ (∀x∈U. ∃W∈𝒪. x ∈ W ∧ W ⊆ U)"
  proof safe
    fix U x
    assume h':"openin S U" "x ∈ U"
    then obtain 𝒰 where hu: "U = ⋃𝒰" "𝒰 ⊆ 𝒪"
      using h by(auto simp: base_in_def)
    then obtain W where "x ∈ W" "W ∈ 𝒰"
      using h'(2) by blast
    thus "∃W∈𝒪. x ∈ W ∧ W ⊆ U"
      using hu by(auto intro!: bexI[where x=W])
  qed
next
  assume h:"∀U. openin S U ⟶ (∀x∈U. ∃W∈𝒪. x ∈ W ∧ W ⊆ U)"
  show "base_in S 𝒪"
    unfolding base_in_def
  proof safe
    fix U
    assume "openin S U"
    then have "∀x∈U. ∃W. W∈𝒪 ∧ x ∈ W ∧ W ⊆ U"
      using h by blast
    hence "∃W. ∀x∈U. W x ∈ 𝒪 ∧ x ∈ W x ∧ W x ⊆ U"
      by(rule bchoice)
    then obtain W where hw:
     "∀x∈U. W x ∈ 𝒪 ∧ x ∈ W x ∧ W x ⊆ U" by auto
    thus "∃𝒰. U = ⋃ 𝒰 ∧ 𝒰 ⊆ 𝒪"
      by(auto intro!: exI[where x="W ` U"])
  next
    fix U 𝒰
    show "𝒰 ⊆ 𝒪 ⟹ openin S (⋃ 𝒰)"
      using assms by auto
  qed
qed

lemma base_in_def2':
 "base_in S 𝒪 ⟷ (∀b∈𝒪. openin S b) ∧ (∀x. openin S x ⟶ (∃B'⊆𝒪. ⋃ B' = x))"
proof
  assume h:"base_in S 𝒪"
  show "(∀b∈𝒪. openin S b) ∧ (∀x. openin S x ⟶ (∃B'⊆𝒪. ⋃ B' = x))"
  proof(rule conjI)
    show "∀b∈𝒪. openin S b"
      using openin_base[OF h,of _ "{_}"] by auto
  next
    show "∀x. openin S x ⟶ (∃B'⊆𝒪. ⋃ B' = x)"
      using h by(auto simp: base_in_def)
  qed
next
  assume h:"(∀b∈𝒪. openin S b) ∧ (∀x. openin S x ⟶ (∃B'⊆𝒪. ⋃ B' = x))"
  show "base_in S 𝒪"
    unfolding base_in_def
  proof safe
    fix U
    assume "openin S U"
    then obtain B' where "B'⊆𝒪" "⋃ B' = U"
      using h by blast
    thus "∃𝒰. U = ⋃ 𝒰 ∧ 𝒰 ⊆ 𝒪"
      by(auto intro!: exI[where x=B'])
  next
    fix U 𝒰
    show "𝒰 ⊆ 𝒪 ⟹ openin S (⋃ 𝒰)"
      using h by auto
  qed
qed

corollary base_in_in_subset:
  assumes "base_in S 𝒪" "openin S u" "x ∈ u"
  shows "∃v∈𝒪. x ∈ v ∧ v ⊆ u"
  using assms base_in_def2 base_in_def2' by fastforce

lemma base_in_without_empty:
  assumes "base_in S 𝒪"
  shows "base_in S {U ∈ 𝒪. U ≠ {}}"
  unfolding base_in_def2'
proof safe
  fix x
  assume "x ∈ 𝒪" " ¬ openin S x"
  thus "⋀y. y ∈ {}"
    using base_in_openin[OF assms ‹x ∈ 𝒪›] by simp
next
  fix x
  assume "openin S x"
  then obtain B' where "B' ⊆𝒪" "⋃ B' = x"
    using assms by(simp add: base_in_def2') metis
  thus "∃B'⊆{U ∈ 𝒪. U ≠ {}}. ⋃ B' = x"
    by(auto intro!: exI[where x="{y ∈ B'. y ≠ {}}"])
qed

lemma second_countable_ex_without_empty:
  assumes "second_countable S"
  shows "∃𝒪. countable 𝒪 ∧ base_in S 𝒪 ∧ (∀U∈𝒪. U ≠ {})"
proof -
  obtain 𝒪 where "countable 𝒪" "base_in S 𝒪"
    using assms second_countable_base_in by blast
  thus ?thesis
    by(auto intro!: exI[where x="{U ∈ 𝒪. U ≠ {}}"] base_in_without_empty)
qed

lemma subtopology_subbase_in:
  assumes "subbase_in S 𝒪"
  shows "subbase_in (subtopology S T) {T ∩ U | U. U ∈ 𝒪}"
  using assms subtopology_generated_by
  by(auto simp: subbase_in_def)

lemma subtopology_base_in:
  assumes "base_in S 𝒪"
  shows "base_in (subtopology S T) {T ∩ U | U. U ∈ 𝒪}"
  unfolding base_in_def
proof
  fix L
  show "openin (subtopology S T) L = (∃𝒰. L = ⋃ 𝒰 ∧ 𝒰 ⊆ {T ∩ U |U. U ∈ 𝒪})"
  proof
    assume "openin (subtopology S T) L "
    then obtain T' where ht:
       "openin S T'" "L = T' ∩ T"
      by(auto simp: openin_subtopology)
    then obtain 𝒰 where hu:
      "T' = (⋃ 𝒰)" "𝒰 ⊆ 𝒪"
      using assms by(auto simp: base_in_def)
    show "∃𝒰. L = ⋃ 𝒰 ∧ 𝒰 ⊆ {T ∩ U |U. U ∈ 𝒪}"
      using hu ht by(auto intro!: exI[where x="{T ∩ U | U. U ∈ 𝒰}"])
  next
    assume "∃𝒰. L = ⋃ 𝒰 ∧ 𝒰 ⊆ {T ∩ U |U. U ∈ 𝒪}"
    then obtain 𝒰 where hu: "L = ⋃ 𝒰" "𝒰 ⊆ {T ∩ U |U. U ∈ 𝒪}"
      by auto
    hence "∀U∈𝒰. ∃U'∈𝒪. U = T ∩ U'" by blast
    then obtain k where hk:"⋀U. U ∈ 𝒰 ⟹ k U ∈ 𝒪" "⋀U. U ∈ 𝒰 ⟹ U = T ∩ k U"
      by metis
    hence "L =  ⋃ {T ∩ k U |U. U ∈ 𝒰}" 
      using hu by auto
    also have "... = ⋃ {k U |U. U ∈ 𝒰} ∩ T" by auto
    finally have 1:"L = ⋃ {k U |U. U ∈ 𝒰} ∩ T" .
    moreover have "openin S (⋃ {k U |U. U ∈ 𝒰})"
      using hu hk assms by(auto simp: base_in_def)
    ultimately show "openin (subtopology S T) L"
      by(auto intro!: exI[where x="⋃ {k U |U. U ∈ 𝒰}"] simp: openin_subtopology)
  qed
qed

lemma second_countable_subtopology:
  assumes "second_countable S"
  shows "second_countable (subtopology S T)"
proof -
  obtain 𝒪 where "countable 𝒪" "base_in S 𝒪"
    using assms second_countable_base_in by blast
  thus ?thesis
    by(auto intro!: exI[where x="{T ∩ U | U. U ∈ 𝒪}"] simp: second_countable_base_in Setcompr_eq_image dest: subtopology_base_in)
qed

lemma open_map_with_base:
  assumes "base_in S 𝒪" "⋀A. A ∈ 𝒪 ⟹ openin S' (f ` A)"
  shows "open_map S S' f"
  unfolding open_map_def
proof safe
  fix U
  assume "openin S U"
  then obtain 𝒰 where "U = ⋃𝒰" "𝒰 ⊆ 𝒪"
    using assms(1) by(auto simp: base_in_def)
  hence "f ` U = ⋃{ f ` A | A. A ∈ 𝒰}" by blast
  also have "openin S' ..."
    using assms(2) ‹𝒰 ⊆ 𝒪› by auto
  finally show "openin S' (f ` U)" .
qed

text ‹ Construct a base from a subbase.›

lemma finite'_intersection_of_idempot [simp]:
   "finite' intersection_of finite' intersection_of P = finite' intersection_of P"
proof
  fix A
  show "(finite' intersection_of finite' intersection_of P) A = (finite' intersection_of P) A"
  proof
    assume "(finite' intersection_of finite' intersection_of P) A"
    then obtain 𝒰 where 𝒰:"finite' 𝒰 ∧ 𝒰 ⊆ Collect (finite' intersection_of P) ∧ ⋂𝒰 = A"
      by(auto simp: intersection_of_def)
    hence "∀U∈𝒰. ∃𝒰'. finite' 𝒰' ∧ 𝒰' ⊆ Collect P ∧ ⋂𝒰' = U"
      by(auto simp: intersection_of_def)
    then obtain 𝒰' where 𝒰':
     "⋀U. U ∈ 𝒰 ⟹ finite' (𝒰' U)" "⋀U. U ∈ 𝒰 ⟹ 𝒰' U ⊆ Collect P" "⋀U. U ∈ 𝒰 ⟹ ⋂(𝒰' U) = U"
      by metis
    have 1: "⋂ (⋃ (𝒰' ` 𝒰)) = A"
      using  𝒰 𝒰'(3) by blast
    show "(finite' intersection_of P) A"
      unfolding intersection_of_def
      using 𝒰 𝒰'(1,2) 1 by(auto intro!: exI[where x="⋃U∈𝒰. 𝒰' U"])
  qed(rule finite'_intersection_of_inc)
qed

lemma finite'_intersection_of_countable:
  assumes "countable 𝒪"
  shows "countable (Collect (finite' intersection_of (λx. x ∈ 𝒪)))"
proof -
  have "Collect (finite' intersection_of (λx. x ∈ 𝒪)) = (⋃i∈{𝒪'. 𝒪' ≠ {} ∧ finite 𝒪' ∧ 𝒪' ⊆ 𝒪}. {⋂ i})"
    by(auto simp: intersection_of_def)
  also have "countable ..."
    using  countable_Collect_finite_subset[OF assms] 
    by(auto intro!: countable_UN[of "{ 𝒪'. 𝒪' ≠ {} ∧ finite 𝒪' ∧ 𝒪' ⊆ 𝒪}" "λ𝒪'. {⋂𝒪'}"])
      (auto intro!: countable_subset[of "{𝒪'. 𝒪' ≠ {} ∧ finite 𝒪' ∧ 𝒪' ⊆ 𝒪}" "{A. finite A ∧ A ⊆ 𝒪}"])
  finally show ?thesis .
qed

lemma finite'_intersection_of_openin:
  assumes "(finite' intersection_of (λx. x ∈ 𝒪)) U"
  shows "openin (topology_generated_by 𝒪) U"
  unfolding openin_topology_generated_by_iff
  using assms by(auto simp: generate_topology_on_eq arbitrary_union_of_inc)

lemma topology_generated_by_finite_intersections:
 "topology_generated_by 𝒪 = topology_generated_by (Collect (finite' intersection_of (λx. x ∈ 𝒪)))"
  unfolding topology_eq openin_topology_generated_by_iff by(simp add: generate_topology_on_eq)

lemma base_from_subbase:
  assumes "subbase_in S 𝒪"
  shows "base_in S (Collect (finite' intersection_of (λx. x ∈ 𝒪)))"
  unfolding subbase_in_def base_in_def assms[simplified subbase_in_def] openin_topology_generated_by_iff
  by(auto simp: arbitrary_def union_of_def generate_topology_on_eq)

lemma countable_base_from_countable_subbase:
  assumes "countable 𝒪" and "subbase_in S 𝒪"
  shows "second_countable S"
  using finite'_intersection_of_countable[OF assms(1)] base_from_subbase[OF assms(2)]
  by(auto simp: second_countable_base_in)

lemma prod_topology_second_countable:
  assumes "second_countable S" and "second_countable S'"
  shows "second_countable (prod_topology S S')"
proof -
  obtain 𝒪 𝒪' where ho:
   "countable 𝒪" "base_in S 𝒪" "countable 𝒪'" "base_in S' 𝒪'"
    using assms by(auto simp: second_countable_base_in)
  show ?thesis
  proof(rule countable_base_from_countable_subbase[where 𝒪="{ U × V | U V. U ∈ 𝒪 ∧ V ∈ 𝒪'}"])
    have "{U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒪'} = (λ(U,V). U × V) ` (𝒪 × 𝒪')"
      by auto
    also have "countable ..."
      using ho(1,3) by auto
    finally show "countable {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒪'}" .
  next
    show "subbase_in (prod_topology S S') {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒪'}"
      using base_is_subbase[OF ho(2)] base_is_subbase[OF ho(4)]
      by(simp add: subbase_in_def prod_topology_generated_by)
  qed
qed

text ‹ Abstract version of the theorem @{thm product_topology_countable_basis}.›
lemma product_topology_countable_base_in:
  assumes "countable I" and "⋀i. i ∈ I ⟹ second_countable (S i)"
  shows "∃𝒪'. countable 𝒪' ∧ base_in (product_topology S I) 𝒪' ∧
             (∀k ∈ 𝒪'. ∃X. k = (Π⇩E i∈I. X i) ∧ (∀i. openin (S i) (X i)) ∧ finite {i. X i ≠ topspace (S i)} ∧ {i. X i ≠ topspace (S i)} ⊆ I)"
proof -
  obtain 𝒪 where ho:
  "⋀i. i ∈ I ⟹ countable (𝒪 i)" "⋀i. i ∈ I ⟹ base_in (S i) (𝒪 i)"
    using assms(2)[simplified second_countable_base_in] by metis
  show ?thesis
    unfolding second_countable_base_in
  proof(intro exI[where x="{Π⇩E i∈I. U i | U. finite {i∈I. U i ≠ topspace (S i)} ∧ (∀i∈{i∈I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i)}"] conjI)
    show "countable {Π⇩E i∈I. U i | U. finite {i∈I. U i ≠ topspace (S i)} ∧ (∀i∈{i∈I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i)}"
         (is "countable ?X")
    proof -
      have "?X  = {Π⇩E i∈I. U i | U. finite {i∈I. U i ≠ topspace (S i)} ∧ (∀i∈{i∈I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i) ∧ (∀i ∈(UNIV- I). U i = {undefined})}"
           (is "_ = ?Y")
      proof (rule set_eqI)
        show "⋀x. x ∈ ?X ⟷ x ∈ ?Y"
        proof
          fix x
          assume "x ∈ ?X"
          then obtain U where hu:
         "x = (Π⇩E i∈I. U i)" "finite {i∈I. U i ≠ topspace (S i)}" "(∀i∈{i∈I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i)"
            by auto
          define U' where "U' i ≡ (if i ∈ I then U i else {undefined})" for i
          have "x = (Π⇩E i∈I. U' i)"
            using hu(1) by(auto simp: U'_def PiE_def extensional_def Pi_def)
          moreover have "finite {i∈I. U' i ≠ topspace (S i)}" "(∀i∈{i∈I. U' i ≠ topspace (S i)}. U' i ∈ 𝒪 i)" "∀i ∈(UNIV- I). U' i = {undefined}"
            using hu(2,3) by(auto simp: U'_def) (metis (mono_tags, lifting) Collect_cong)
          ultimately show "x ∈ ?Y" by auto
        qed auto
      qed
      also have "... = (λU. Π⇩E i∈I. U i) ` {U. finite {i∈I. U i ≠ topspace (S i)} ∧ (∀i∈{i∈I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i) ∧ (∀i ∈(UNIV- I). U i = {undefined})}" by auto
      also have "countable ..."
      proof(rule countable_image)
        have "{U. finite {i ∈ I. U i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i) ∧ (∀i∈UNIV - I. U i = {undefined})} = {U. ∃I'. finite I' ∧ I' ⊆ I ∧ (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈(I - I'). U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})}"
            (is "?A = ?B")
        proof (rule set_eqI)
          show "⋀x. x ∈ ?A ⟷ x ∈ ?B"
          proof
            fix U
            assume "U ∈ {U. finite {i ∈ I. U i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i) ∧ (∀i∈UNIV - I. U i = {undefined})}"
            then show "U ∈ {U. ∃I'. finite I' ∧ I' ⊆ I ∧ (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈I - I'. U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})}"
              by auto
          next
            fix U
            assume assm:"U ∈ {U. ∃I'. finite I' ∧ I' ⊆ I ∧ (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈I - I'. U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})}"
            then obtain I' where hi':
               "finite I'" "I' ⊆ I" "∀i∈I'. U i ∈ 𝒪 i" "∀i∈I - I'. U i = topspace (S i)" "∀i∈UNIV - I. U i = {undefined}"
              by auto
            then have "⋀i. i ∈ I ⟹ U i ≠ topspace (S i) ⟹ i ∈ I'" by auto
            hence "{i ∈ I. U i ≠ topspace (S i)} ⊆ I'" by auto
            hence "finite {i ∈ I. U i ≠ topspace (S i)}"
              using hi'(1) by (simp add: rev_finite_subset) 
            thus "U ∈ {U. finite {i ∈ I. U i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i) ∧ (∀i∈UNIV - I. U i = {undefined})}"
              using hi' by auto
          qed
        qed
        also have "... = (⋃I'∈{I'. finite I' ∧ I' ⊆ I}. {U. (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈I - I'. U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})})"
          by auto
        also have "countable ..."
        proof(rule countable_UN[OF countable_Collect_finite_subset[OF assms(1)]])
          fix I'
          assume "I' ∈ {I'. finite I' ∧ I' ⊆ I}"
          hence hi':"finite I'" "I' ⊆ I" by auto
          have "(λU i. if i ∈ I' then U i else undefined) ` {U. (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈I - I'. U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})} ⊆ (Π⇩E i∈I'. 𝒪 i)"
            by auto
          moreover have "countable ..."
            using hi' by(auto intro!: countable_PiE ho)
          ultimately have "countable ((λU i. if i ∈ I' then U i else undefined) ` {U. (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈I - I'. U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})})"
            by(simp add: countable_subset)
          moreover have "inj_on (λU i. if i ∈ I' then U i else undefined) {U. (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈I - I'. U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})}"
                        (is "inj_on ?f ?X")
          proof
            fix x y
            assume hxy: "x ∈ ?X" "y ∈ ?X" "?f x = ?f y"
            show "x = y"
            proof
              fix i
              consider "i ∈ I'" | "i ∈ I - I'" | "i ∈ UNIV - I"
                using hi'(2) by blast
              then show "x i = y i"
              proof cases
                case i:1
                then show ?thesis
                  using fun_cong[OF hxy(3),of i] by auto
              next
                case i:2
                then show ?thesis
                  using hxy(1,2) by auto
              next
                case i:3
                then show ?thesis
                  using hxy(1,2) by auto
              qed
            qed
          qed
          ultimately show "countable {U. (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈I - I'. U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})}"
            using countable_image_inj_on by auto
        qed
        finally show "countable {U. finite {i ∈ I. U i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i) ∧ (∀i∈UNIV - I. U i = {undefined})}" .
      qed
      finally show ?thesis .
    qed
  next
    show "base_in (product_topology S I) {Π⇩E i∈I. U i |U. finite {i ∈ I. U i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i)}"
         (is "base_in (product_topology S I) ?X")
      unfolding base_in_def
    proof safe
      fix U
      assume "openin (product_topology S I) U"
      then have "∀x∈U. ∃Ux. finite {i ∈ I. Ux i ≠ topspace (S i)} ∧ (∀i∈I. openin (S i) (Ux i)) ∧ x ∈ Pi⇩E I Ux ∧ Pi⇩E I Ux ⊆ U"
        by(simp add: openin_product_topology_alt)
      hence "∃Ux. ∀x∈U. finite {i ∈ I. Ux x i ≠ topspace (S i)} ∧ (∀i∈I. openin (S i) (Ux x i)) ∧ x ∈ Pi⇩E I (Ux x) ∧ Pi⇩E I (Ux x) ⊆ U"
        by(rule bchoice)
      then obtain Ux where hui:
       "⋀x. x ∈ U ⟹ finite {i ∈ I. Ux x i ≠ topspace (S i)}" "⋀x i. x ∈ U ⟹ i ∈ I ⟹ openin (S i) (Ux x i)" "⋀x. x ∈ U ⟹ x ∈ Pi⇩E I (Ux x)" "⋀x. x ∈ U ⟹ Pi⇩E I (Ux x) ⊆ U"
        by fastforce
      then have 1:"∀x∈U. ∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. ∃𝒰xj. 𝒰xj ⊆ 𝒪 i ∧ Ux x i = ⋃ 𝒰xj"
        using ho[simplified base_in_def] by (metis (no_types, lifting) mem_Collect_eq) 
      have "∀x∈U. ∃𝒰xj. ∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. 𝒰xj i ⊆ 𝒪 i ∧ Ux x i = ⋃ (𝒰xj i)"
        by(standard, rule bchoice) (use 1 in simp)
      hence "∃𝒰xj. ∀x∈U. ∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. 𝒰xj x i ⊆ 𝒪 i ∧ Ux x i = ⋃ (𝒰xj x i)"
        by(rule bchoice)
      then obtain 𝒰xj where
       "∀x∈U. ∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. 𝒰xj x i ⊆ 𝒪 i ∧ Ux x i = ⋃ (𝒰xj x i)"
        by auto
      hence huxj: "⋀x i. x ∈ U ⟹ i ∈ {i ∈ I. Ux x i ≠ topspace (S i)} ⟹ 𝒰xj x i ⊆ 𝒪 i"
                  "⋀x i. x ∈ U ⟹ i ∈ {i ∈ I. Ux x i ≠ topspace (S i)} ⟹ Ux x i = ⋃ (𝒰xj x i)"
        by blast+
      show "∃𝒰. U = ⋃ 𝒰 ∧ 𝒰 ⊆ ?X"
      proof(intro exI[where x="{Π⇩E i∈I. K i | K. ∃x∈U. finite {i ∈ I. Ux x i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. K i ∈ 𝒰xj x i) ∧ (∀i∈UNIV -{i ∈ I. Ux x i ≠ topspace (S i)}. K i = topspace (S i))}"] conjI)
        show "U = ⋃ {Π⇩E i∈I. K i | K. ∃x∈U. finite {i ∈ I. Ux x i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. K i ∈ 𝒰xj x i) ∧ (∀i∈UNIV -{i ∈ I. Ux x i ≠ topspace (S i)}. K i = topspace (S i))}"
        proof safe
          fix x
          assume hxu:"x ∈ U"
          have "∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. Ux x i = ⋃ (𝒰xj x i)"
            using huxj[OF hxu] by blast
          hence "∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. ∃Uxj. Uxj ∈ 𝒰xj x i ∧ x i ∈ Uxj"
            using hui(3)[OF hxu] by auto
          hence "∃Uxj. ∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. Uxj i ∈ 𝒰xj x i ∧ x i ∈ Uxj i"
            by(rule bchoice)
          then obtain Uxj where huxj':
             "⋀i. i ∈ {i ∈ I. Ux x i ≠ topspace (S i)} ⟹ Uxj i ∈ 𝒰xj x i"
             "⋀i. i ∈ {i ∈ I. Ux x i ≠ topspace (S i)} ⟹ x i ∈ Uxj i"
            by auto
          define K where "K ≡ (λi. if i ∈ {i ∈ I. Ux x i ≠ topspace (S i)} then Uxj i else topspace (S i))"
          have "x ∈ (Π⇩E i∈I. K i)"
            using huxj'(2) hui(3,4)[OF hxu] openin_subset[OF hui(2)[OF hxu]]
            by(auto simp: K_def PiE_def Pi_def)
          moreover have "∃x∈U. finite {i ∈ I. Ux x i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. K i ∈ 𝒰xj x i) ∧ (∀i∈UNIV -{i ∈ I. Ux x i ≠ topspace (S i)}. K i = topspace (S i))"
            by(rule bexI[OF _ hxu], rule conjI,simp add: hui(1)[OF hxu]) (use hui(2) hxu openin_subset huxj'(1)  K_def in auto)
          ultimately show "x ∈ ⋃ {Π⇩E i∈I. K i | K. ∃x∈U. finite {i ∈ I. Ux x i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. K i ∈ 𝒰xj x i) ∧ (∀i∈UNIV -{i ∈ I. Ux x i ≠ topspace (S i)}. K i = topspace (S i))}"
            by auto
        next
          fix x X K u
          assume  hu: "x ∈ (Π⇩E i∈I. K i)"  "u ∈ U" "finite {i ∈ I. Ux u i ≠ topspace (S i)}" "∀i∈{i ∈ I. Ux u i ≠ topspace (S i)}. K i ∈ 𝒰xj u i" "∀i∈UNIV -{i ∈ I. Ux u i ≠ topspace (S i)}. K i = topspace (S i)"            
          have "⋀i. i ∈ {i ∈ I. Ux u i ≠ topspace (S i)} ⟹ K i ⊆ Ux u i"
            using huxj[OF hu(2)] hu(4) by blast
          moreover have "⋀i. i ∈ I - {i ∈ I. Ux u i ≠ topspace (S i)} ⟹ K i = Ux u i"
            using hu(5) by auto
          ultimately have "⋀i. i ∈ I ⟹ K i ⊆ Ux u i"
            by blast
          thus "x ∈ U"
            using hui(4)[OF hu(2)] hu(1) by blast
        qed
      next
        show "{Π⇩E i∈I. K i | K. ∃x∈U. finite {i ∈ I. Ux x i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. K i ∈ 𝒰xj x i) ∧ (∀i∈UNIV -{i ∈ I. Ux x i ≠ topspace (S i)}. K i = topspace (S i))} ⊆ ?X"
        proof
          fix x
          assume "x ∈ {Π⇩E i∈I. K i | K. ∃x∈U. finite {i ∈ I. Ux x i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. K i ∈ 𝒰xj x i) ∧ (∀i∈UNIV -{i ∈ I. Ux x i ≠ topspace (S i)}. K i = topspace (S i))}"
          then obtain u K where hu:
           "x = (Π⇩E i∈I. K i)"  "u ∈ U" "finite {i ∈ I. Ux u i ≠ topspace (S i)}" "∀i∈{i ∈ I. Ux u i ≠ topspace (S i)}. K i ∈ 𝒰xj u i" "∀i∈UNIV -{i ∈ I. Ux u i ≠ topspace (S i)}. K i = topspace (S i)"
            by auto
          have hksubst:"{i ∈ I. K i ≠ topspace (S i)} ⊆ {i ∈ I. Ux u i ≠ topspace (S i)}"
            using hu(5) by fastforce
          hence "finite {i ∈ I. K i ≠ topspace (S i)}"
            using hu(3) by (simp add: finite_subset)
          moreover have "∀i∈{i ∈ I. K i ≠ topspace (S i)}. K i ∈ 𝒪 i"
            using huxj(1)[OF hu(2)] hu(4) hksubst
            by (meson subsetD)
          ultimately show "x ∈ ?X"
            using hu(1) by auto
        qed
      qed
    next
      fix 𝒰
      assume "𝒰 ⊆ ?X"
      have "openin (product_topology S I) u" if hu:"u ∈ 𝒰" for u
      proof -
        have hu': "u ∈ ?X"
          using ‹𝒰 ⊆ ?X› hu by auto
        then obtain U where hU:
       "u = (Π⇩E i∈I. U i)" "finite {i ∈ I. U i ≠ topspace (S i)}" "∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i"
          by auto
        define U' where "U' ≡ (λi. if i ∈ {i ∈ I. U i ≠ topspace (S i)} then U i else topspace (S i))"
        have hU': "u = (Π⇩E i∈I. U' i)"
          by(auto simp: hU(1) U'_def PiE_def Pi_def)
        have hUfinite : "finite {i. U' i ≠ topspace (S i)}"
          using hU(2) by(auto simp: U'_def)
        have hUoi: "∀i∈{i. U' i ≠ topspace (S i)}. U' i ∈ 𝒪 i"
          using hU(3) by(auto simp: U'_def)
        have hUi: "∀i∈{i. U' i ≠ topspace (S i)}. i ∈ I"
          using hU(2) by(auto simp: U'_def)
        have hallopen:"openin (S i) (U' i)" for i
        proof -
          consider "i ∈ {i. U' i ≠ topspace (S i)}" | "i ∉ {i. U' i ≠ topspace (S i)}" by auto
          then show ?thesis
          proof cases
            case 1
            then show ?thesis
              using hUoi ho(2)[of i] base_in_openin[of "S i" "𝒪 i" "U' i"] hUi
              by auto
          next
            case 2
            then have "U' i = topspace (S i)" by auto
            thus ?thesis by auto
          qed
        qed
        show "openin (product_topology S I) u"
          using hallopen hUfinite by(auto intro!: product_topology_basis simp: hU')
      qed
      thus "openin (product_topology S I) (⋃ 𝒰)"
        by auto
    qed
  next
    show "∀k∈{Pi⇩E I U |U. finite {i ∈ I. U i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i)}. ∃X. k = Pi⇩E I X ∧ (∀i. openin (S i) (X i)) ∧ finite {i. X i ≠ topspace (S i)} ∧ {i. X i ≠ topspace (S i)} ⊆ I"
    proof
      fix k
      assume "k ∈ {Pi⇩E I U |U. finite {i ∈ I. U i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i)}"
      then obtain U where hu:
         "k = (Π⇩E i∈I. U i)" "finite {i ∈ I. U i ≠ topspace (S i)}" "∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i"
        by auto
      define X where "X ≡ (λi. if i ∈ {i ∈ I. U i ≠ topspace (S i)} then U i else topspace (S i))"
      have hX1: "k = (Π⇩E i∈I. X i)"
        using hu(1) by(auto simp: X_def PiE_def Pi_def)
      have hX2: "openin (S i) (X i)" for i
        using hu(3) base_in_openin[of "S i" _ "U i",OF ho(2)]
        by(auto simp: X_def)
      have hX3: "finite {i. X i ≠ topspace (S i)}"
        using hu(2) by(auto simp: X_def)
      have hX4: "{i. X i ≠ topspace (S i)} ⊆ I"
        by(auto simp: X_def)
      show "∃X. k = (Π⇩E i∈I. X i) ∧ (∀i. openin (S i) (X i)) ∧ finite {i. X i ≠ topspace (S i)} ∧ {i. X i ≠ topspace (S i)} ⊆ I"
        using hX1 hX2 hX3 hX4 by(auto intro!: exI[where x=X])
    qed
  qed
qed

lemma product_topology_second_countable:
  assumes "countable I" and "⋀i. i ∈ I ⟹ second_countable (S i)"
  shows "second_countable (product_topology S I)"
  using product_topology_countable_base_in[OF assms(1)] assms(2)
  by(fastforce simp: second_countable_base_in)

lemma second_countable_euclidean[simp]:
 "second_countable (euclidean :: 'a :: second_countable_topology topology)"
  using ex_countable_basis second_countable_def topological_basis_def by fastforce

lemma Cantor_Bendixon:
  assumes "second_countable X"
  shows "∃U P. countable U ∧ openin X U ∧ perfect_set X P ∧ U ∪ P = topspace X ∧ U ∩ P = {} ∧ (∀a≠{}. openin (subtopology X P) a ⟶ uncountable a)"
proof -
  obtain 𝒪 where o: "countable 𝒪" "base_in X 𝒪"
    using assms by(auto simp: second_countable_base_in)
  define U where "U ≡ ⋃ {u∈𝒪. countable u}"
  define P where "P ≡ topspace X - U"
  have 1: "countable U"
    using o(1) by(auto simp: U_def intro!: countable_UN[of _ id,simplified])
  have 2: "openin X U"
    using base_in_openin[OF o(2)] by(auto simp: U_def)
  have openin_c:"countable v ⟷ v ⊆ U" if "openin X v" for v
  proof
    assume "countable v"
    obtain 𝒰 where "v = ⋃𝒰" "𝒰 ⊆ 𝒪"
      using ‹openin X v› o(2) by(auto simp: base_in_def)
    with ‹countable v› have "⋀u. u ∈ 𝒰 ⟹ countable u"
      by (meson Sup_upper countable_subset)
    thus "v ⊆ U"
      using ‹𝒰 ⊆ 𝒪› by(auto simp: ‹v = ⋃𝒰› U_def)
  qed(rule countable_subset[OF _ 1])
  have 3: "perfect_set X P"
  proof(rule perfect_setI)
    fix x T
    assume h:"x ∈ P" "x ∈ T" "openin X T"
    have T_unc:"uncountable T"
      using openin_c[OF h(3)] h(1,2) by(auto simp: P_def)
    obtain 𝒰 where U:"T = ⋃𝒰" "𝒰 ⊆ 𝒪"
      using h(3) o(2) by(auto simp: base_in_def)
    then obtain u where u:"u ∈ 𝒰" "uncountable u"
      using T_unc U_def h(3) openin_c by auto
    hence "uncountable (u - {x})" by simp
    hence "¬ (u - {x} ⊆ U)"
      using 1 by (metis countable_subset) 
    then obtain y where "y ∈ u - {x}" "y ∉ U"
      by blast
    thus "∃y. y ≠ x ∧ y ∈ T ∧ y ∈ P"
      using U u base_in_subset[OF o(2),of u] by(auto intro!: exI[where x=y] simp:P_def)
  qed(use 2 P_def in auto)
  have 4 : "uncountable a" if "openin (subtopology X P) a" "a ≠ {}" for a
  proof
    assume contable:"countable a"
    obtain b where b: "openin X b" "a = P ∩ b"
      using ‹openin (subtopology X P) a› by(auto simp: openin_subtopology)
    hence "uncountable b"
      using P_def openin_c that(2) by auto
    thus False
      by (metis 1 Diff_Int_distrib2 Int_absorb1 P_def b(1) b(2) contable countable_Int1 openin_subset uncountable_minus_countable)
  qed
  show ?thesis
    using 1 2 3 4 by(auto simp: P_def)
qed

subsubsection ‹ Separable Spaces ›
definition dense_in :: "['a topology, 'a set] ⇒ bool" where
"dense_in S U ⟷ (U ⊆ topspace S ∧ (∀V. openin S V ⟶ V ≠ {} ⟶ U ∩ V ≠ {}))"

lemma dense_in_def2:
 "dense_in S U ⟷ (U ⊆ topspace S ∧ (S closure_of U) = topspace S)"
  using dense_intersects_open by(auto simp: dense_in_def closure_of_subset_topspace in_closure_of) auto

lemma dense_in_topspace[simp]: "dense_in S (topspace S)"
  by(auto simp: dense_in_def2)

lemma dense_in_subset:
  assumes "dense_in S U"
  shows "U ⊆ topspace S"
  using assms by(simp add: dense_in_def)

lemma dense_in_nonempty:
  assumes "topspace S ≠ {}" "dense_in S U"
  shows "U ≠ {}"
  using assms by(auto simp: dense_in_def)

lemma dense_inI:
  assumes "U ⊆ topspace S"
      and "⋀V. openin S V ⟹ V ≠ {} ⟹ U ∩ V ≠ {}"
    shows "dense_in S U"
  using assms by(auto simp: dense_in_def)

lemma dense_in_infinite:
  assumes "t1_space X" "infinite (topspace X)" "dense_in X U"
  shows "infinite U"
proof
  assume fin: "finite U"
  then have "closedin X U"
    by (metis assms(1,3) dense_in_def t1_space_closedin_finite)
  hence "X closure_of U = U"
    by (simp add: closure_of_eq)
  thus False
    by (metis assms(2) assms(3) dense_in_def2 fin)
qed

lemma dense_in_prod:
  assumes "dense_in S U" and "dense_in S' U'"
  shows "dense_in (prod_topology S S') (U × U')"
proof(rule dense_inI)
  fix V
  assume h:"openin (prod_topology S S') V" "V ≠ {}"
  then obtain x y where hxy:"(x,y) ∈ V" by auto
  then obtain V1 V2 where hv12:
  "openin S V1" "openin S' V2" "x ∈ V1" "y ∈ V2" "V1 × V2 ⊆ V"
    using h(1) openin_prod_topology_alt[of S S' V] by blast
  hence "V1 ≠ {}" "V2 ≠ {}" by auto
  hence "U ∩ V1 ≠ {}" "U' ∩ V2 ≠ {}"
    using assms hv12 by(auto simp: dense_in_def)
  thus "U × U' ∩ V ≠ {}"
    using hv12 by auto
next
  show "U × U' ⊆ topspace (prod_topology S S')"
    using assms by(auto simp add: dense_in_def)
qed

lemma separable_space_def2:"separable_space S ⟷ (∃U. countable U ∧ dense_in S U)"
  by(auto simp: separable_space_def dense_in_def2)

lemma countable_space_separable_space:
  assumes "countable (topspace S)"
  shows "separable_space S"
  using assms by(auto simp: separable_space_def2 intro!: exI[where x="topspace S"])

lemma separable_space_prod:
  assumes "separable_space S" and "separable_space S'"
  shows "separable_space (prod_topology S S')"
proof -
  obtain U U' where
    "countable U" "dense_in S U" "countable U'" "dense_in S' U'"
    using assms by(auto simp: separable_space_def2)
  thus ?thesis
    by(auto intro!: exI[where x="U×U'"] dense_in_prod simp: separable_space_def2)
qed

lemma dense_in_product:
  assumes "⋀i. i ∈ I ⟹ dense_in (T i) (U i)"
  shows "dense_in (product_topology T I) (Π⇩E i∈I. U i)"
proof(rule dense_inI)
  fix V
  assume h:"openin (product_topology T I) V" "V ≠ {}"
  then obtain x where hx:"x ∈ V" by auto
  then obtain K where hk:
   "finite {i ∈ I. K i ≠ topspace (T i)}" "∀i∈I. openin (T i) (K i)" "x ∈ (Π⇩E i∈I. K i)" "(Π⇩E i∈I. K i) ⊆ V"
    using h(1) openin_product_topology_alt[of T I V] by auto
  hence "⋀i. i ∈ I ⟹ K i ≠ {}" by auto
  hence "⋀i. i ∈ I ⟹ U i ∩ K i ≠ {}"
    using assms hk by(auto simp: dense_in_def)
  hence "(Π⇩E i∈I. U i) ∩ (Π⇩E i∈I. K i) ≠ {}"
    by (simp add: PiE_Int PiE_eq_empty_iff) 
  thus "(Π⇩E i∈I. U i) ∩ V ≠ {}"
    using hk by auto
next
  show "(Π⇩E i∈I. U i) ⊆ topspace (product_topology T I)"
    using assms by(auto simp: dense_in_def)
qed

lemma separable_countable_product:
  assumes "countable I" and "⋀i. i ∈ I ⟹ separable_space (T i)"
  shows "separable_space (product_topology T I)"
proof -
  consider "∃i∈I. T i = trivial_topology" | "⋀i. i ∈ I ⟹ T i ≠ trivial_topology"
    by auto
  thus ?thesis
  proof cases
    case 1
    then obtain i where i:"i ∈ I" "topspace (T i) = {}"
      by auto
    show ?thesis
      unfolding separable_space_def2 dense_in_def
    proof(intro exI[where x="{}"] conjI)
      show "∀V. openin (product_topology T I) V ⟶ V ≠ {} ⟶ {} ∩ V ≠ {}"
      proof safe
        fix V x
        assume h: "openin (product_topology T I) V" "x ∈ V"
        from i have "(product_topology T I) = trivial_topology"
          using product_topology_trivial_iff by auto
        with h(1) have "V = {}"
          by simp
        thus "x ∈ {}"
          using h(2) by auto
      qed
    qed auto
  next
    case 2
    then have "∃x. ∀i∈I. x i ∈ topspace (T i)" "∃U. ∀i∈I. countable (U i) ∧ dense_in (T i) (U i)"
      using assms(2) by(auto intro!: bchoice simp: separable_space_def2 ex_in_conv)
    then obtain x U where hxu:
     "⋀i. i ∈ I ⟹ x i ∈ topspace (T i)" "⋀i. i ∈ I ⟹ countable (U i)" "⋀i. i ∈ I ⟹ dense_in (T i) (U i)"
      by auto
    define U' where "U' ≡ (λJ i. if i ∈ J then U i else {x i})"
    show ?thesis
      unfolding separable_space_def2
    proof(intro exI[where x="⋃{Π⇩E i∈I. U' J i | J. finite J ∧ J ⊆ I}"] conjI)
      have "(⋃{ Π⇩E i∈I. U' J i | J. finite J ∧ J ⊆ I}) = (⋃ ((λJ. Π⇩E i∈I. U' J i) ` {J. finite J ∧ J ⊆ I}))"
        by auto
      also have "countable ..."
      proof(rule countable_UN)
        fix J
        assume hj:"J ∈ {J. finite J ∧ J ⊆ I}"
        have "inj_on (λf. (λi∈J. f i, λi∈(I-J). f i)) (Π⇩E i∈I. U' J i)"
        proof(rule inj_onI)
          fix f g
          assume h:"f ∈ Pi⇩E I (U' J)" "g ∈ Pi⇩E I (U' J)"
                   "(restrict f J, restrict f (I - J)) = (restrict g J, restrict g (I - J))"
          then have "⋀i. i ∈ J ⟹ f i = g i" "⋀i. i ∈(I-J) ⟹ f i = g i"
             by(auto simp: restrict_def) meson+
          thus "f = g"
            using h(1,2) by(auto simp: U'_def) (meson PiE_ext)
        qed
        moreover have "countable ((λf. (λi∈J. f i, λi∈(I-J). f i)) ` (Π⇩E i∈I. U' J i))" (is "countable ?K")
        proof -
          have 1:"?K ⊆ (Π⇩E i∈J. U i) × (Π⇩E i∈(I-J). {x i})"
            using hj by(auto simp: U'_def PiE_def Pi_def)
          have 2:"countable ..."
          proof(rule countable_SIGMA)
            show "countable (Pi⇩E J U)"
              using hj hxu(2) by(auto intro!: countable_PiE)
          next
            have "(Π⇩E i∈I - J. {x i}) = { λi∈I-J. x i }"
              by(auto simp: PiE_def extensional_def restrict_def Pi_def)
            thus "countable (Π⇩E i∈I - J. {x i})"
              by simp
          qed
          show ?thesis
            by(rule countable_subset[OF 1 2])
        qed
        ultimately show "countable (Π⇩E i∈I. U' J i)"
          by(simp add: countable_image_inj_eq)
      qed(rule countable_Collect_finite_subset[OF assms(1)])
      finally show "countable (⋃{ Π⇩E i∈I. U' J i | J. finite J ∧ J ⊆ I})" .
    next
      show "dense_in (product_topology T I) (⋃ {Π⇩E i∈I. U' J i |J. finite J ∧ J ⊆ I})"
      proof(rule dense_inI)
        fix V
        assume h:"openin (product_topology T I) V" "V ≠ {}"
        then obtain y where hx:"y ∈ V" by auto
        then obtain K where hk:
         "finite {i ∈ I. K i ≠ topspace (T i)}" "⋀i. i∈I ⟹ openin (T i) (K i)" "y ∈ (Π⇩E i∈I. K i)" "(Π⇩E i∈I. K i) ⊆ V"
          using h(1) openin_product_topology_alt[of T I V] by auto
        hence 3:"⋀i. i ∈ I ⟹ K i ≠ {}" by auto
        hence 4:"i ∈ {i ∈ I. K i ≠ topspace (T i)} ⟹ K i ∩ U' {i ∈ I. K i ≠ topspace (T i)} i ≠ {}" for i
          using hxu(3)[of i] hk(2)[of i] by(auto simp: U'_def dense_in_def)
        have "∃z. ∀i∈{i ∈ I. K i ≠ topspace (T i)}. z i ∈ K i ∩ U' {i ∈ I. K i ≠ topspace (T i)} i"
          by(rule bchoice) (use 4 in auto)
        then obtain z where hz: "∀i∈{i ∈ I. K i ≠ topspace (T i)}. z i ∈ K i ∩ U' {i ∈ I. K i ≠ topspace (T i)} i"
          by auto          
        have 5: "i ∉ {i ∈ I. K i ≠ topspace (T i)} ⟹ i ∈ I ⟹ x i ∈ K i" for i
          using hxu(1)[of i] by auto
        have "(λi. if i ∈ {i ∈ I. K i ≠ topspace (T i)} then z i else if i ∈ I then x i else undefined) ∈ (Π⇩E i∈I. U' {i ∈ I. K i ≠ topspace (T i)} i) ∩ (Π⇩E i∈I. K i)"
          using 4 5 hz by(auto simp: U'_def)
        thus "⋃ {Pi⇩E I (U' J) |J. finite J ∧ J ⊆ I} ∩ V ≠ {}"
          using hk(1,4) by blast
      next
        have "⋀J. J ⊆ I ⟹ (Π⇩E i∈I. U' J i) ⊆ topspace (product_topology T I)"
          using hxu by(auto simp: dense_in_def U'_def PiE_def Pi_def) (metis subsetD)
        thus "(⋃ {Π⇩E i∈I. U' J i |J. finite J ∧ J ⊆ I}) ⊆ topspace (product_topology T I)"
          by auto
      qed
    qed
  qed
qed

lemma separable_finite_product:
  assumes "finite I" and "⋀i. i ∈ I ⟹ separable_space (T i)"
  shows "separable_space (product_topology T I)"
  using separable_countable_product[OF countable_finite[OF assms(1)]] assms by auto

subsubsection ‹ $G_{\delta}$ Set ›
lemma gdelta_inD:
  assumes "gdelta_in S A"
  shows "∃𝒰. 𝒰 ≠ {} ∧ countable 𝒰 ∧ (∀b∈𝒰. openin S b) ∧ A = ⋂ 𝒰"
  using assms unfolding gdelta_in_def relative_to_def intersection_of_def
  by (metis IntD1 Int_insert_right_if1 complete_lattice_class.Inf_insert countable_insert empty_not_insert inf.absorb_iff2 mem_Collect_eq openin_topspace)

lemma gdelta_inD':
  assumes "gdelta_in S A"
  shows "∃U. (∀n::nat. openin S (U n)) ∧ A = ⋂ (range U)"
proof-
  obtain 𝒰 where h:"𝒰 ≠ {}" "countable 𝒰" "⋀b. b∈𝒰 ⟹ openin S b" "A = ⋂ 𝒰"
    using gdelta_inD[OF assms] by metis
  show ?thesis
    using range_from_nat_into[OF h(1,2)] h(3,4)
    by(auto intro!: exI[where x="from_nat_into 𝒰"])
qed

lemma gdelta_in_continuous_map:
  assumes "continuous_map X Y f" "gdelta_in Y a"
  shows "gdelta_in X (f -` a ∩ topspace X)"
proof -
  obtain Ua where u:
  "Ua ≠ {}" "countable Ua" "⋀b. b ∈ Ua ⟹ openin Y b" "a = ⋂ Ua"
    using gdelta_inD[OF assms(2)] by metis
  then have 0:"f -` a ∩ topspace X = ⋂ {f -` b ∩ topspace X|b. b ∈ Ua}"
    by auto
  have 1: "{f -` b ∩ topspace X |b. b ∈ Ua} ≠ {}"
    using u(1) by simp
  have 2:"countable {f -` b ∩ topspace X|b. b ∈ Ua}"
    using u by (simp add: Setcompr_eq_image)
  have 3:"⋀c. c ∈ {f -` b ∩ topspace X|b. b ∈ Ua} ⟹ openin X c"
    using assms u(3) by blast
  show ?thesis
    by (metis (mono_tags, lifting) "0" "1" "2" "3" gdelta_in_Inter open_imp_gdelta_in)
qed

lemma g_delta_of_inj_open_map:
  assumes "open_map X Y f" "inj_on f (topspace X)" "gdelta_in X a"
  shows "gdelta_in Y (f ` a)"
proof -
  obtain Ua where u:
  "Ua ≠ {}" "countable Ua" "⋀b. b ∈ Ua ⟹ openin X b" "a = ⋂ Ua"
    using gdelta_inD[OF assms(3)] by metis
  then obtain j where "j ∈ Ua" by auto
  have "f ` a = f ` ⋂ Ua" by(simp add: u(4))
  also have "... = ⋂ ((`) f ` Ua)"
    using u openin_subset by(auto intro!: image_INT[OF assms(2) _ ‹j ∈ Ua›,of id,simplified])
  also have "... = ⋂ {f ` u|u. u ∈ Ua}" by auto
  finally have 0: "f ` a = ⋂ {f ` u |u. u ∈ Ua}" .
  have 1:"{f ` u |u. u ∈ Ua} ≠ {}"
    using u(1) by auto
  have 2:"countable {f ` u |u. u ∈ Ua}"
    using u(2) by (simp add: Setcompr_eq_image)
  have 3: "⋀c. c ∈ {f ` u |u. u ∈ Ua} ⟹ openin Y c"
    using assms(1) u(3) by(auto simp: open_map_def)
  show ?thesis
    by (metis (no_types, lifting) "0" "1" "2" "3" gdelta_in_Inter open_imp_gdelta_in)
qed

lemma gdelta_in_prod:
  assumes "gdelta_in X A" "gdelta_in Y B"
  shows "gdelta_in (prod_topology X Y) (A × B)"
proof -
  obtain Ua Ub where hu:
  "Ua ≠ {}" "countable Ua" "⋀b. b ∈ Ua ⟹ openin X b" "A = ⋂ Ua"
  "Ub ≠ {}" "countable Ub" "⋀b. b ∈ Ub ⟹ openin Y b" "B = ⋂ Ub"
    by (meson gdelta_inD assms) 
  then have 0:"A × B = ⋂ {a × b | a b. a ∈ Ua ∧ b ∈ Ub}" by blast
  have 1: "{a × b | a b. a ∈ Ua ∧ b ∈ Ub} ≠ {}"
    using hu(1,5) by auto
  have 2: "countable {a × b | a b. a ∈ Ua ∧ b ∈ Ub}"
  proof -
    have "countable ((λ(x, y). x × y) ` (Ua × Ub))"
      using hu(2,6) by(auto intro!: countable_image[of "Ua × Ub" "λ(x,y). x × y"])
    moreover have "... = {a × b | a b. a ∈ Ua ∧ b ∈ Ub}" by auto
    ultimately show ?thesis by simp
  qed
  have 3: "⋀c. c ∈ {a × b | a b. a ∈ Ua ∧ b ∈ Ub} ⟹ openin (prod_topology X Y) c"
    using hu(3,7) by(auto simp: openin_prod_Times_iff)
  show ?thesis
    by (metis (no_types, lifting) gdelta_in_Inter open_imp_gdelta_in 0 1 2 3)
qed

corollary gdelta_in_prod1:
  assumes "gdelta_in X A"
  shows "gdelta_in (prod_topology X Y) (A × topspace Y)"
  by(auto intro!: gdelta_in_prod assms)

corollary gdelta_in_prod2:
  assumes "gdelta_in Y B"
  shows "gdelta_in (prod_topology X Y) (topspace X × B)"
  by(auto intro!: gdelta_in_prod assms)

lemma continuous_map_imp_closed_graph':
  assumes "continuous_map X Y f" "Hausdorff_space Y"
  shows "closedin (prod_topology Y X) ((λx. (f x,x)) ` topspace X)"
  using assms closed_map_def closed_map_paired_continuous_map_left by blast

subsubsection ‹ Continuous Maps on First Countable Topology›
text ‹ Generalized version of @{thm Metric_space.eventually_atin_sequentially}›
lemma eventually_atin_sequentially:
  assumes "first_countable X"
  shows "eventually P (atin X a) ⟷ (∀σ. range σ ⊆ topspace X - {a} ∧ limitin X σ a sequentially ⟶ eventually (λn. P (σ n)) sequentially)"
proof safe
  fix an
  assume h:"eventually P (atin X a)" "range an ⊆ topspace X - {a}" "limitin X an a sequentially"
  then obtain U where U: "openin X U" "a ∈ U" "∀x∈U - {a}. P x"
    by (auto simp: eventually_atin limitin_topspace)
  with h(3) obtain N where "∀n≥N. an n ∈ U"
    by (meson limitin_sequentially)
  with U(3) h(2) show "∀⇩F n in sequentially. P (an n)"
    unfolding eventually_sequentially by blast
next
  assume h:"∀an. range an ⊆ topspace X - {a} ∧ limitin X an a sequentially ⟶ (∀⇩F n in sequentially. P (an n))"
  consider "a ∉ topspace X" | "a ∈ topspace X"
    by blast
  then show "eventually P (atin X a)"
  proof cases
    assume a:"a ∈ topspace X"
    from a assms obtain B' where B': "countable B'" "⋀V. V ∈ B' ⟹ openin X V" "⋀U. openin X U ⟹ a ∈ U ⟹ (∃V ∈ B'. a ∈ V ∧ V ⊆ U)"
      by(fastforce simp: first_countable_def)
    define B where "B ≡ {V∈B'. a ∈ V}"
    have B:"⋀V. V ∈ B ⟹ openin X V" "countable B" "B ≠ {}"  "⋀U. openin X U ⟹ a ∈ U ⟹ (∃V ∈ B. a ∈ V ∧ V ⊆ U)"
      using B' B'(3)[OF _ a] by(fastforce simp: B_def)+
    define An where "An ≡ (λn. ⋂i≤n. from_nat_into B i)"
    have a_in_An:"a ∈ An n" for n
      by (metis (no_types, lifting) An_def B_def B(3) INT_I from_nat_into mem_Collect_eq)
    have openAn:"⋀n. openin X (An n)"
      using B by(auto simp: An_def from_nat_into[OF B(3)] openin_Inter)
    have deqseq_An:"decseq An"
      by(fastforce simp: decseq_def An_def)
    have "∃U. openin X U ∧ a ∈ U ∧ Ball (U - {a}) P"
    proof(rule ccontr)
      assume "∄U. openin X U ∧ a ∈ U ∧ Ball (U - {a}) P"
      then have "⋀U. openin X U ⟹ a ∈ U ⟹ ∃x ∈ U - {a}. ¬ P x"
        by blast
      hence "∃b∈An n - {a}. ¬ P b" for n
        using openAn a_in_An by auto
      then obtain an where an: "⋀n. an n ∈ An n" "⋀n. an n ≠ a" "⋀n. ¬ P (an n)"
        by (metis Diff_iff singletonI)
      have "limitin X an a sequentially"
        unfolding limitin_sequentially
      proof safe
        fix U
        assume "openin X U" "a ∈ U"
        then obtain V where V:"a ∈ V" "V ⊆ U" "V ∈ B"
          using B by meson
        then obtain N where "V = from_nat_into B N"
          by (metis B(2) from_nat_into_surj)
        hence "⋀n. n ≥ N ⟹ an n ∈ V"
          using an(1) An_def by blast
        thus "∃N. ∀n≥N. an n ∈ U"
          using V by blast
      qed fact
      hence 1:"∀⇩F n in sequentially. P (an n)"
        using an(2) h an(1) openin_subset[OF openAn] by blast
      thus False
        using an(3) by simp
    qed
    thus ?thesis
      by(simp add: eventually_atin)
  qed(auto simp: eventually_atin)
qed

lemma continuous_map_iff_limit_seq:
  assumes "first_countable X"
  shows "continuous_map X Y f ⟷ (∀xn x. limitin X xn x sequentially ⟶ limitin Y (λn. f (xn n)) (f x) sequentially)"
  unfolding continuous_map_atin
proof safe
  fix xn x
  assume h:"∀x∈topspace X. limitin Y f (f x) (atin X x)" "limitin X xn x sequentially"
  then have limfx: "limitin Y f (f x) (atin X x)"
    by(simp add: limitin_topspace)
  show "limitin Y (λn. f (xn n)) (f x) sequentially"
    unfolding limitin_sequentially
  proof safe
    fix U
    assume U:"openin Y U" "f x ∈ U"
    then have h':"⋀σ. range σ ⊆ topspace X - {x} ⟹ x ∈ topspace X ⟹ limitin X σ x sequentially ⟹ (∃N. ∀n≥N. f (σ n) ∈ U)"
      using limfx by(auto simp: limitin_def eventually_atin_sequentially[OF assms(1)] eventually_sequentially)
    show "∃N. ∀n≥N. f (xn n) ∈ U"
    proof(cases "finite {n. xn n ≠ x}")
      assume "finite {n. xn n ≠ x}"
      then obtain N where "⋀n. n ≥ N ⟹ xn n = x"
        using infinite_nat_iff_unbounded_le by blast
      then show ?thesis
        using U by auto
    next
      assume inf:"infinite {n. xn n ≠ x}"
      obtain n0 where n0:"⋀n. n ≥ n0 ⟹ xn n ∈ topspace X"
        by (meson h(2) limitin_sequentially openin_topspace)
      have inf':"infinite ({n. xn n ≠ x} ∩ {n0..})"
      proof
        have 1:"({n. xn n ≠ x} ∩ {n0..}) ∪ ({n. xn n ≠ x} ∩ {..<n0}) = {n. xn n ≠ x}"
          by auto
        assume "finite ({n. xn n ≠ x} ∩ {n0..})"
        then have "finite (({n. xn n ≠ x} ∩ {n0..}) ∪ ({n. xn n ≠ x} ∩ {..<n0}))"
          by auto
        with inf show False
          unfolding 1 by blast
      qed
      define a where "a ≡ enumerate ({n. xn n ≠ x} ∩ {n0..})"
      have a: "strict_mono a" "range a = ({n. xn n ≠ x} ∩ {n0..})"
        using range_enumerate[OF inf'] strict_mono_enumerate[OF inf']
        by(auto simp: a_def)
      have "∃N. ∀n≥N. f (xn (a n)) ∈ U"
        using limitin_subsequence[OF a(1) h(2)] a(2) n0
        by(auto intro!: h' limitin_topspace[OF h(2)] simp: comp_def)
      then obtain N where N:"⋀n. n ≥ N ⟹ f (xn (a n)) ∈ U"
        by blast
      show "∃N. ∀n≥N. f (xn n) ∈ U"
      proof(auto intro!: exI[where x="a N"])
        fix n
        assume n:"n ≥ a N"
        show "f (xn n) ∈ U"
        proof (cases "xn n = x")
          assume "xn n ≠ x"
          moreover have "n0 ≤ n"
            using seq_suble[OF a(1),of N] n a(2)
            by (metis Int_Collect atLeast_def dual_order.trans rangeI)
          ultimately obtain n1 where n1:"n = a n1"
            by (metis (mono_tags, lifting) Int_Collect atLeast_def imageE mem_Collect_eq a(2))
          have "n1 ≥ N"
            using strict_mono_less_eq[OF a(1),of N n1] n by(simp add: n1)
          thus ?thesis
            by(auto intro!: N simp: n1)
        qed(auto simp: U)
      qed
    qed
  qed(auto intro!: limitin_topspace limfx)
next
  fix x
  assume h:"∀xn x. limitin X xn x sequentially ⟶ limitin Y (λn. f (xn n)) (f x) sequentially" "x ∈ topspace X"
  then have "f x ∈ topspace Y"
    by (meson Abstract_Limits.limitin_const_iff limitin_topspace)
  thus "limitin Y f (f x) (atin X x)"
    using h by(auto simp: eventually_atin_sequentially[OF assms(1)] limitin_def )
qed

subsubsection ‹ Upper-Semicontinuous Functions ›
definition upper_semicontinuous_map :: "['a topology, 'a ⇒ 'b :: linorder_topology] ⇒ bool" where
"upper_semicontinuous_map X f ⟷ (∀a. openin X {x∈topspace X. f x < a})"

lemma continuous_upper_semicontinuous:
  assumes "continuous_map X (euclidean :: ('b :: linorder_topology) topology) f"
  shows "upper_semicontinuous_map X f"
  unfolding upper_semicontinuous_map_def
proof safe
  fix a :: 'b
  have *:"openin euclidean U ⟹ openin X {x ∈ topspace X. f x ∈ U}" for U
    using assms by(simp add: continuous_map)
  have "openin euclidean {..<a}" by auto
  with *[of "{..<a}"] show "openin X {x ∈ topspace X. f x < a}" by auto
qed

lemma upper_semicontinuous_map_iff_closed:
 "upper_semicontinuous_map X f ⟷ (∀a. closedin X {x∈topspace X. f x ≥ a})"
proof -
  have "{x ∈ topspace X. f x < a} = topspace X - {x ∈ topspace X. f x ≥ a}" for a
    by auto
  thus ?thesis
    by (simp add: closedin_def upper_semicontinuous_map_def)
qed

lemma upper_semicontinuous_map_real_iff:
  fixes f :: "'a ⇒ real"
  shows "upper_semicontinuous_map X f ⟷ upper_semicontinuous_map X (λx. ereal (f x))"
  unfolding upper_semicontinuous_map_def
proof safe
  fix a :: ereal
  assume h:"∀a::real. openin X {x ∈ topspace X. f x < a}"
  consider "a = - ∞" | "a = ∞" | "a ≠ - ∞ ∧ a ≠ ∞" by auto
  then show "openin X {x ∈ topspace X. ereal (f x) < a}"
  proof cases
    case 3
    then have "ereal (f x) < a ⟷ f x < real_of_ereal a" for x
      by (metis ereal_less_eq(3) linorder_not_less real_of_ereal.elims)
    thus ?thesis
      using h by simp
  qed simp_all
next
  fix a :: real
  assume h:"∀a::ereal. openin X {x ∈ topspace X. ereal (f x) < a}"
  then have "openin X {x ∈ topspace X. ereal (f x) < ereal a}"
    by blast
  moreover have"ereal (f x) < real_of_ereal a ⟷ f x < a" for x
    by auto
  ultimately show "openin X {x ∈ topspace X. f x < a}" by auto
qed

subsubsection ‹ Lower-Semicontinuous Functions ›
definition lower_semicontinuous_map :: "['a topology, 'a ⇒ 'b :: linorder_topology] ⇒ bool" where
"lower_semicontinuous_map X f ⟷ (∀a. openin X {x∈topspace X. a < f x})"

lemma continuous_lower_semicontinuous:
  assumes "continuous_map X (euclidean :: ('b :: linorder_topology) topology) f"
  shows "lower_semicontinuous_map X f"
  unfolding lower_semicontinuous_map_def
proof safe
  fix a :: 'b
  have *:"openin euclidean U ⟹ openin X {x ∈ topspace X. f x ∈ U}" for U
    using assms by(simp add: continuous_map)
  have "openin euclidean {a<..}" by auto
  with *[of "{a<..}"] show "openin X {x ∈ topspace X. a < f x}" by auto
qed

lemma lower_semicontinuous_map_iff_closed:
 "lower_semicontinuous_map X f ⟷ (∀a. closedin X {x∈topspace X. f x ≤ a})"
proof -
  have "{x ∈ topspace X. a < f x} = topspace X - {x ∈ topspace X. f x ≤ a}" for a
    by auto
  thus ?thesis
    by (simp add: closedin_def lower_semicontinuous_map_def)
qed

lemma lower_semicontinuous_map_real_iff:
  fixes f :: "'a ⇒ real"
  shows "lower_semicontinuous_map X f ⟷ lower_semicontinuous_map X (λx. ereal (f x))"
  unfolding lower_semicontinuous_map_def
proof safe
  fix a :: ereal
  assume h:"∀a::real. openin X {x ∈ topspace X. a < f x}"
  consider "a = - ∞" | "a = ∞" | "a ≠ - ∞ ∧ a ≠ ∞" by auto
  then show "openin X {x ∈ topspace X. a < ereal (f x)}"
  proof cases
    case 3
    then have "a < ereal (f x) ⟷ real_of_ereal a < f x" for x
      by (metis ereal_less_eq(3) linorder_not_less real_of_ereal.elims)
    thus ?thesis
      using h by simp
  qed simp_all
next
  fix a :: real
  assume h:"∀a::ereal. openin X {x ∈ topspace X. a < ereal (f x)}"
  then have "openin X {x ∈ topspace X. ereal (f x) > ereal a}"
    by blast
  moreover have"ereal (f x) > real_of_ereal a ⟷ a < f x" for x
    by auto
  ultimately show "openin X {x ∈ topspace X. f x > a}" by auto
qed

subsection ‹Lemmas for Measure Theory›
subsubsection ‹ Lemmas for Measurable Sets›
lemma measurable_preserve_sigma_sets:
  assumes "sets M = sigma_sets Ω S" "S ⊆ Pow Ω"
          "⋀a. a ∈ S ⟹ f ` a ∈ sets N" "inj_on f (space M)" "f ` space M ∈ sets N"
      and "b ∈ sets M" 
    shows "f ` b ∈ sets N"
proof -
  have "b ∈ sigma_sets Ω S"
    using assms(1,6) by simp
  thus ?thesis
  proof induction
    case (Basic a)
    then show ?case by(rule assms(3))
  next
    case Empty
    then show ?case by simp
  next
    case (Compl a)
    moreover have " Ω = space M"
      by (metis assms(1) assms(2) sets.sets_into_space sets.top sigma_sets_into_sp sigma_sets_top subset_antisym)
    ultimately show ?case
      by (metis Diff_subset assms(2) assms(4) assms(5) inj_on_image_set_diff sets.Diff sigma_sets_into_sp)
  next
    case (Union a)
    then show ?case
      by (simp add: image_UN)
  qed
qed

inductive_set sigma_sets_cinter :: "'a set ⇒ 'a set set ⇒ 'a set set"
  for sp :: "'a set" and A :: "'a set set"
  where
    Basic_c[intro, simp]: "a ∈ A ⟹ a ∈ sigma_sets_cinter sp A"
  | Top_c[simp]: "sp ∈ sigma_sets_cinter sp A"
  | Inter_c: "(⋀i::nat. a i ∈ sigma_sets_cinter sp A) ⟹ (⋂i. a i) ∈ sigma_sets_cinter sp A"
  | Union_c: "(⋀i::nat. a i ∈ sigma_sets_cinter sp A) ⟹ (⋃i. a i) ∈ sigma_sets_cinter sp A"

inductive_set sigma_sets_cinter_dunion :: "'a set ⇒ 'a set set ⇒ 'a set set"
  for sp :: "'a set" and A :: "'a set set"
  where
    Basic_cd[intro, simp]: "a ∈ A ⟹ a ∈ sigma_sets_cinter_dunion sp A"
  | Top_cd[simp]: "sp ∈ sigma_sets_cinter_dunion sp A"
  | Inter_cd: "(⋀i::nat. a i ∈ sigma_sets_cinter_dunion sp A) ⟹ (⋂i. a i) ∈ sigma_sets_cinter_dunion sp A"
  | Union_cd: "(⋀i::nat. a i ∈ sigma_sets_cinter_dunion sp A) ⟹ disjoint_family a ⟹ (⋃i. a i) ∈ sigma_sets_cinter_dunion sp A"

lemma sigma_sets_cinter_dunion_subset: "sigma_sets_cinter_dunion sp A ⊆ sigma_sets_cinter sp A"
proof safe
  fix x
  assume "x ∈ sigma_sets_cinter_dunion sp A"
  then show "x ∈ sigma_sets_cinter sp A"
    by induction (auto intro!: Union_c Inter_c)
qed

lemma sigma_sets_cinter_into_sp:
  assumes "A ⊆ Pow sp" "x ∈ sigma_sets_cinter sp A"
  shows "x ⊆ sp"
  using assms(2) by induction (use assms(1) subsetD in blast)+

lemma sigma_sets_cinter_dunion_into_sp:
  assumes "A ⊆ Pow sp" "x ∈ sigma_sets_cinter_dunion sp A"
  shows "x ⊆ sp"
  using assms(2) by induction (use assms(1) subsetD in blast)+

lemma sigma_sets_cinter_int:
  assumes "a ∈ sigma_sets_cinter sp A" "b ∈ sigma_sets_cinter sp A"
  shows "a ∩ b ∈ sigma_sets_cinter sp A"
proof -
  have 1:"a ∩ b = (⋂i::nat. if i = 0 then a else b)" by auto
  show ?thesis
    unfolding 1 by(rule Inter_c,use assms in auto)
qed

lemma sigma_sets_cinter_dunion_int:
  assumes "a ∈ sigma_sets_cinter_dunion sp A" "b ∈ sigma_sets_cinter_dunion sp A"
  shows "a ∩ b ∈ sigma_sets_cinter_dunion sp A"
proof -
  have 1:"a ∩ b = (⋂i::nat. if i = 0 then a else b)" by auto
  show ?thesis
    unfolding 1 by(rule Inter_cd,use assms in auto)
qed

lemma sigma_sets_cinter_un:
  assumes "a ∈ sigma_sets_cinter sp A" "b ∈ sigma_sets_cinter sp A"
  shows "a ∪ b ∈ sigma_sets_cinter sp A"
proof -
  have 1:"a ∪ b = (⋃i::nat. if i = 0 then a else b)" by auto
  show ?thesis
    unfolding 1 by(rule Union_c,use assms in auto)
qed

lemma sigma_sets_eq_cinter_dunion:
  assumes "metrizable_space X"
  shows "sigma_sets (topspace X) {U. openin X U} = sigma_sets_cinter_dunion (topspace X) {U. openin X U}"
proof safe
  fix a
  interpret sa: sigma_algebra "topspace X" "sigma_sets (topspace X) {U. openin X U}"
    by(auto intro!: sigma_algebra_sigma_sets openin_subset)
  assume "a ∈ sigma_sets_cinter_dunion (topspace X) {U. openin X U}"
  then show "a ∈ sigma_sets (topspace X) {U. openin X U}"
    by induction auto
next
  have c:"sigma_sets_cinter_dunion (topspace X) {U. openin X U} ⊆ {U∈sigma_sets_cinter_dunion (topspace X) {U. openin X U}. topspace X - U ∈ sigma_sets_cinter_dunion (topspace X) {U. openin X U}}"
  proof
    fix a
    assume a: "a ∈ sigma_sets_cinter_dunion (topspace X) {U. openin X U}"
    then show "a ∈ {U ∈ sigma_sets_cinter_dunion (topspace X) {U. openin X U}. topspace X - U ∈ sigma_sets_cinter_dunion (topspace X) {U. openin X U}}"
    proof induction
      case a:(Basic_cd a)
      then have "gdelta_in X (topspace X - a)"
        by(auto intro!: closed_imp_gdelta_in assms)
      from gdelta_inD'[OF this] obtain U where U:
       "⋀n :: nat. openin X (U n)" "topspace X - a = ⋂ (range U)" by auto
      show ?case
        using a U(1) by(auto simp: U(2) intro!: Inter_cd)
    next
      case Top_cd
      then show ?case by auto
    next
      case ca:(Inter_cd a)
      define b where "b ≡ (λn. (topspace X - a n) ∩ (⋂i. if i < n then a i else topspace X))"
      have bd:"disjoint_family b"
        using nat_neq_iff by(fastforce simp: disjoint_family_on_def b_def)
      have bin:"b i ∈ sigma_sets_cinter_dunion (topspace X) {U. openin X U}" for i
        unfolding b_def
        apply(rule sigma_sets_cinter_dunion_int)
        using ca(2)[of i]
         apply auto[1]
        apply(rule Inter_cd) using ca by auto
      have bun:"topspace X - (⋂ (range a)) = (⋃i. b i)" (is "?lhs = ?rhs")
      proof -
        { fix x
          have "x ∈ ?lhs ⟷ x ∈ topspace X ∧ x ∈ (⋃i. topspace X - a i)"
            by auto
          also have "... ⟷ x ∈ topspace X ∧ (∃n. x ∈ topspace X - a n)"
            by auto
          also have "... ⟷ x ∈ topspace X ∧ (∃n. x ∈ topspace X - a n ∧ (∀i<n. x ∈ a i))"
          proof safe
            fix n
            assume 1:"x ∉ a n" "x ∈ topspace X"
            define N where "N ≡ Min {m. m ≤ n ∧ x ∉ a m}"
            have N:"x ∉ a N" "N ≤ n"
              using linorder_class.Min_in[of "{m. m ≤ n ∧ x ∉ a m}"] 1
              by(auto simp: N_def)
            have N':"x ∈ a i" if "i < N" for i
            proof(rule ccontr)
              assume "x ∉ a i"
              then have "N ≤ i"
                using linorder_class.Min_le[of "{m. m ≤ n ∧ x ∉ a m}" i] that N(2)
                by(auto simp: N_def)
              with that show False by auto
            qed
            show "∃n. x ∈ topspace X - a n ∧ (∀i<n. x ∈ a i)"
              using N N' by(auto intro!: exI[where x=N] 1)
          qed auto
          also have "... ⟷ x ∈ ?rhs"
            by(auto simp: b_def)
          finally have "x ∈ ?lhs ⟷ x ∈ ?rhs" . }
        thus ?thesis by auto
      qed
      have "... ∈ sigma_sets_cinter_dunion (topspace X) {U. openin X U}"
        by(rule Union_cd) (use bin bd in auto)
      thus ?case
        using Inter_cd[of a,OF ca(1)] by(auto simp: bun)
    next
      case ca:(Union_cd a)
      have "topspace X - (⋃ (range a)) = (⋂i. (topspace X - a i))"
        by simp
      have "... ∈ sigma_sets_cinter_dunion (topspace X) {U. openin X U}"
        by(rule Inter_cd) (use ca in auto)
      then show ?case
        using Union_cd[of a,OF ca(1,2)] by auto 
    qed
  qed
  fix a
  assume "a ∈ sigma_sets (topspace X) {U. openin X U}"
  then show "a ∈ sigma_sets_cinter_dunion (topspace X) {U. openin X U}"
  proof induction
    case a:(Union a)
    define b where "b ≡ (λn. a n ∩  (⋂i. if i < n then topspace X - a i else topspace X))"
    have bd:"disjoint_family b"
      by(auto simp: disjoint_family_on_def b_def) (metis Diff_iff UnCI image_eqI linorder_neqE_nat mem_Collect_eq)
    have bin:"b i ∈ sigma_sets_cinter_dunion (topspace X) {U. openin X U}" for i
      unfolding b_def
      apply(rule sigma_sets_cinter_dunion_int)
      using a(2)[of i]
       apply auto[1]
      apply(rule Inter_cd) using c a by auto
    have bun:"(⋃i. a i) = (⋃i. b i)" (is "?lhs = ?rhs")
    proof -
      {
        fix x
        have "x ∈ ?lhs ⟷ x ∈ topspace X ∧ x ∈ ?lhs"
          using sigma_sets_cinter_dunion_into_sp[OF _ a(2)]
          by (metis UN_iff subsetD subset_Pow_Union topspace_def)
        also have "... ⟷ x ∈ topspace X ∧ (∃n. x ∈ a n)" by auto
        also have "... ⟷ x ∈ topspace X ∧ (∃n. x ∈ a n ∧ (∀i<n. x ∈ topspace X - a i))"
        proof safe
          fix n
          assume 1:"x ∈ topspace X" "x ∈ a n"
          define N where "N ≡ Min {m. m ≤ n ∧ x ∈ a m}"
          have N:"x ∈ a N" "N ≤ n"
            using linorder_class.Min_in[of "{m. m ≤ n ∧ x ∈ a m}"] 1
            by(auto simp: N_def)
          have N':"x ∉ a i" if "i < N" for i
          proof(rule ccontr)
            assume "¬ x ∉ a i"
            then have "N ≤ i"
              using linorder_class.Min_le[of "{m. m ≤ n ∧ x ∈ a m}" i] that N(2)
              by(auto simp: N_def)
            with that show False by auto
          qed
          show "∃n. x ∈ a n ∧ (∀i<n. x ∈ topspace X - a i)"
            using N N' 1 by(auto intro!: exI[where x=N])
        qed auto
        also have "... ⟷ x ∈ ?rhs"
        proof safe
          fix m
          assume "x ∈ b m"
          then show "x ∈ topspace X" "∃n. x ∈ a n ∧ (∀i<n. x ∈ topspace X - a i)"
            by(auto intro!: exI[where x=m] simp: b_def)
        qed(auto simp: b_def)
        finally have "x ∈ ?lhs ⟷ x ∈ ?rhs" . }
      thus ?thesis by auto
    qed
    have "... ∈ sigma_sets_cinter_dunion (topspace X) {U. openin X U}"
      by(rule Union_cd) (use bin bd in auto)
    thus ?case
      by(auto simp: bun)
  qed(use c in auto)
qed

lemma sigma_sets_eq_cinter:
  assumes "metrizable_space X"
  shows "sigma_sets (topspace X) {U. openin X U} = sigma_sets_cinter (topspace X) {U. openin X U}"
proof safe
  fix a
  interpret sa: sigma_algebra "topspace X" "sigma_sets (topspace X) {U. openin X U}"
    by(auto intro!: sigma_algebra_sigma_sets openin_subset)
  assume "a ∈ sigma_sets_cinter (topspace X) {U. openin X U}"
  then show "a ∈ sigma_sets (topspace X) {U. openin X U}"
    by induction auto
qed (use sigma_sets_cinter_dunion_subset sigma_sets_eq_cinter_dunion[OF assms] in auto)

subsubsection ‹ Measurable Isomorphisms ›
definition measurable_isomorphic_map::"['a measure, 'b measure, 'a ⇒ 'b] ⇒ bool" where
"measurable_isomorphic_map M N f ⟷ bij_betw f (space M) (space N) ∧ f ∈ M →⇩M N ∧ the_inv_into (space M) f ∈ N →⇩M M"

lemma measurable_isomorphic_map_sets_cong:
  assumes "sets M = sets M'" "sets N = sets N'"
  shows "measurable_isomorphic_map M N f ⟷ measurable_isomorphic_map M' N' f"
  by(simp add: measurable_isomorphic_map_def sets_eq_imp_space_eq[OF assms(1)] sets_eq_imp_space_eq[OF assms(2)] measurable_cong_sets[OF assms] measurable_cong_sets[OF assms(2,1)])

lemma measurable_isomorphic_map_surj:
  assumes "measurable_isomorphic_map M N f"
  shows "f ` space M = space N"
  using assms by(auto simp: measurable_isomorphic_map_def bij_betw_def)

lemma measurable_isomorphic_mapI:
  assumes "bij_betw f (space M) (space N)" "f ∈ M →⇩M N" "the_inv_into (space M) f ∈ N →⇩M M"
  shows "measurable_isomorphic_map M N f"
  using assms by(simp add: measurable_isomorphic_map_def)

lemma measurable_isomorphic_map_byWitness:
  assumes "f ∈ M →⇩M N" "g ∈ N →⇩M M" "⋀x. x ∈ space M ⟹ g (f x) = x" "⋀x. x ∈ space N ⟹ f (g x) = x"
  shows "measurable_isomorphic_map M N f"
proof -
  have *:"bij_betw f (space M) (space N)"
    using assms by(auto intro!: bij_betw_byWitness[where f'=g] dest:measurable_space)
  show ?thesis
  proof(rule measurable_isomorphic_mapI)
    have "the_inv_into (space M) f x = g x" if "x ∈ space N" for x
      by (metis * assms(2) assms(4) bij_betw_imp_inj_on measurable_space that the_inv_into_f_f)
    thus "the_inv_into (space M) f ∈ N →⇩M M"
      using measurable_cong assms(2) by blast
  qed (simp_all add: * assms(1))
qed

lemma measurable_isomorphic_map_restrict_space:
  assumes "f ∈ M →⇩M N" "⋀A. A ∈ sets M ⟹ f ` A ∈ sets N" "inj_on f (space M)"
  shows "measurable_isomorphic_map M (restrict_space N (f ` space M)) f"
proof(rule measurable_isomorphic_mapI)
  show "bij_betw f (space M) (space (restrict_space N (f ` space M)))"
    by (simp add: assms(2,3) inj_on_imp_bij_betw)
next
  show "f ∈ M →⇩M restrict_space N (f ` space M)"
    by (simp add: assms(1) measurable_restrict_space2)
next
  show "the_inv_into (space M) f ∈ restrict_space N (f ` space M) →⇩M M"
  proof(rule measurableI)
    show "x ∈ space (restrict_space N (f ` space M)) ⟹ the_inv_into (space M) f x ∈ space M" for x
      by (simp add: assms(2,3) the_inv_into_into)
  next
    fix A
    assume "A ∈ sets M"
    have "the_inv_into (space M) f -` A ∩ space (restrict_space N (f ` space M)) = f ` A"
      by (simp add: ‹A ∈ sets M› assms(2,3) sets.sets_into_space the_inv_into_vimage)
    also note assms(2)[OF ‹A ∈ sets M›]
    finally show "the_inv_into (space M) f -` A ∩ space (restrict_space N (f ` space M)) ∈ sets (restrict_space N (f ` space M))"
      by (simp add: assms(2) sets_restrict_space_iff)
  qed
qed

lemma measurable_isomorphic_mapD':
  assumes "measurable_isomorphic_map M N f"
  shows "⋀A. A ∈ sets M ⟹ f ` A ∈ sets N" "f ∈ M →⇩M N"
        "∃g. bij_betw g (space N) (space M) ∧ g ∈ N →⇩M M ∧ (∀x ∈ space M. g (f x) = x) ∧ (∀x∈ space N. f (g x) = x) ∧ (∀A∈sets N. g ` A ∈ sets M)"
proof -
  have h:"bij_betw f (space M) (space N)" "f ∈ M →⇩M N" "the_inv_into (space M) f ∈ N →⇩M M"
    using assms by(simp_all add: measurable_isomorphic_map_def)
  show "f ` A ∈ sets N" if "A ∈ sets M" for A
  proof -
    have "f ` A = the_inv_into (space M) f -` A ∩ space N"
      using the_inv_into_vimage[OF bij_betw_imp_inj_on[OF h(1)] sets.sets_into_space[OF that]]
      by(simp add: bij_betw_imp_surj_on[OF h(1)])
    also have "... ∈ sets N"
      using that h(3) by auto
    finally show ?thesis .
  qed
  show "f ∈ M →⇩M N"
    using assms by(simp add: measurable_isomorphic_map_def)

  show "∃g. bij_betw g (space N) (space M) ∧ g ∈ N →⇩M M ∧ (∀x ∈ space M. g (f x) = x) ∧ (∀x∈ space N. f (g x) = x) ∧ (∀A∈sets N. g ` A ∈ sets M)"
  proof(rule exI[where x="the_inv_into (space M) f"])
    have *:"the_inv_into (space M) f ` A ∈ sets M" if "A ∈ sets N" for A
    proof -
      have "⋀x. x ∈ space M ⟹ the_inv_into (space N) (the_inv_into (space M) f) x = f x"
        by (metis bij_betw_imp_inj_on bij_betw_the_inv_into h(1) h(2) measurable_space the_inv_into_f_f)
      from vimage_inter_cong[of "space M" _ f A,OF this] the_inv_into_vimage[OF bij_betw_imp_inj_on[OF bij_betw_the_inv_into[OF h(1)]] sets.sets_into_space[OF that]]
           bij_betw_imp_surj_on[OF bij_betw_the_inv_into[OF h(1)]] measurable_sets[OF h(2) that]
      show ?thesis
        by fastforce
    qed
    show "bij_betw (the_inv_into (space M) f) (space N) (space M) ∧ the_inv_into (space M) f ∈ N →⇩M M ∧ (∀x∈space M. the_inv_into (space M) f (f x) = x) ∧ (∀x∈space N. f (the_inv_into (space M) f x) = x) ∧ (∀A∈sets N. the_inv_into (space M) f ` A ∈ sets M)"
      using bij_betw_the_inv_into[OF h(1)]
      by (meson * bij_betw_imp_inj_on f_the_inv_into_f_bij_betw h(1) h(3) the_inv_into_f_f)
  qed
qed

lemma measurable_isomorphic_map_inv:
  assumes "measurable_isomorphic_map M N f"
  shows "measurable_isomorphic_map N M (the_inv_into (space M) f)"
  using assms[simplified measurable_isomorphic_map_def]
  by(auto intro!: measurable_isomorphic_map_byWitness[where g=f] bij_betw_the_inv_into f_the_inv_into_f_bij_betw[of f] bij_betw_imp_inj_on the_inv_into_f_f)

lemma measurable_isomorphic_map_comp:
  assumes "measurable_isomorphic_map M N f" and "measurable_isomorphic_map N L g"
  shows "measurable_isomorphic_map M L (g ∘ f)"
proof -
  obtain f' g' where
  [measurable]: "f' ∈ N →⇩M M"     and hf:"⋀x. x∈space M ⟹ f' (f x) = x" "⋀x. x∈space N ⟹ f (f' x) = x"
  and [measurable]: "g' ∈ L →⇩M N" and hg:"⋀x. x∈space N ⟹ g' (g x) = x" "⋀x. x∈space L ⟹ g (g' x) = x"
    using measurable_isomorphic_mapD'[OF assms(1)] measurable_isomorphic_mapD'[OF assms(2)] by metis
  have [measurable]: "f ∈ M →⇩M N" "g ∈ N →⇩M L"
    using assms by(auto simp: measurable_isomorphic_map_def)
  from hf hg measurable_space[OF ‹f ∈ M →⇩M N›] measurable_space[OF ‹g' ∈ L →⇩M N›] show ?thesis
    by(auto intro!: measurable_isomorphic_map_byWitness[where g="f'∘g'"])
qed

definition measurable_isomorphic::"['a measure, 'b measure] ⇒ bool" (infixr "measurable'_isomorphic" 50) where
"M measurable_isomorphic N ⟷ (∃f. measurable_isomorphic_map M N f)"

lemma measurable_isomorphic_sets_cong:
  assumes "sets M = sets M'" "sets N = sets N'"
  shows "M measurable_isomorphic N  ⟷ M' measurable_isomorphic N'"
  using measurable_isomorphic_map_sets_cong[OF assms]
  by(auto simp: measurable_isomorphic_def)

lemma measurable_isomorphicD:
  assumes "M measurable_isomorphic N"
  shows "∃f g. f ∈ M →⇩M N ∧ g ∈ N →⇩M M ∧ (∀x∈space M. g (f x) = x) ∧ (∀y∈space N. f (g y) = y) ∧ (∀A∈sets M. f ` A ∈ sets N) ∧ (∀A∈sets N. g ` A ∈ sets M)"
  using assms measurable_isomorphic_mapD'[of M N]
  by (metis (mono_tags, lifting) measurable_isomorphic_def)

lemma measurable_isomorphic_cardinality_eq:
  assumes "M measurable_isomorphic N"
  shows "space M ≈ space N"
  by (meson assms eqpoll_def measurable_isomorphic_def measurable_isomorphic_map_def)

lemma measurable_isomorphic_count_spaces: "count_space A measurable_isomorphic count_space B ⟷ A ≈ B"
proof
  assume "A ≈ B"
  then obtain f where f:"bij_betw f A B"
    by(auto simp: eqpoll_def)
  then show "count_space A measurable_isomorphic count_space B"
    by(auto simp: measurable_isomorphic_def measurable_isomorphic_map_def bij_betw_def the_inv_into_into intro!: exI[where x=f])
qed(use measurable_isomorphic_cardinality_eq in fastforce)

lemma measurable_isomorphic_byWitness:
  assumes "f ∈ M →⇩M N" "⋀x. x∈space M ⟹ g (f x) = x"
      and "g ∈ N →⇩M M" "⋀y. y∈space N ⟹ f (g y) = y"
    shows "M measurable_isomorphic N"
  by(auto simp: measurable_isomorphic_def assms intro!: exI[where x = f] measurable_isomorphic_map_byWitness[where g=g])

lemma measurable_isomorphic_refl:
  "M measurable_isomorphic M"
  by(auto intro!: measurable_isomorphic_byWitness[where f=id and g=id])

lemma measurable_isomorphic_sym:
  assumes "M measurable_isomorphic N"
  shows "N measurable_isomorphic M"
  using assms measurable_isomorphic_map_inv[of M N]
  by(auto simp: measurable_isomorphic_def)

lemma measurable_isomorphic_trans:
  assumes "M measurable_isomorphic N" and "N measurable_isomorphic L"
  shows "M measurable_isomorphic L"
  using assms measurable_isomorphic_map_comp[of M N _ L]
  by(auto simp: measurable_isomorphic_def)

lemma measurable_isomorphic_empty:
  assumes "space M = {}" "space N = {}"
  shows "M measurable_isomorphic N"
  using assms by(auto intro!: measurable_isomorphic_byWitness[where f=undefined and g=undefined] simp: measurable_empty_iff)

lemma measurable_isomorphic_empty1:
  assumes "space M = {}" "M measurable_isomorphic N"
  shows "space N = {}"
  using measurable_isomorphicD[OF assms(2)] by(auto simp: measurable_empty_iff[OF assms(1)])

lemma measurable_ismorphic_empty2:
  assumes "space N = {}" "M measurable_isomorphic N"
  shows "space M = {}"
  using measurable_isomorphic_sym[OF assms(2)] assms(1)
  by(simp add: measurable_isomorphic_empty1)

lemma measurable_lift_product:
  assumes "⋀i. i ∈ I ⟹ f i ∈ (M i) →⇩M (N i)"
  shows "(λx i. if i ∈ I then f i (x i) else undefined) ∈ (Π⇩M i∈I. M i) →⇩M (Π⇩M i∈I. N i)"
  using measurable_space[OF assms]
  by(auto intro!: measurable_PiM_single' simp: assms measurable_PiM_component_rev space_PiM PiE_iff)

lemma measurable_isomorphic_map_lift_product:
  assumes "⋀i. i ∈ I ⟹ measurable_isomorphic_map (M i) (N i) (h i)"
  shows "measurable_isomorphic_map (Π⇩M i∈I. M i) (Π⇩M i∈I. N i) (λx i. if i ∈ I then h i (x i) else undefined)"
proof -
  obtain h' where
   "⋀i. i ∈ I ⟹ h' i ∈ (N i) →⇩M (M i)" "⋀i x. i ∈ I ⟹ x∈space (M i) ⟹ h' i (h i x) = x" "⋀i x. i ∈ I ⟹ x∈space (N i) ⟹ h i (h' i x) = x"
    using measurable_isomorphic_mapD'(3)[OF assms] by metis
  thus ?thesis
    by(auto intro!: measurable_isomorphic_map_byWitness[OF measurable_lift_product[of I h M N,OF measurable_isomorphic_mapD'(2)[OF assms]] measurable_lift_product[of I h' N M,OF ‹⋀i. i ∈ I ⟹ h' i ∈ (N i) →⇩M (M i)›]]
              simp: space_PiM PiE_iff extensional_def)
qed

lemma measurable_isomorphic_lift_product:
  assumes "⋀i. i ∈ I ⟹ (M i) measurable_isomorphic (N i)"
  shows "(Π⇩M i∈I. M i) measurable_isomorphic  (Π⇩M i∈I. N i)"
proof -
  obtain h where "⋀i. i ∈ I ⟹ measurable_isomorphic_map (M i) (N i) (h i)"
    using assms by(auto simp: measurable_isomorphic_def) metis
  thus ?thesis
    by(auto intro!: measurable_isomorphic_map_lift_product exI[where x="λx i. if i ∈ I then h i (x i) else undefined"] simp: measurable_isomorphic_def)
qed

text ‹🌐‹https://math24.net/cantor-schroder-bernstein-theorem.html››
lemma Schroeder_Bernstein_measurable':
  assumes "f ` (space M) ∈ sets N" "g ` (space N) ∈ sets M"
      and "measurable_isomorphic_map M (restrict_space N (f ` (space M))) f" and "measurable_isomorphic_map N (restrict_space M (g ` (space N))) g"
    shows "∃h. measurable_isomorphic_map M N h"
proof -
  have hset:"⋀A. A ∈ sets M ⟹ f ` A ∈ sets (restrict_space N (f ` space M))" 
            "⋀A. A ∈ sets N ⟹ g ` A ∈ sets (restrict_space M (g ` space N))" 
  and hfg[measurable]:"f ∈ M →⇩M restrict_space N (f ` space M)"
                      "g ∈ N →⇩M restrict_space M (g ` space N)"
    using measurable_isomorphic_mapD'(1,2)[OF assms(3)]  measurable_isomorphic_mapD'(1,2)[OF assms(4)] assms(1,2)
    by auto
  have hset2:"⋀A. A ∈ sets M ⟹ f ` A ∈ sets N" "⋀A. A ∈ sets N ⟹ g ` A ∈ sets M"
   and hfg2[measurable]: "f ∈ M →⇩M N" "g ∈ N →⇩M M"
    using sets.Int_space_eq2[OF assms(1)] sets.Int_space_eq2[OF assms(2)] sets_restrict_space_iff[of "f ` space M" N] sets_restrict_space_iff[of "g ` space N" M] hset
          measurable_restrict_space2_iff[of f M N] measurable_restrict_space2_iff[of g N M] hfg assms(1,2)
    by auto
  have bij1:"bij_betw f (space M) (f ` (space M))" "bij_betw g (space N) (g ` (space N))"
    using assms(3,4) by(auto simp: measurable_isomorphic_map_def space_restrict_space sets.Int_space_eq2[OF assms(1)] sets.Int_space_eq2[OF assms(2)])
  obtain f' g' where
  hfg1'[measurable]: "f' ∈ restrict_space N (f ` (space M)) →⇩M M" "g' ∈ restrict_space M (g ` (space N)) →⇩M N"
    and hfg':"⋀x. x∈space M ⟹ f' (f x) = x" "⋀x. x∈f ` space M ⟹ f (f' x) = x"
             "⋀x. x∈space N ⟹ g' (g x) = x" "⋀x. x∈g ` space N ⟹ g (g' x) = x"
             "bij_betw f' (f ` space M) (space M)" "bij_betw g' (g ` space N) (space N)"
    using measurable_isomorphic_mapD'(3)[OF assms(3)] measurable_isomorphic_mapD'(3)[OF assms(4)] sets.Int_space_eq2[OF assms(1)] sets.Int_space_eq2[OF assms(2)]
    by (metis space_restrict_space)

  have hgfA:"(g ∘ f) ` A ∈ sets M" if "A ∈ sets M" for A
    using hset2(2)[OF hset2(1)[OF that]] by(simp add: image_comp)
  define An where "An ≡ (λn. ((g ∘ f)^^n) ` (space M - g ` (space N)))"
  define A where "A ≡ (⋃n∈UNIV. An n)"
  have "An n ∈ sets M" for n
  proof(induction n)
    case 0
    thus ?case
      using hset2[OF sets.top] by(simp add: An_def)
  next
    case ih:(Suc n)
    have "An (Suc n) = (g ∘ f) ` (An n)"
      by(auto simp add: An_def)
    thus ?case
      using hgfA[OF ih] by simp
  qed
  hence Asets:"A ∈ sets M"
    by(simp add: A_def)
  have Acompl:"space M - A ⊆ g ` space N"
  proof -
    have "space M - A ⊆ space M - An 0"
      by(auto simp: A_def)
    also have "... ⊆ g ` space N"
      by(auto simp: An_def)
    finally show ?thesis .
  qed
  define h where "h ≡ (λx. if x ∈ A ∪ (- space M) then f x else g' x)"
  define h' where "h' ≡ (λx. if x ∈ f ` A then f' x else g x)"
  have xinA_iff:"x ∈ A ⟷ h x ∈ f ` A" if "x ∈ space M" for x
  proof
    assume "h x ∈ f ` A"
    show "x ∈ A"
    proof(rule ccontr)
      assume "x ∉ A"
      then have "⋀n. x ∉ An n"
        by(auto simp: A_def)
      from this[of 0] have "x ∈ g ` (space N)"
        using that by(auto simp: An_def)
      have "g' x ∈ f ` A "
        using ‹h x ∈ f ` A› ‹x ∉ A›
        by (simp add: h_def that)
      hence "g (g' x) ∈ (g ∘ f) ` A"
        by auto
      hence "x ∈ (g ∘ f) ` A"
        using ‹x ∈ g ` (space N)› by (simp add: hfg'(4))
      then obtain n where "x ∈ (g ∘ f) ` (An n)"
        by(auto simp: A_def)
      hence "x ∈ An (Suc n)"
        by(auto simp: An_def)
      thus False
        using ‹⋀n. x ∉ An n› by simp
    qed
  qed(simp add: h_def)

  show ?thesis
  proof(intro exI[where x=h] measurable_isomorphic_map_byWitness[where g=h'])
    have "{x ∈ space M. x ∈ A ∪ (- space M)} ∈ sets M"
      using sets.Int_space_eq2[OF Asets] Asets by simp
    moreover have "f ∈ restrict_space M {x. x ∈ A ∪ - space M} →⇩M N"
      by (simp add: measurable_restrict_space1)
    moreover have "g' ∈ restrict_space M {x. x ∉  A ∪ (- space M)} →⇩M N"
    proof -
      have "sets (restrict_space (restrict_space M (g ` space N))  {x. x ∉ A ∪ - space M}) = sets (restrict_space M (g ` space N ∩  {x. x ∉ A ∪ - space M}))"
        by(simp add: sets_restrict_restrict_space)
      also have "... = sets (restrict_space M (g ` space N ∩ {x. x ∈ space M - A}))"
        by (metis Compl_iff DiffE DiffI Un_iff)
      also have "... = sets (restrict_space M {x. x ∈ space M - A})"
        by (metis Acompl le_inf_iff mem_Collect_eq subsetI subset_antisym)
      also have "... = sets (restrict_space M {x. x ∉  A ∪ (- space M)})"
        by (metis Compl_iff DiffE DiffI Un_iff)
      finally have "sets (restrict_space (restrict_space M (g ` space N)) {x. x ∉ A ∪ - space M}) = sets (restrict_space M {x. x ∉ A ∪ - space M})" .
      from measurable_cong_sets[OF this refl] measurable_restrict_space1[OF hfg1'(2),of " {x. x ∉ A ∪ - space M}"]
      show ?thesis by auto
    qed
    ultimately show "h ∈ M →⇩M N"
      by(simp add: h_def measurable_If_restrict_space_iff)
  next
    have "{x ∈ space N. x ∈ f ` A} ∈ sets N"
      using sets.Int_space_eq2[OF hset2(1)[OF Asets]] hset2(1)[OF Asets] by simp
    moreover have "f' ∈ restrict_space N {x. x ∈ f ` A} →⇩M M"
    proof -
      have "sets (restrict_space (restrict_space N (f ` space M)) {x. x ∈ f ` A}) = sets (restrict_space N (f ` space M ∩ {x. x ∈ f ` A}))"
        by(simp add: sets_restrict_restrict_space)
      also have "... = sets (restrict_space N {x. x ∈ f ` A})"
      proof -
        have "f ` space M ∩ {x. x ∈ f ` A} = {x. x ∈ f ` A}"
          using sets.sets_into_space[OF Asets] by auto
        thus ?thesis by simp
      qed
      finally have "sets (restrict_space (restrict_space N (f ` space M)) {x. x ∈ f ` A}) = sets (restrict_space N {x. x ∈ f ` A})" .
      from measurable_cong_sets[OF this refl] measurable_restrict_space1[OF hfg1'(1),of "{x. x ∈ f ` A}"]
      show ?thesis by auto
    qed
    moreover have "g ∈ restrict_space N {x. x ∉ f ` A} →⇩M M"
      by (simp add: measurable_restrict_space1)
    ultimately show "h' ∈ N →⇩M M"
      by(simp add: h'_def measurable_If_restrict_space_iff)
  next
    fix x
    assume "x ∈ space M"
    then consider "x ∈ A" | "x ∈ space M - A" by auto
    thus "h' (h x) = x"
    proof cases
      case xa:2
      hence "h x ∉ f ` A"
        using ‹x ∈ space M› xinA_iff by blast
      thus ?thesis
        using Acompl hfg'(4) xa by(auto simp add: h_def h'_def)
    qed(simp add: h_def h'_def ‹x ∈ space M› hfg'(1))
  next
    fix x
    assume "x ∈ space N"
    then consider "x ∈ f ` A" | "x ∈ space N -  f ` A" by auto
    thus "h (h' x) = x"
    proof cases
      case hx:1
      hence "x ∈ f ` (space M)"
        using image_mono[OF sets.sets_into_space[OF Asets],of f] by auto
      have "h' x = f' x"
        using hx by(simp add: h'_def)
      also have "... ∈ A"
        using hx sets.sets_into_space[OF Asets] hfg'(1) by auto
      finally show ?thesis
        using hfg'(2)[OF ‹x ∈ f ` (space M)›] hx by(auto simp: h_def h'_def)
    next
      case hx:2
      then have "h' x = g x"
        by(simp add: h'_def)
      also have "... ∉ A"
      proof(rule ccontr)
        assume "¬ g x ∉ A"
        then have "g x ∈ A" by simp
        then obtain n where hg:"g x ∈ An n" by(auto simp: A_def)
        hence "0 < n" using hx by(auto simp: An_def)
        then obtain n' where [simp]:"n = Suc n'"
          using not0_implies_Suc by blast
        then have "g x ∈ g ` f `  An n'"
          using hg by(auto simp: An_def)
        hence "x ∈ f ` An n'"
          using inj_on_image_mem_iff[OF bij_betw_imp_inj_on[OF bij1(2)] ‹x ∈ space N›,of "f ` An n'"]
                sets.sets_into_space[OF ‹An n' ∈ sets M›] measurable_space[OF hfg2(1)] by auto
        also have "... ⊆ f ` A"
          by(auto simp: A_def)
        finally show False
          using hx by simp
      qed
      finally show ?thesis
        using hx hfg'(3)[OF ‹x ∈ space N›] measurable_space[OF hfg2(2) ‹x ∈ space N›]
        by(auto simp: h_def h'_def)
    qed
  qed
qed

lemma Schroeder_Bernstein_measurable:
  assumes "f ∈ M →⇩M N" "⋀A. A ∈ sets M ⟹ f ` A ∈ sets N" "inj_on f (space M)"
      and "g ∈ N →⇩M M" "⋀A. A ∈ sets N ⟹ g ` A ∈ sets M" "inj_on g (space N)"
    shows "∃h. measurable_isomorphic_map M N h"
  using Schroeder_Bernstein_measurable'[OF assms(2)[OF sets.top] assms(5)[OF sets.top] measurable_isomorphic_map_restrict_space[OF assms(1-3)] measurable_isomorphic_map_restrict_space[OF assms(4-6)]]
  by simp

lemma measurable_isomorphic_from_embeddings:
  assumes "M measurable_isomorphic (restrict_space N B)" "N measurable_isomorphic (restrict_space M A)"
      and "A ∈ sets M" "B ∈ sets N"
    shows "M measurable_isomorphic N"
proof -
  obtain f g where fg:"measurable_isomorphic_map M (restrict_space N B) f" "measurable_isomorphic_map N (restrict_space M A) g"
    using assms(1,2) by(auto simp: measurable_isomorphic_def)
  have [simp]:"f ` space M = B" "g ` space N = A"
    using measurable_isomorphic_map_surj[OF fg(1)] measurable_isomorphic_map_surj[OF fg(2)] sets.sets_into_space[OF assms(3)] sets.sets_into_space[OF assms(4)]
    by(auto simp: space_restrict_space)
  obtain h where "measurable_isomorphic_map M N h"
    using Schroeder_Bernstein_measurable'[of f M N g] assms(3,4) fg by auto
  thus ?thesis
    by(auto simp: measurable_isomorphic_def)
qed

lemma measurable_isomorphic_antisym:
  assumes "B measurable_isomorphic (restrict_space C c)" "A measurable_isomorphic (restrict_space B b)"
      and "c ∈ sets C" "b ∈ sets B" "C measurable_isomorphic A" 
    shows "C measurable_isomorphic B"
  by(rule measurable_isomorphic_from_embeddings[OF measurable_isomorphic_trans[OF assms(5,2)] assms(1) assms(3,4)])

lemma countable_infinite_isomorphisc_to_nat_index:
  assumes "countable I" and "infinite I"
  shows "(Π⇩M x∈I. M) measurable_isomorphic (Π⇩M (x::nat)∈UNIV. M)"
proof(rule measurable_isomorphic_byWitness[where f="λx n. x (from_nat_into I n)" and g="λx. λi∈I. x (to_nat_on I i)"])
  show "(λx n. x (from_nat_into I n)) ∈ (Π⇩M x∈I. M) →⇩M (Π⇩M (x::nat)∈UNIV. M)"
    by(auto intro!: measurable_PiM_single' measurable_component_singleton[OF from_nat_into[OF infinite_imp_nonempty[OF assms(2)]]])
      (simp add: PiE_iff infinite_imp_nonempty space_PiM from_nat_into[OF infinite_imp_nonempty[OF assms(2)]])
next
  show "(λx. λi∈I. x (to_nat_on I i)) ∈ (Π⇩M (x::nat)∈UNIV. M) →⇩M (Π⇩M x∈I. M)"
    by(auto intro!: measurable_PiM_single')
next
  show "x ∈ space (Π⇩M x∈I. M) ⟹ (λi∈I. x (from_nat_into I (to_nat_on I i))) = x" for x
    by (simp add: assms(1) restrict_ext space_PiM)
next
  show "y ∈ space (Pi⇩M UNIV (λx. M)) ⟹ (λn. (λi∈I. y (to_nat_on I i)) (from_nat_into I n)) = y" for y
    by (simp add: assms(1) assms(2) from_nat_into infinite_imp_nonempty)
qed

lemma PiM_PiM_isomorphic_to_PiM:
 "(Π⇩M i∈I. Π⇩M j∈J. M i j) measurable_isomorphic (Π⇩M (i,j)∈I×J. M i j)"
proof(rule measurable_isomorphic_byWitness[where f="λx (i,j). if (i,j) ∈ I × J then x i j else undefined" and g="λx i j. if i ∉ I then undefined j else if j ∉ J then undefined else x (i,j)"])
  have [simp]: "(λω. ω a b) ∈ (Π⇩M i∈I. Π⇩M j∈J. M i j) →⇩M M a b" if "a ∈ I" "b ∈ J" for a b
    using measurable_component_singleton[OF that(1),of "λi.  Π⇩M j∈J. M i j"] measurable_component_singleton[OF that(2),of "M a"]
    by auto
  show "(λx (i, j). if (i, j) ∈ I × J then x i j else undefined) ∈ (Π⇩M i∈I. Π⇩M j∈J. M i j) →⇩M (Π⇩M (i,j)∈I×J. M i j)"
    apply(rule measurable_PiM_single')
     apply auto[1]
    apply(auto simp: PiE_def Pi_def space_PiM extensional_def;meson)
    done
next
  have [simp]: "(λω. ω (i, j))  ∈ Pi⇩M (I × J) (λ(i, j). M i j) →⇩M M i j" if "i ∈ I" "j ∈ J" for i j
    using measurable_component_singleton[of "(i,j)" "I × J" "λ(i, j). M i j"] that by auto
  show "(λx i j. if i ∉ I then undefined j else if j ∉ J then undefined else x (i, j)) ∈ (Π⇩M (i,j)∈I×J. M i j) →⇩M (Π⇩M i∈I. Π⇩M j∈J. M i j)"
    by(auto intro!: measurable_PiM_single') (simp_all add: PiE_iff space_PiM extensional_def)
next
  show "x ∈ space (Π⇩M i∈I. Π⇩M j∈J. M i j) ⟹ (λi j. if i ∉ I then undefined j else if j ∉ J then undefined else case (i, j) of (i, j) ⇒ if (i, j) ∈ I × J then x i j else undefined) = x" for x
    by standard+ (auto simp: space_PiM PiE_def Pi_def extensional_def)
next
  show "y ∈ space (Π⇩M (i,j)∈I×J. M i j) ⟹ (λ(i, j). if (i, j) ∈ I × J then if i ∉ I then undefined j else if j ∉ J then undefined else y (i, j) else undefined) = y" for y
    by standard+ (auto simp: space_PiM PiE_def Pi_def extensional_def)
qed

lemma measurable_isomorphic_map_sigma_sets:
  assumes "sets M = sigma_sets (space M) U" "measurable_isomorphic_map M N f"
  shows "sets N = sigma_sets (space N) ((`) f ` U)"
proof -
  from measurable_isomorphic_mapD'[OF assms(2)]
  obtain g where h: "⋀A. A ∈ sets M ⟹ f ` A ∈ sets N" "f ∈ M →⇩M N" "bij_betw g (space N) (space M)" "g ∈ N →⇩M M" "⋀x. x∈space M ⟹ g (f x) = x" "⋀x. x∈space N ⟹ f (g x) = x" "⋀A. A∈sets N ⟹ g ` A ∈ sets M"
    by metis
  interpret s: sigma_algebra "space N"  "sigma_sets (space N) ((`) f ` U)"
    by(auto intro!: sigma_algebra_sigma_sets) (metis assms(1) h(2) measurable_space sets.sets_into_space sigma_sets_superset_generator subsetD)
  show ?thesis
  proof safe
    fix x
    assume "x ∈ sets N"
    from h(7)[OF this] assms(1)
    have "g ` x ∈ sigma_sets (space M) U" by simp
    hence "f ` (g ` x) ∈ sigma_sets (space N) ((`) f ` U)"
    proof induction
      case h:(Compl a)
      have "f ` (space M - a) = f ` (space M) - f ` a"
        by(rule inj_on_image_set_diff[where C="space M"], insert assms h) (auto simp: measurable_isomorphic_map_def bij_betw_def sets.sets_into_space)
      with h show ?case
        by (metis assms(2) measurable_isomorphic_map_surj s.Diff s.top) 
    qed (auto simp: image_UN)
    moreover have "f ` (g ` x) = x"
      using sets.sets_into_space[OF ‹x ∈ sets N›] h(6) by(fastforce simp: image_def)
    ultimately show "x ∈ sigma_sets (space N) ((`) f ` U)" by simp
  next
    interpret s': sigma_algebra "space M" "sigma_sets (space M) U"
      by(simp add: assms(1)[symmetric] sets.sigma_algebra_axioms)
    have 1:"⋀x. x ∈ U ⟹ x ⊆ space M"
      by (simp add: s'.sets_into_space)
    fix x
    assume assm:"x ∈ sigma_sets (space N) ((`) f ` U)"
    then show "x ∈ sets N"
      by induction (auto simp: assms(1) h(1))
  qed
qed

subsubsection ‹Borel Spaces Genereted from Abstract Topologies›
definition borel_of :: "'a topology ⇒ 'a measure" where
"borel_of X ≡ sigma (topspace X) {U. openin X U}"

lemma emeasure_borel_of: "emeasure (borel_of X) A = 0"
  by (simp add: borel_of_def emeasure_sigma)

lemma borel_of_euclidean: "borel_of euclidean = borel"
  by(simp add: borel_of_def borel_def)

lemma space_borel_of: "space (borel_of X) = topspace X"
  by(simp add: space_measure_of_conv borel_of_def)

lemma sets_borel_of: "sets (borel_of X) = sigma_sets (topspace X) {U. openin X U}"
  by (simp add: subset_Pow_Union topspace_def borel_of_def)

lemma sets_borel_of_closed: "sets (borel_of X) = sigma_sets (topspace X) {U. closedin X U}"
  unfolding sets_borel_of
proof(safe intro!: sigma_sets_eqI)
  fix a
  assume a:"openin X a"
  have "topspace X - (topspace X - a) ∈ sigma_sets (topspace X) {U. closedin X U}"
    by(rule sigma_sets.Compl) (use a in auto)
  thus "a ∈ sigma_sets (topspace X) {U. closedin X U}"
    using openin_subset[OF a] by (simp add: Diff_Diff_Int inf.absorb_iff2) 
next
  fix b
  assume b:"closedin X b"
  have "topspace X - (topspace X - b) ∈ sigma_sets (topspace X) {U. openin X U}"
    by(rule sigma_sets.Compl) (use b in auto)
  thus "b ∈ sigma_sets (topspace X) {U. openin X U}"
    using closedin_subset[OF b] by (simp add: Diff_Diff_Int inf.absorb_iff2) 
qed

lemma borel_of_open:
  assumes "openin X U"
  shows "U ∈ sets (borel_of X)"
  using assms by (simp add: subset_Pow_Union topspace_def borel_of_def)

lemma borel_of_closed:
  assumes "closedin X U"
  shows "U ∈ sets (borel_of X)"
  using assms sigma_sets.Compl[of "topspace X - U" "topspace X"]
  by (simp add: closedin_def double_diff sets_borel_of)

lemma(in Metric_space) nbh_sets[measurable]: "(⋃a∈A. mball a e) ∈ sets (borel_of mtopology)"
  by(auto intro!: borel_of_open openin_clauses(3))

lemma borel_of_gdelta_in:
  assumes "gdelta_in X U"
  shows "U ∈ sets (borel_of X)"
  using gdelta_inD[OF assms] borel_of_open
  by(auto intro!: sets.countable_INT'[of _ id,simplified])

lemma borel_of_subtopology:
 "borel_of (subtopology X U) = restrict_space (borel_of X) U"
proof(rule measure_eqI)
  show "sets (borel_of (subtopology X U)) = sets (restrict_space (borel_of X) U)"
    unfolding restrict_space_eq_vimage_algebra' sets_vimage_algebra sets_borel_of topspace_subtopology space_borel_of Int_commute[of U]
  proof(rule sigma_sets_eqI)
    fix a
    assume "a ∈ Collect (openin (subtopology X U))"
    then obtain T where "openin X T" "a = T ∩ U"
      by(auto simp: openin_subtopology)
    show "a ∈ sigma_sets (topspace X ∩ U) {(λx. x) -` A ∩ (topspace X ∩ U) |A. A ∈ sigma_sets (topspace X) (Collect (openin X))}"
      using openin_subset[OF ‹openin X T›] ‹a = T ∩ U› by(auto intro!: exI[where x=T] ‹openin X T›)
  next
    fix b
    assume "b ∈ {(λx. x) -` A ∩ (topspace X ∩ U) |A. A ∈ sigma_sets (topspace X) (Collect (openin X))}"
    then obtain T where ht:"b = T ∩ (topspace X ∩ U)" "T ∈ sigma_sets (topspace X) (Collect (openin X))"
      by auto
    hence "b = T ∩ U"
    proof -
      have "T ⊆ topspace X"
        by(rule sigma_sets_into_sp[OF _ ht(2)]) (simp add: subset_Pow_Union topspace_def)
      thus ?thesis
        by(auto simp: ht(1))
    qed
    with ht(2) show "b ∈ sigma_sets (topspace X ∩ U) (Collect (openin (subtopology X U)))"
    proof(induction arbitrary: b U)
      case (Basic a)
      then show ?case
        by(auto simp: openin_subtopology)
    next
      case Empty
      then show ?case by simp
    next
      case ih:(Compl a)
      then show ?case
        by (simp add: Diff_Int_distrib2 sigma_sets.Compl)
    next
      case (Union a)
      then show ?case
        by (metis UN_extend_simps(4) sigma_sets.Union)
    qed
  qed
qed(simp add: emeasure_borel_of restrict_space_def emeasure_measure_of_conv)

lemma sets_borel_of_discrete_topology: "sets (borel_of (discrete_topology I)) = sets (count_space I)"
  by (metis Pow_UNIV UNIV_eq_I borel_of_open borel_of_subtopology inf.absorb_iff2 openin_discrete_topology sets_count_space sets_restrict_space sets_restrict_space_count_space subtopology_discrete_topology top_greatest)

lemma continuous_map_measurable:
  assumes "continuous_map X Y f"
  shows "f ∈ borel_of X →⇩M borel_of Y"
proof(rule measurable_sigma_sets[OF sets_borel_of[of Y]])
  show "{U. openin Y U} ⊆ Pow (topspace Y)"
    by (simp add: subset_Pow_Union topspace_def)
next
  show "f ∈ space (borel_of X) → topspace Y"
    using continuous_map_image_subset_topspace[OF assms]
    by(auto simp: space_borel_of)
next
  fix U
  assume "U ∈ {U. openin Y U}"
  then have "openin X (f -` U ∩ topspace X)"
    using continuous_map[of X Y f] assms by auto
  thus "f -` U ∩ space (borel_of X) ∈ sets (borel_of X)"
    by(simp add: space_borel_of sets_borel_of)
qed

lemma upper_semicontinuous_map_measurable:
  fixes f :: "'a ⇒ 'b :: {linorder_topology, second_countable_topology}"
  assumes "upper_semicontinuous_map X f"
  shows "f ∈ borel_measurable (borel_of X)"
  using assms by(auto intro!: borel_measurableI_less borel_of_open simp: space_borel_of upper_semicontinuous_map_def)

lemma lower_semicontinuous_map_measurable:
  fixes f :: "'a ⇒ 'b :: {linorder_topology, second_countable_topology}"
  assumes "lower_semicontinuous_map X f"
  shows "f ∈ borel_measurable (borel_of X)"
  using assms by(auto intro!: borel_measurableI_greater borel_of_open simp: space_borel_of lower_semicontinuous_map_def)

lemma open_map_preserves_sets:
  assumes "open_map S T f" "inj_on f (topspace S)" "A ∈ sets (borel_of S)"
  shows "f ` A ∈ sets (borel_of T)"
  using assms(3)[simplified sets_borel_of]
proof(induction)
  case (Basic a)
  with assms(1) show ?case
    by(auto simp: sets_borel_of open_map_def)
next
  case Empty
  show ?case by simp
next
  case (Compl a)
  moreover have "f ` (topspace S - a) = f ` (topspace S) - f ` a"
    by (metis Diff_subset assms(2) calculation(1) inj_on_image_set_diff sigma_sets_into_sp subset_Pow_Union topspace_def)
  moreover have "f ` (topspace S) ∈ sets (borel_of T)"
    by (meson assms(1) borel_of_open open_map_def openin_topspace)
  ultimately show ?case
    by auto
next
  case (Union a)
  then show ?case
    by (simp add: image_UN)
qed

lemma open_map_preserves_sets':
  assumes "open_map S (subtopology T (f ` (topspace S))) f" "inj_on f (topspace S)" "f ` (topspace S) ∈ sets (borel_of T)" "A ∈ sets (borel_of S)"
  shows "f ` A ∈ sets (borel_of T)"
  using assms(4)[simplified sets_borel_of]
proof(induction)
  case (Basic a)
  then have "openin (subtopology T (f ` (topspace S))) (f ` a)"
    using assms(1) by(auto simp: open_map_def)
  hence "f ` a ∈ sets (borel_of (subtopology T (f ` (topspace S))))"
    by(simp add: sets_borel_of)
  hence "f ` a ∈ sets (restrict_space (borel_of T) (f ` (topspace S)))"
    by(simp add: borel_of_subtopology)
  thus ?case
    by (metis sets_restrict_space_iff assms(3) sets.Int_space_eq2)
next
  case Empty
  show ?case by simp
next
  case (Compl a)
  moreover have "f ` (topspace S - a) = f ` (topspace S) - f ` a"
    by (metis Diff_subset assms(2) calculation(1) inj_on_image_set_diff sigma_sets_into_sp subset_Pow_Union topspace_def)
  ultimately show ?case
    using assms(3) by auto
next
  case (Union a)
  then show ?case
    by (simp add: image_UN)
qed


text ‹ Abstract topology version of @{thm second_countable_borel_measurable}. ›
lemma borel_of_second_countable':
  assumes "second_countable S" and "subbase_in S 𝒰"
  shows "borel_of S = sigma (topspace S) 𝒰"
  unfolding borel_of_def
proof(rule sigma_eqI)
  show "{U. openin S U} ⊆ Pow (topspace S)"
    by (simp add: subset_Pow_Union topspace_def)
next
  show "𝒰 ⊆ Pow (topspace S)"
    using subbase_in_subset[OF assms(2)] by auto
next
  interpret s: sigma_algebra "topspace S" "sigma_sets (topspace S) 𝒰"
    using subbase_in_subset[OF assms(2)] by(auto intro!: sigma_algebra_sigma_sets)
  obtain 𝒪 where ho: "countable 𝒪" "base_in S 𝒪"
    using assms(1) by(auto simp: second_countable_base_in)
  show "sigma_sets (topspace S) {U. openin S U} = sigma_sets (topspace S) 𝒰"
  proof(rule sigma_sets_eqI)
    fix U
    assume "U ∈ {U. openin S U}"
    then have "generate_topology_on 𝒰 U"
      using assms(2) by(simp add: subbase_in_def openin_topology_generated_by_iff)
    thus "U ∈ sigma_sets (topspace S) 𝒰"
    proof induction
      case (UN K)
      with ho(2) obtain V where hv:
       "⋀k. k ∈ K ⟹ V k ⊆ 𝒪" "⋀k. k ∈ K ⟹ ⋃ (V k) = k"
        by(simp add: base_in_def openin_topology_generated_by_iff[symmetric] assms(2)[simplified subbase_in_def,symmetric]) metis
      define 𝒰k where "𝒰k = (⋃k∈K. V k)"
      have 0:"countable 𝒰k"
        using hv by(auto intro!: countable_subset[OF _ ho(1)] simp: 𝒰k_def)
      have "⋃ 𝒰k = (⋃A∈𝒰k. A)" by auto
      also have "... = ⋃ K"
        unfolding 𝒰k_def UN_simps by(simp add: hv(2))
      finally have 1:"⋃ 𝒰k = ⋃ K" .
      have "∀b∈𝒰k. ∃k∈K. b ⊆ k"
        using hv by (auto simp: 𝒰k_def)
      then obtain V' where hv': "⋀b. b ∈ 𝒰k ⟹ V' b ∈ K" and "⋀b. b ∈ 𝒰k ⟹ b ⊆ V' b"
        by metis
      then have "(⋃b∈𝒰k. V' b) ⊆ ⋃K" "⋃𝒰k ⊆ (⋃b∈𝒰k. V' b)"
        by auto
      then have "⋃K = (⋃b∈𝒰k. V' b)"
        unfolding 1 by auto
      also have "… ∈ sigma_sets (topspace S) 𝒰"
        using hv' UN by(auto intro!: s.countable_UN' simp: 0)
      finally show "⋃K ∈ sigma_sets (topspace S) 𝒰" .
    qed auto
  next
    fix U
    assume "U ∈ 𝒰"
    from assms(2)[simplified subbase_in_def] openin_topology_generated_by_iff generate_topology_on.Basis[OF this]
    show "U ∈ sigma_sets (topspace S) {U. openin S U}"
      by auto
  qed
qed

text ‹ Abstract topology version @{thm borel_prod}.›
lemma borel_of_prod:
  assumes "second_countable S" and "second_countable S'"
  shows "borel_of S ⨂⇩M borel_of S' = borel_of (prod_topology S S')"
proof -
  have "borel_of S ⨂⇩M borel_of S' = sigma (topspace S × topspace S') {a × b |a b. a ∈ {a. openin S a} ∧ b ∈ {b. openin S' b}}"
  proof -
    obtain 𝒪 𝒪' where ho:
    "countable 𝒪" "base_in S 𝒪" "countable 𝒪'" "base_in S' 𝒪'"
      using assms by(auto simp: second_countable_base_in)
    show ?thesis
      unfolding borel_of_def
      apply(rule sigma_prod)
      using topology_generated_by_topspace[of 𝒪,simplified base_is_subbase[OF ho(2),simplified subbase_in_def,symmetric]] topology_generated_by_topspace[of 𝒪',simplified base_is_subbase[OF ho(4),simplified subbase_in_def,symmetric]]
              base_in_openin[OF ho(2)] base_in_openin[OF ho(4)]
      by(auto intro!: exI[where x=𝒪] exI[where x=𝒪'] simp: ho subset_Pow_Union topspace_def)
  qed
  also have "... = borel_of (prod_topology S S')"
    using borel_of_second_countable'[OF prod_topology_second_countable[OF assms],simplified subbase_in_def,OF prod_topology_generated_by_open]
    by simp
  finally show ?thesis .
qed

lemma product_borel_of_measurable:
  assumes "i ∈ I"
  shows "(λx. x i) ∈ (borel_of (product_topology S I)) →⇩M borel_of (S i)"
  by(auto intro!: continuous_map_measurable simp: assms)


text ‹ Abstract topology version of @{thm sets_PiM_subset_borel} ›
lemma sets_PiM_subset_borel_of:
  "sets (Π⇩M i∈I. borel_of (S i)) ⊆ sets (borel_of (product_topology S I))"
proof -
  have *: "(Π⇩E i∈I. X i) ∈ sets (borel_of (product_topology S I))" if [measurable]:"⋀i. X i ∈ sets (borel_of (S i))" "finite {i. X i ≠ topspace (S i)}" for X
  proof -
    note [measurable] = product_borel_of_measurable
    define I' where "I' = {i. X i ≠ topspace (S i)} ∩ I"
    have "finite I'" unfolding I'_def using that by simp
    have "(Π⇩E i∈I. X i) = (⋂i∈I'. (λx. x i)-`(X i) ∩ space (borel_of (product_topology S I))) ∩ space (borel_of (product_topology S I))"
    proof(standard;standard)
      fix x
      assume "x ∈ Pi⇩E I X"
      then show "x ∈ (⋂i∈I'. (λx. x i) -` X i ∩ space (borel_of (product_topology S I))) ∩ space (borel_of (product_topology S I))"
        using sets.sets_into_space[OF that(1)] by(auto simp: PiE_def I'_def Pi_def space_borel_of)
    next
      fix x
      assume 1:"x ∈ (⋂i∈I'. (λx. x i) -` X i ∩ space (borel_of (product_topology S I))) ∩ space (borel_of (product_topology S I))"
      have "x i ∈ X i" if hi:"i ∈ I" for i
      proof -
        consider "i ∈ I' ∧ I' ≠ {}" | "i ∉ I' ∧ I' = {}" | "i ∉ I' ∧ I' ≠ {}" by auto
        then show ?thesis
          apply cases
          using sets.sets_into_space[OF ‹⋀i. X i ∈ sets (borel_of (S i))›] 1 that
          by(auto simp: space_borel_of I'_def)
      qed
      then show "x ∈ Pi⇩E I X"
        using 1 by(auto simp: space_borel_of)
    qed
    also have "... ∈ sets (borel_of (product_topology S I))"
     using that ‹finite I'› by(auto simp: I'_def)
    finally show ?thesis .
  qed
  then have "{Pi⇩E I X |X. (∀i. X i ∈ sets (borel_of (S i))) ∧ finite {i. X i ≠ space (borel_of (S i))}} ⊆ sets (borel_of (product_topology S I))"
    by(auto simp: space_borel_of)
  show ?thesis unfolding sets_PiM_finite
    by(rule sets.sigma_sets_subset',fact) (simp add: borel_of_open[OF openin_topspace, of "product_topology S I",simplified] space_borel_of)
qed

text ‹ Abstract topology version of @{thm sets_PiM_equal_borel}.›
lemma sets_PiM_equal_borel_of:
  assumes "countable I" and "⋀i. i ∈ I ⟹ second_countable (S i)"
  shows "sets (Π⇩M i∈I. borel_of (S i)) = sets (borel_of (product_topology S I))"
proof
  obtain K where hk:
  "countable K" "base_in (product_topology S I) K"
  "⋀k. k ∈ K ⟹ ∃X. (k = (Π⇩E i∈I. X i)) ∧ (∀i. openin (S i) (X i)) ∧ finite {i. X i ≠ topspace (S i)} ∧ {i. X i ≠ topspace (S i)} ⊆ I"
    using product_topology_countable_base_in[OF assms(1)] assms(2)
    by force
  have *:"k ∈ sets (Π⇩M i∈I. borel_of (S i))" if "k ∈ K" for k
  proof -
    obtain X where H: "k = (Π⇩E i∈I. X i)" "⋀i. openin (S i) (X i)" "finite {i. X i ≠ topspace (S i)}" "{i. X i ≠ topspace (S i)} ⊆ I"
      using hk(3)[OF ‹k ∈ K›] by blast
    show ?thesis unfolding H(1) sets_PiM_finite
      using borel_of_open[OF H(2)] H(3) by(auto simp: space_borel_of)
  qed
  have **: "U ∈ sets (Π⇩M i∈I. borel_of (S i))" if "openin (product_topology S I) U" for U
  proof -
    obtain B where "B ⊆ K" "U = (⋃B)"
      using ‹openin (product_topology S I) U› ‹base_in (product_topology S I) K› by (metis base_in_def)
    have "countable B" using ‹B ⊆ K› ‹countable K› countable_subset by blast
    moreover have "k ∈ sets (Π⇩M i∈I. borel_of (S i))" if "k ∈ B" for k
      using ‹B ⊆ K› * that by auto
    ultimately show ?thesis unfolding ‹U = (⋃B)› by auto
  qed
  have "sigma_sets (topspace (product_topology S I)) {U. openin (product_topology S I) U} ⊆ sets (Π⇩M i∈I. borel_of (S i))"
    apply (rule sets.sigma_sets_subset') using ** by(auto intro!: sets_PiM_I_countable[OF assms(1)] simp: borel_of_open[OF openin_topspace])
  thus " sets (borel_of (product_topology S I)) ⊆ sets (Π⇩M i∈I. borel_of (S i))"
    by (simp add: subset_Pow_Union topspace_def borel_of_def) 
qed(rule sets_PiM_subset_borel_of)

lemma homeomorphic_map_borel_isomorphic:
  assumes "homeomorphic_map X Y f"
  shows "measurable_isomorphic_map (borel_of X) (borel_of Y) f"
proof -
  obtain g where "homeomorphic_maps X Y f g"
    using assms by(auto simp: homeomorphic_map_maps)
  hence "continuous_map X Y f" "continuous_map Y X g"
        "⋀x. x ∈ topspace X ⟹ g (f x) = x"
        "⋀y. y ∈ topspace Y ⟹ f (g y) = y"
    by(auto simp: homeomorphic_maps_def)
  thus ?thesis
    by(auto intro!: measurable_isomorphic_map_byWitness dest: continuous_map_measurable simp: space_borel_of)
qed

lemma homeomorphic_space_measurable_isomorphic:
  assumes "S homeomorphic_space T"
  shows "borel_of S measurable_isomorphic borel_of T"
  using homeomorphic_map_borel_isomorphic[of S T] assms by(auto simp: measurable_isomorphic_def homeomorphic_space)

lemma measurable_isomorphic_borel_map:
  assumes "sets M = sets (borel_of S)" and f: "measurable_isomorphic_map M N f"
  shows "∃S'. homeomorphic_map S S' f ∧ sets N = sets (borel_of S')"
proof -
  obtain g where fg:"f ∈ M →⇩M N" "g ∈ N →⇩M M" "⋀x. x∈space M ⟹ g (f x) = x" "⋀y. y∈space N ⟹ f (g y) = y" "⋀A. A∈sets M ⟹ f ` A ∈ sets N" "⋀A. A∈sets N ⟹ g ` A ∈ sets M" "bij_betw g (space N) (space M)"
    using measurable_isomorphic_mapD'[OF f] by metis
  have g:"measurable_isomorphic_map N M g"
    by(auto intro!: measurable_isomorphic_map_byWitness fg)
  have g':"bij_betw g (space N) (topspace S)"
    using fg(7) sets_eq_imp_space_eq[OF assms(1)] by(auto simp: space_borel_of)
  show ?thesis
  proof(intro exI[where x="pullback_topology (space N) g S"] conjI)
    have [simp]: "{U. openin (pullback_topology (space N) g S) U} = (`) f ` {U. openin S U}"
      unfolding openin_pullback_topology'[OF g']
    proof safe
      fix u
      assume u:"openin S u"
      then have 1:"u ⊆ space M"
        by(simp add: sets_eq_imp_space_eq[OF assms(1)] space_borel_of openin_subset)
      with fg(3) have "g ` f ` u = u"
        by(fastforce simp: image_def)
      with u show "openin S (g ` f ` u)" by simp
      fix x
      assume "x ∈ u"
      with 1 fg(1) show "f x ∈ space N" by(auto simp: measurable_space)
    next
      fix u
      assume "openin S (g ` u)" "u ⊆ space N"
      with fg(4) show "u ∈ (`) f ` {U. openin S U}"
        by(auto simp: image_def intro!: exI[where x="g ` u"]) (metis in_mono)
    qed
    have [simp]:"g -` topspace S ∩ space N = space N"
      using bij_betw_imp_surj_on g' by blast
    show "sets N = sets (borel_of (pullback_topology (space N) g S))"
      by(auto simp: sets_borel_of topspace_pullback_topology intro!: measurable_isomorphic_map_sigma_sets[OF assms(1)[simplified sets_borel_of space_borel_of[symmetric] sets_eq_imp_space_eq[OF assms(1),symmetric]] f])
  next
    show "homeomorphic_map S (pullback_topology (space N) g S) f"
    proof(rule homeomorphic_maps_imp_map[where g=g])
      obtain f' where f':"homeomorphic_maps (pullback_topology (space N) g S) S g f'"
        using topology_from_bij(1)[OF g'] homeomorphic_map_maps by blast
      have f'2:"f' y = f y" if y:"y ∈ topspace S" for y
      proof -
        have [simp]:"g -` topspace S ∩ space N = space N"
          using bij_betw_imp_surj_on g' by blast
        obtain x where "x ∈ space N" "y = g x"
          using g' y by(auto simp: bij_betw_def image_def)
        thus ?thesis
          using fg(4) f' by(auto simp: homeomorphic_maps_def topspace_pullback_topology)
      qed
      thus "homeomorphic_maps S (pullback_topology (space N) g S) f g"
        by(auto intro!: homeomorphic_maps_eq[OF f'] simp: homeomorphic_maps_sym[of S])
    qed
  qed
qed

lemma measurable_isomorphic_borels:
  assumes "sets M = sets (borel_of S)" "M measurable_isomorphic N"
  shows "∃S'. S homeomorphic_space S' ∧ sets N = sets (borel_of S')"
  using measurable_isomorphic_borel_map[OF assms(1)] assms(2) homeomorphic_map_maps
  by(fastforce simp: measurable_isomorphic_def homeomorphic_space_def )

end