Theory Standard_Borel_Spaces.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="kK. 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 "zU. 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. zU. 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 "zU. 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. zU. 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. zU  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 = (zU. (V1 z) × (V2 z))"
    by auto
  have "openin (topology_generated_by {U × V |U V. U  𝒪  V  𝒰}) (zU. (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 iI. X i |X. (i. openin (S i) (X i))  finite {i. X i  topspace (S i)}}  {ΠE iI. 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 iI. X i |X. (i. openin (S i) (X i))  finite {i. X i  topspace (S i)}}"
    then obtain X where hX:
     "x = (ΠE iI. 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 iI. 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 iI. 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 iI. X i |X. (i. openin (S i) (X i))  finite {i. X i  topspace (S i)}} = {ΠE iI. 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  {xtopspace X  A. x  X derived_set_of A}"

lemma isolated_points_of_eq:
 "X isolated_points_of A = {xtopspace 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  yx. 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  yx. 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  yx. 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  (xU. W𝒪. x  W  W  U))"
proof
  assume h:"base_in S 𝒪"
  show "U. openin S U  (xU. 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  (xU. W𝒪. x  W  W  U)"
  show "base_in S 𝒪"
    unfolding base_in_def
  proof safe
    fix U
    assume "openin S U"
    then have "xU. W. W𝒪  x  W  W  U"
      using h by blast
    hence "W. xU. W x  𝒪  x  W x  W x  U"
      by(rule bchoice)
    then obtain W where hw:
     "xU. 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 iI. 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 iI. U i | U. finite {iI. U i  topspace (S i)}  (i{iI. U i  topspace (S i)}. U i  𝒪 i)}"] conjI)
    show "countable {ΠE iI. U i | U. finite {iI. U i  topspace (S i)}  (i{iI. U i  topspace (S i)}. U i  𝒪 i)}"
         (is "countable ?X")
    proof -
      have "?X  = {ΠE iI. U i | U. finite {iI. U i  topspace (S i)}  (i{iI. 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 iI. U i)" "finite {iI. U i  topspace (S i)}" "(i{iI. 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 iI. U' i)"
            using hu(1) by(auto simp: U'_def PiE_def extensional_def Pi_def)
          moreover have "finite {iI. U' i  topspace (S i)}" "(i{iI. 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 iI. U i) ` {U. finite {iI. U i  topspace (S i)}  (i{iI. 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)  (iUNIV - I. U i = {undefined})} = {U. I'. finite I'  I'  I  (iI'. U i  𝒪 i)  (i(I - I'). U i = topspace (S i))  (iUNIV - 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)  (iUNIV - I. U i = {undefined})}"
            then show "U  {U. I'. finite I'  I'  I  (iI'. U i  𝒪 i)  (iI - I'. U i = topspace (S i))  (iUNIV - I. U i = {undefined})}"
              by auto
          next
            fix U
            assume assm:"U  {U. I'. finite I'  I'  I  (iI'. U i  𝒪 i)  (iI - I'. U i = topspace (S i))  (iUNIV - I. U i = {undefined})}"
            then obtain I' where hi':
               "finite I'" "I'  I" "iI'. U i  𝒪 i" "iI - I'. U i = topspace (S i)" "iUNIV - 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)  (iUNIV - I. U i = {undefined})}"
              using hi' by auto
          qed
        qed
        also have "... = (I'{I'. finite I'  I'  I}. {U. (iI'. U i  𝒪 i)  (iI - I'. U i = topspace (S i))  (iUNIV - 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. (iI'. U i  𝒪 i)  (iI - I'. U i = topspace (S i))  (iUNIV - I. U i = {undefined})}  (ΠE iI'. 𝒪 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. (iI'. U i  𝒪 i)  (iI - I'. U i = topspace (S i))  (iUNIV - I. U i = {undefined})})"
            by(simp add: countable_subset)
          moreover have "inj_on (λU i. if i  I' then U i else undefined) {U. (iI'. U i  𝒪 i)  (iI - I'. U i = topspace (S i))  (iUNIV - 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. (iI'. U i  𝒪 i)  (iI - I'. U i = topspace (S i))  (iUNIV - 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)  (iUNIV - I. U i = {undefined})}" .
      qed
      finally show ?thesis .
    qed
  next
    show "base_in (product_topology S I) {ΠE iI. 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 "xU. Ux. finite {i  I. Ux i  topspace (S i)}  (iI. openin (S i) (Ux i))  x  PiE I Ux  PiE I Ux  U"
        by(simp add: openin_product_topology_alt)
      hence "Ux. xU. finite {i  I. Ux x i  topspace (S i)}  (iI. openin (S i) (Ux x i))  x  PiE I (Ux x)  PiE 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  PiE I (Ux x)" "x. x  U  PiE I (Ux x)  U"
        by fastforce
      then have 1:"xU. 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 "xU. 𝒰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. xU. 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
       "xU. 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 iI. K i | K. xU. finite {i  I. Ux x i  topspace (S i)}  (i{i  I. Ux x i  topspace (S i)}. K i  𝒰xj x i)  (iUNIV -{i  I. Ux x i  topspace (S i)}. K i = topspace (S i))}"] conjI)
        show "U =  {ΠE iI. K i | K. xU. finite {i  I. Ux x i  topspace (S i)}  (i{i  I. Ux x i  topspace (S i)}. K i  𝒰xj x i)  (iUNIV -{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 iI. 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 "xU. finite {i  I. Ux x i  topspace (S i)}  (i{i  I. Ux x i  topspace (S i)}. K i  𝒰xj x i)  (iUNIV -{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 iI. K i | K. xU. finite {i  I. Ux x i  topspace (S i)}  (i{i  I. Ux x i  topspace (S i)}. K i  𝒰xj x i)  (iUNIV -{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 iI. 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" "iUNIV -{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 iI. K i | K. xU. finite {i  I. Ux x i  topspace (S i)}  (i{i  I. Ux x i  topspace (S i)}. K i  𝒰xj x i)  (iUNIV -{i  I. Ux x i  topspace (S i)}. K i = topspace (S i))}  ?X"
        proof
          fix x
          assume "x  {ΠE iI. K i | K. xU. finite {i  I. Ux x i  topspace (S i)}  (i{i  I. Ux x i  topspace (S i)}. K i  𝒰xj x i)  (iUNIV -{i  I. Ux x i  topspace (S i)}. K i = topspace (S i))}"
          then obtain u K where hu:
           "x = (ΠE iI. 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" "iUNIV -{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 iI. 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 iI. 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{PiE I U |U. finite {i  I. U i  topspace (S i)}  (i{i  I. U i  topspace (S i)}. U i  𝒪 i)}. X. k = PiE 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  {PiE 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 iI. 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 iI. 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 iI. 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 iI. 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)}" "iI. openin (T i) (K i)" "x  (ΠE iI. K i)" "(ΠE iI. 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 iI. U i)  (ΠE iI. K i)  {}"
    by (simp add: PiE_Int PiE_eq_empty_iff) 
  thus "(ΠE iI. U i)  V  {}"
    using hk by auto
next
  show "(ΠE iI. 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 "iI. 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. iI. x i  topspace (T i)" "U. iI. 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 iI. U' J i | J. finite J  J  I}"] conjI)
      have "({ ΠE iI. U' J i | J. finite J  J  I}) = ( ((λJ. ΠE iI. 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. (λiJ. f i, λi(I-J). f i)) (ΠE iI. U' J i)"
        proof(rule inj_onI)
          fix f g
          assume h:"f  PiE I (U' J)" "g  PiE 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. (λiJ. f i, λi(I-J). f i)) ` (ΠE iI. U' J i))" (is "countable ?K")
        proof -
          have 1:"?K  (ΠE iJ. 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 (PiE J U)"
              using hj hxu(2) by(auto intro!: countable_PiE)
          next
            have "(ΠE iI - J. {x i}) = { λiI-J. x i }"
              by(auto simp: PiE_def extensional_def restrict_def Pi_def)
            thus "countable (ΠE iI - J. {x i})"
              by simp
          qed
          show ?thesis
            by(rule countable_subset[OF 1 2])
        qed
        ultimately show "countable (ΠE iI. U' J i)"
          by(simp add: countable_image_inj_eq)
      qed(rule countable_Collect_finite_subset[OF assms(1)])
      finally show "countable ({ ΠE iI. U' J i | J. finite J  J  I})" .
    next
      show "dense_in (product_topology T I) ( {ΠE iI. 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. iI  openin (T i) (K i)" "y  (ΠE iI. K i)" "(ΠE iI. 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 iI. U' {i  I. K i  topspace (T i)} i)  (ΠE iI. K i)"
          using 4 5 hz by(auto simp: U'_def)
        thus " {PiE I (U' J) |J. finite J  J  I}  V  {}"
          using hk(1,4) by blast
      next
        have "J. J  I  (ΠE iI. 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 iI. 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" "xU - {a}. P x"
    by (auto simp: eventually_atin limitin_topspace)
  with h(3) obtain N where "nN. 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  {VB'. 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. in. 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 "bAn 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. nN. 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:"xtopspace 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. nN. f (σ n)  U)"
      using limfx by(auto simp: limitin_def eventually_atin_sequentially[OF assms(1)] eventually_sequentially)
    show "N. nN. 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. nN. 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. nN. 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 {xtopspace 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 {xtopspace 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 {xtopspace 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 {xtopspace 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}  {Usigma_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)  (Asets 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)  (Asets 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  (xspace M. the_inv_into (space M) f (f x) = x)  (xspace N. f (the_inv_into (space M) f x) = x)  (Asets 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. xspace M  f' (f x) = x" "x. xspace N  f (f' x) = x"
  and [measurable]: "g'  L M N" and hg:"x. xspace N  g' (g x) = x" "x. xspace 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  (xspace M. g (f x) = x)  (yspace N. f (g y) = y)  (Asets M. f ` A  sets N)  (Asets 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. xspace M  g (f x) = x"
      and "g  N M M" "y. yspace 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 iI. M i) M (ΠM iI. 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 iI. M i) (ΠM iI. 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  xspace (M i)  h' i (h i x) = x" "i x. i  I  xspace (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 iI. M i) measurable_isomorphic  (ΠM iI. 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. xspace M  f' (f x) = x" "x. xf ` space M  f (f' x) = x"
             "x. xspace N  g' (g x) = x" "x. xg ` 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  (nUNIV. 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 xI. 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. λiI. x (to_nat_on I i)"])
  show "(λx n. x (from_nat_into I n))  (ΠM xI. 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. λiI. x (to_nat_on I i))  (ΠM (x::nat)UNIV. M) M (ΠM xI. M)"
    by(auto intro!: measurable_PiM_single')
next
  show "x  space (ΠM xI. M)  (λiI. 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 (PiM UNIV (λx. M))  (λn. (λiI. 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 iI. ΠM jJ. 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 iI. ΠM jJ. 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 jJ. 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 iI. ΠM jJ. 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))   PiM (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 iI. ΠM jJ. M i j)"
    by(auto intro!: measurable_PiM_single') (simp_all add: PiE_iff space_PiM extensional_def)
next
  show "x  space (ΠM iI. ΠM jJ. 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. xspace M  g (f x) = x" "x. xspace N  f (g x) = x" "A. Asets 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]: "(aA. 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 = (kK. 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. kK. 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 iI. borel_of (S i))  sets (borel_of (product_topology S I))"
proof -
  have *: "(ΠE iI. 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 iI. X i) = (iI'. (λ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  PiE I X"
      then show "x  (iI'. (λ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  (iI'. (λ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  PiE 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 "{PiE 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 iI. 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 iI. 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 iI. borel_of (S i))" if "k  K" for k
  proof -
    obtain X where H: "k = (ΠE iI. 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 iI. 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 iI. 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 iI. 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 iI. 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. xspace M  g (f x) = x" "y. yspace N  f (g y) = y" "A. Asets M  f ` A  sets N" "A. Asets 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