Theory Lemmas_StandardBorel
text ‹ We refer to the HOL-Analysis library,
the textbooks by Matsuzaka~\cite{topology} and Srivastava~\cite{borelsets},
and the lecture note by Biskup~\cite{standardborel}.›
section ‹Lemmas›
theory Lemmas_StandardBorel
imports "HOL-Probability.Probability"
begin
subsection ‹Lemmas for Abstract Topology›
subsubsection ‹ Generated By ›
lemma topology_generated_by_sub:
assumes "⋀U. U ∈ 𝒰 ⟹ (openin X U)"
and "openin (topology_generated_by 𝒰) U"
shows "openin X U"
proof -
have "generate_topology_on 𝒰 U"
by (simp add: assms(2) openin_topology_generated_by)
then show ?thesis
by induction (use assms(1) in auto)
qed
lemma topology_generated_by_open:
"S = topology_generated_by {U | U . openin S U}"
unfolding topology_eq
proof standard+
fix U
assume "openin (topology_generated_by {U |U. openin S U}) U"
note this[simplified openin_topology_generated_by_iff]
then show "openin S U"
by induction auto
qed(simp add: openin_topology_generated_by_iff generate_topology_on.Basis)
lemma topology_generated_by_eq:
assumes "⋀U. U ∈ 𝒰 ⟹ (openin (topology_generated_by 𝒪) U)"
and "⋀U. U ∈ 𝒪 ⟹ (openin (topology_generated_by 𝒰) U)"
shows "topology_generated_by 𝒪 = topology_generated_by 𝒰"
using topology_generated_by_sub[of 𝒰, OF assms(1)] topology_generated_by_sub[of 𝒪,OF assms(2)]
by(auto simp: topology_eq)
lemma topology_generated_by_homeomorphic_spaces:
assumes "homeomorphic_map X Y f" "X = topology_generated_by 𝒪"
shows "Y = topology_generated_by ((`) f ` 𝒪)"
unfolding topology_eq
proof
have f:"open_map X Y f" "inj_on f (topspace X)"
using assms(1) by (simp_all add: homeomorphic_imp_open_map perfect_injective_eq_homeomorphic_map[symmetric])
obtain g where g: "⋀x. x ∈ topspace X ⟹ g (f x) = x" "⋀y. y ∈ topspace Y ⟹ f (g y) = y" "open_map Y X g" "inj_on g (topspace Y)"
using homeomorphic_map_maps[of X Y f,simplified assms(1)] homeomorphic_imp_open_map homeomorphic_maps_map[of X Y f] homeomorphic_imp_injective_map[of Y X] by blast
show "⋀S. openin Y S = openin (topology_generated_by ((`) f ` 𝒪)) S"
proof safe
fix S
assume "openin Y S"
then have "openin X (g ` S)"
using g(3) by (simp add: open_map_def)
hence h:"generate_topology_on 𝒪 (g ` S)"
by(simp add: assms(2) openin_topology_generated_by_iff)
have "S = f ` (g ` S)"
using openin_subset[OF ‹openin Y S›] g(2) by(fastforce simp: image_def)
also have "openin (topology_generated_by ((`) f ` 𝒪)) ..."
using h
proof induction
case Empty
then show ?case by simp
next
case (Int a b)
with inj_on_image_Int[OF f(2),of a b] show ?case
by (metis assms(2) openin_Int openin_subset openin_topology_generated_by_iff)
next
case (UN K)
then show ?case
by(auto simp: image_Union)
next
case (Basis s)
then show ?case
by(auto intro!: generate_topology_on.Basis simp: openin_topology_generated_by_iff)
qed
finally show "openin (topology_generated_by ((`) f ` 𝒪)) S" .
next
fix S
assume "openin (topology_generated_by ((`) f ` 𝒪)) S"
then have "generate_topology_on ((`) f ` 𝒪) S"
by(simp add: openin_topology_generated_by_iff)
thus "openin Y S"
proof induction
case (Basis s)
then obtain U where u:"U ∈ 𝒪" "s = f ` U" by auto
then show ?case
using assms(1) assms(2) homeomorphic_map_openness_eq topology_generated_by_Basis by blast
qed auto
qed
qed
lemma open_map_generated_topo:
assumes "⋀u. u ∈ U ⟹ openin S (f ` u)" "inj_on f (topspace (topology_generated_by U))"
shows "open_map (topology_generated_by U) S f"
unfolding open_map_def
proof safe
fix u
assume "openin (topology_generated_by U) u"
then have "generate_topology_on U u"
by(simp add: openin_topology_generated_by_iff)
thus "openin S (f ` u)"
proof induction
case (Int a b)
then have [simp]:"f ` (a ∩ b) = f ` a ∩ f ` b"
by (meson assms(2) inj_on_image_Int openin_subset openin_topology_generated_by_iff)
from Int show ?case by auto
qed (simp_all add: image_Union openin_clauses(3) assms)
qed
lemma subtopology_generated_by:
"subtopology (topology_generated_by 𝒪) T = topology_generated_by {T ∩ U | U. U ∈ 𝒪}"
unfolding topology_eq openin_subtopology openin_topology_generated_by_iff
proof safe
fix A
assume "generate_topology_on 𝒪 A"
then show "generate_topology_on {T ∩ U |U. U ∈ 𝒪} (A ∩ T)"
proof induction
case Empty
then show ?case
by (simp add: generate_topology_on.Empty)
next
case (Int a b)
moreover have "a ∩ b ∩ T = (a ∩ T) ∩ (b ∩ T)" by auto
ultimately show ?case
by(auto intro!: generate_topology_on.Int)
next
case (UN K)
moreover have "(⋃ K ∩ T) = (⋃ { k ∩ T | k. k ∈ K})" by auto
ultimately show ?case
by(auto intro!: generate_topology_on.UN)
next
case (Basis s)
then show ?case
by(auto intro!: generate_topology_on.Basis)
qed
next
fix A
assume "generate_topology_on {T ∩ U |U. U ∈ 𝒪} A"
then show "∃L. generate_topology_on 𝒪 L ∧ A = L ∩ T"
proof induction
case Empty
show ?case
by(auto intro!: exI[where x="{}"] generate_topology_on.Empty)
next
case ih:(Int a b)
then obtain La Lb where
"generate_topology_on 𝒪 La" "a = La ∩ T" "generate_topology_on 𝒪 Lb" "b = Lb ∩ T"
by auto
thus ?case
using ih by(auto intro!: exI[where x="La ∩ Lb"] generate_topology_on.Int)
next
case ih:(UN K)
then obtain L where
"⋀k. k ∈ K ⟹ generate_topology_on 𝒪 (L k) " "⋀k. k ∈ K ⟹ k = (L k) ∩ T"
by metis
thus ?case
using ih by(auto intro!: exI[where x="⋃k∈K. L k"] generate_topology_on.UN)
next
case (Basis s)
then show ?case
using generate_topology_on.Basis by fastforce
qed
qed
lemma prod_topology_generated_by:
"topology_generated_by { U × V | U V. U ∈ 𝒪 ∧ V ∈ 𝒰} = prod_topology (topology_generated_by 𝒪) (topology_generated_by 𝒰)"
unfolding topology_eq
proof safe
fix U
assume h:"openin (topology_generated_by {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒰}) U"
show "openin (prod_topology (topology_generated_by 𝒪) (topology_generated_by 𝒰)) U"
by(auto simp: openin_prod_Times_iff[of "topology_generated_by 𝒪" "topology_generated_by 𝒰"]
intro!: topology_generated_by_Basis topology_generated_by_sub[OF _ h])
next
fix U
assume "openin (prod_topology (topology_generated_by 𝒪) (topology_generated_by 𝒰)) U"
then have "∀z∈U. ∃V1 V2. openin (topology_generated_by 𝒪) V1 ∧ openin (topology_generated_by 𝒰) V2 ∧ fst z ∈ V1 ∧ snd z ∈ V2 ∧ V1 × V2 ⊆ U"
by(auto simp: openin_prod_topology_alt)
hence "∃V1. ∀z∈U. ∃V2. openin (topology_generated_by 𝒪) (V1 z) ∧ openin (topology_generated_by 𝒰) V2 ∧ fst z ∈ (V1 z) ∧ snd z ∈ V2 ∧ (V1 z) × V2 ⊆ U"
by(rule bchoice)
then obtain V1 where "∀z∈U. ∃V2. openin (topology_generated_by 𝒪) (V1 z) ∧ openin (topology_generated_by 𝒰) V2 ∧ fst z ∈ (V1 z) ∧ snd z ∈ V2 ∧ (V1 z) × V2 ⊆ U"
by auto
hence "∃V2. ∀z∈U. openin (topology_generated_by 𝒪) (V1 z) ∧ openin (topology_generated_by 𝒰) (V2 z) ∧ fst z ∈ (V1 z) ∧ snd z ∈ (V2 z) ∧ (V1 z) × (V2 z) ⊆ U"
by(rule bchoice)
then obtain V2 where hv12:"⋀z. z∈U ⟹ openin (topology_generated_by 𝒪) (V1 z) ∧ openin (topology_generated_by 𝒰) (V2 z) ∧ fst z ∈ (V1 z) ∧ snd z ∈ (V2 z) ∧ (V1 z) × (V2 z) ⊆ U"
by auto
hence 1:"U = (⋃z∈U. (V1 z) × (V2 z))"
by auto
have "openin (topology_generated_by {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒰}) (⋃z∈U. (V1 z) × (V2 z))"
proof(rule openin_Union)
show "⋀S. S ∈ (λz. V1 z × V2 z) ` U ⟹ openin (topology_generated_by {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒰}) S"
proof safe
fix x y
assume h:"(x,y) ∈ U"
then have "generate_topology_on 𝒪 (V1 (x,y))"
using hv12 by(auto simp: openin_topology_generated_by_iff)
thus "openin (topology_generated_by {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒰}) (V1 (x, y) × V2 (x, y))"
proof induction
case Empty
then show ?case by auto
next
case (Int a b)
thus ?case
by (auto simp: Sigma_Int_distrib1)
next
case (UN K)
then have "openin (topology_generated_by {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒰}) (⋃{ k × V2 (x, y) | k. k ∈ K})"
by auto
moreover have "(⋃ {k × V2 (x, y) |k. k ∈ K}) = (⋃ K × V2 (x, y))"
by blast
ultimately show ?case by simp
next
case ho:(Basis s)
have "generate_topology_on 𝒰 (V2 (x,y))"
using h hv12 by(auto simp: openin_topology_generated_by_iff)
thus ?case
proof induction
case Empty
then show ?case by auto
next
case (Int a b)
then show ?case
by (auto simp: Sigma_Int_distrib2)
next
case (UN K)
then have "openin (topology_generated_by {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒰}) (⋃ { s × k | k. k ∈K})"
by auto
moreover have "(⋃ { s × k | k. k ∈K}) = s × ⋃K"
by blast
ultimately show ?case by simp
next
case (Basis s')
then show ?case
using ho by(auto intro!: topology_generated_by_Basis)
qed
qed
qed
qed
thus "openin (topology_generated_by {U × V |U V. U ∈ 𝒪 ∧ V ∈ 𝒰}) U"
using 1 by auto
qed
lemma prod_topology_generated_by_open:
"prod_topology S S' = topology_generated_by {U × V | U V. openin S U ∧ openin S' V}"
using prod_topology_generated_by[of " {U |U. openin S U}" "{U |U. openin S' U}"] topology_generated_by_open[of S,symmetric] topology_generated_by_open[of S']
by auto
lemma product_topology_cong:
assumes "⋀i. i ∈ I ⟹ S i = K i"
shows "product_topology S I = product_topology K I"
proof -
have 1:"{Π⇩E i∈I. X i |X. (∀i. openin (S i) (X i)) ∧ finite {i. X i ≠ topspace (S i)}} ⊆ {Π⇩E i∈I. X i |X. (∀i. openin (K i) (X i)) ∧ finite {i. X i ≠ topspace (K i)}}" if "⋀i. i ∈ I ⟹ S i = K i" for S K :: "_ ⇒ 'b topology"
proof
fix x
assume hx:"x ∈ {Π⇩E i∈I. X i |X. (∀i. openin (S i) (X i)) ∧ finite {i. X i ≠ topspace (S i)}}"
then obtain X where hX:
"x = (Π⇩E i∈I. X i)" "⋀i. openin (S i) (X i)" "finite {i. X i ≠ topspace (S i)}"
by auto
define X' where "X' ≡ (λi. if i ∈ I then X i else topspace (K i))"
have "x = (Π⇩E i∈I. X' i)"
by(auto simp: hX(1) X'_def PiE_def Pi_def)
moreover have "finite {i. X' i ≠ topspace (K i)}"
using that by(auto intro!: finite_subset[OF _ hX(3)] simp: X'_def)
moreover have "openin (K i) (X' i)" for i
using hX(2)[of i] that[of i] by(auto simp: X'_def)
ultimately show "x ∈ {Π⇩E i∈I. X i |X. (∀i. openin (K i) (X i)) ∧ finite {i. X i ≠ topspace (K i)}}"
by(auto intro!: exI[where x="X'"])
qed
have "{Π⇩E i∈I. X i |X. (∀i. openin (S i) (X i)) ∧ finite {i. X i ≠ topspace (S i)}} = {Π⇩E i∈I. X i |X. (∀i. openin (K i) (X i)) ∧ finite {i. X i ≠ topspace (K i)}}"
using 1[of S K] 1[of K S] assms by auto
thus ?thesis
by(simp add: product_topology_def)
qed
lemma topology_generated_by_without_empty:
"topology_generated_by 𝒪 = topology_generated_by { U ∈ 𝒪. U ≠ {}}"
proof(rule topology_generated_by_eq)
fix U
show "U ∈ 𝒪 ⟹ openin (topology_generated_by { U ∈ 𝒪. U ≠ {}}) U"
by(cases "U = {}") (simp_all add: topology_generated_by_Basis)
qed (simp add: topology_generated_by_Basis)
lemma topology_from_bij:
assumes "bij_betw f A (topspace S)"
shows "homeomorphic_map (pullback_topology A f S) S f" "topspace (pullback_topology A f S) = A"
proof -
note h = bij_betw_imp_surj_on[OF assms] bij_betw_inv_into_left[OF assms] bij_betw_inv_into_right[OF assms]
then show [simp]:"topspace (pullback_topology A f S) = A"
by(auto simp: topspace_pullback_topology)
show "homeomorphic_map (pullback_topology A f S) S f"
by(auto simp: homeomorphic_map_maps homeomorphic_maps_def h continuous_map_pullback[OF continuous_map_id,simplified] inv_into_into intro!: exI[where x="inv_into A f"] continuous_map_pullback'[where f=f]) (metis (mono_tags, opaque_lifting) comp_apply continuous_map_eq continuous_map_id h(3) id_apply)
qed
lemma openin_pullback_topology':
assumes "bij_betw f A (topspace S)"
shows "openin (pullback_topology A f S) u ⟷ (openin S (f ` u)) ∧ u ⊆ A"
unfolding openin_pullback_topology
proof safe
fix U
assume h:"openin S U" "u = f -` U ∩ A"
from openin_subset[OF this(1)] assms
have [simp]:"f ` (f -` U ∩ A) = U"
by(auto simp: image_def vimage_def bij_betw_def)
show "openin S (f ` (f -` U ∩ A))"
by(simp add: h)
next
assume "openin S (f ` u)" "u ⊆ A"
with assms show "∃U. openin S U ∧ u = f -` U ∩ A"
by(auto intro!: exI[where x="f ` u"] simp: bij_betw_def inj_on_def)
qed
subsubsection ‹ Isolated Point ›
definition isolated_points_of :: "'a topology ⇒ 'a set ⇒ 'a set" (infixr "isolated'_points'_of" 80) where
"X isolated_points_of A ≡ {x∈topspace X ∩ A. x ∉ X derived_set_of A}"
lemma isolated_points_of_eq:
"X isolated_points_of A = {x∈topspace X ∩ A. ∃U. x ∈ U ∧ openin X U ∧ U ∩ (A - {x}) = {}}"
unfolding isolated_points_of_def by(auto simp: in_derived_set_of)
lemma in_isolated_points_of:
"x ∈ X isolated_points_of A ⟷ x ∈ topspace X ∧ x ∈ A ∧ (∃U. x ∈ U ∧ openin X U ∧ U ∩ (A - {x}) = {})"
by(simp add: isolated_points_of_eq)
lemma derived_set_of_eq:
"x ∈ X derived_set_of A ⟷ x ∈ X closure_of (A - {x})"
by(auto simp: in_derived_set_of in_closure_of)
subsubsection ‹ Perfect Set ›
definition perfect_set :: "'a topology ⇒ 'a set ⇒ bool" where
"perfect_set X A ⟷ closedin X A ∧ X isolated_points_of A = {}"
abbreviation "perfect_space X ≡ perfect_set X (topspace X)"
lemma perfect_setI:
assumes "closedin X A"
and "⋀x T. ⟦x ∈ A; x ∈ T; openin X T⟧ ⟹ ∃y≠x. y ∈ T ∧ y ∈ A"
shows "perfect_set X A"
using assms by(simp add: perfect_set_def isolated_points_of_def in_derived_set_of) blast
lemma perfect_spaceI:
assumes "⋀x T. ⟦x ∈ T; openin X T⟧ ⟹ ∃y≠x. y ∈ T"
shows "perfect_space X"
using assms by(auto intro!: perfect_setI) (meson in_mono openin_subset)
lemma perfect_setD:
assumes "perfect_set X A"
shows "closedin X A" "A ⊆ topspace X" "⋀x T. ⟦x ∈ A; x ∈ T; openin X T⟧ ⟹ ∃y≠x. y ∈ T ∧ y ∈ A"
using assms closedin_subset[of X A] by(simp_all add: perfect_set_def isolated_points_of_def in_derived_set_of) blast
lemma perfect_space_perfect:
"perfect_set euclidean (UNIV :: 'a :: perfect_space set)"
by(auto simp: perfect_set_def in_isolated_points_of) (metis Int_Diff inf_top.right_neutral insert_Diff not_open_singleton)
lemma perfect_set_subtopology:
assumes "perfect_set X A"
shows "perfect_space (subtopology X A)"
using perfect_setD[OF assms] by(auto intro!: perfect_setI simp: inf.absorb_iff2 openin_subtopology)
subsubsection ‹ Bases and Sub-Bases in Abstract Topology›
definition subbase_of :: "['a topology, 'a set set] ⇒ bool" where
"subbase_of S 𝒪 ⟷ S = topology_generated_by 𝒪"
definition base_of :: "['a topology, 'a set set] ⇒ bool" where
"base_of S 𝒪 ⟷ (∀U. openin S U ⟷ (∃𝒰. U = ⋃𝒰 ∧ 𝒰 ⊆ 𝒪))"
definition second_countable :: "'a topology ⇒ bool" where
"second_countable S ⟷ (∃𝒪. countable 𝒪 ∧ base_of S 𝒪)"
definition zero_dimensional :: "'a topology ⇒ bool" where
"zero_dimensional S ⟷ (∃𝒪. base_of S 𝒪 ∧ (∀u∈𝒪. openin S u ∧ closedin S u))"
lemma openin_base:
assumes "base_of S 𝒪 " "U = ⋃𝒰" and "𝒰 ⊆ 𝒪"
shows "openin S U"
using assms by(auto simp: base_of_def)
lemma base_is_subbase:
assumes "base_of S 𝒪"
shows "subbase_of S 𝒪"
unfolding subbase_of_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_of_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_of_subset:
assumes "subbase_of S 𝒪" and "U ∈ 𝒪"
shows "U ⊆ topspace S"
using assms(1)[simplified subbase_of_def] topology_generated_by_topspace assms
by auto
lemma subbase_of_openin:
assumes "subbase_of S 𝒪" and "U ∈ 𝒪"
shows "openin S U"
using assms by(simp add: subbase_of_def openin_topology_generated_by_iff generate_topology_on.Basis)
lemma base_of_subset:
assumes "base_of S 𝒪" and "U ∈ 𝒪"
shows "U ⊆ topspace S"
using subbase_of_subset[OF base_is_subbase[OF assms(1)] assms(2)] .
lemma base_of_openin:
assumes "base_of S 𝒪" and "U ∈ 𝒪"
shows "openin S U"
using subbase_of_openin[OF base_is_subbase[OF assms(1)] assms(2)] .
lemma base_of_def2:
assumes "⋀U. U ∈ 𝒪 ⟹ openin S U"
shows "base_of S 𝒪 ⟷ (∀U. openin S U ⟶ (∀x∈U. ∃W∈𝒪. x ∈ W ∧ W ⊆ U))"
proof
assume h:"base_of S 𝒪"
show "∀U. openin S U ⟶ (∀x∈U. ∃W∈𝒪. x ∈ W ∧ W ⊆ U)"
proof safe
fix U x
assume h':"openin S U" "x ∈ U"
then obtain 𝒰 where hu: "U = ⋃𝒰" "𝒰 ⊆ 𝒪"
using h by(auto simp: base_of_def)
then obtain W where "x ∈ W" "W ∈ 𝒰"
using h'(2) by blast
thus "∃W∈𝒪. x ∈ W ∧ W ⊆ U"
using hu by(auto intro!: bexI[where x=W])
qed
next
assume h:"∀U. openin S U ⟶ (∀x∈U. ∃W∈𝒪. x ∈ W ∧ W ⊆ U)"
show "base_of S 𝒪"
unfolding base_of_def
proof safe
fix U
assume "openin S U"
then have "∀x∈U. ∃W. W∈𝒪 ∧ x ∈ W ∧ W ⊆ U"
using h by blast
hence "∃W. ∀x∈U. W x ∈ 𝒪 ∧ x ∈ W x ∧ W x ⊆ U"
by(rule bchoice)
then obtain W where hw:
"∀x∈U. W x ∈ 𝒪 ∧ x ∈ W x ∧ W x ⊆ U" by auto
thus "∃𝒰. U = ⋃ 𝒰 ∧ 𝒰 ⊆ 𝒪"
by(auto intro!: exI[where x="W ` U"])
next
fix U 𝒰
show "𝒰 ⊆ 𝒪 ⟹ openin S (⋃ 𝒰)"
using assms by auto
qed
qed
lemma base_of_def2':
"base_of S 𝒪 ⟷ (∀b∈𝒪. openin S b) ∧ (∀x. openin S x ⟶ (∃B'⊆𝒪. ⋃ B' = x))"
proof
assume h:"base_of 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_of_def)
qed
next
assume h:"(∀b∈𝒪. openin S b) ∧ (∀x. openin S x ⟶ (∃B'⊆𝒪. ⋃ B' = x))"
show "base_of S 𝒪"
unfolding base_of_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_of_in_subset:
assumes "base_of S 𝒪" "openin S u" "x ∈ u"
shows "∃v∈𝒪. x ∈ v ∧ v ⊆ u"
using assms base_of_def2 base_of_def2' by fastforce
lemma base_of_without_empty:
assumes "base_of S 𝒪"
shows "base_of S {U ∈ 𝒪. U ≠ {}}"
unfolding base_of_def2'
proof safe
fix x
assume "x ∈ 𝒪" " ¬ openin S x"
thus "⋀y. y ∈ {}"
using base_of_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_of_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_of S 𝒪 ∧ (∀U∈𝒪. U ≠ {})"
proof -
obtain 𝒪 where "countable 𝒪" "base_of S 𝒪"
using assms second_countable_def by blast
thus ?thesis
by(auto intro!: exI[where x="{U ∈ 𝒪. U ≠ {}}"] base_of_without_empty)
qed
lemma subtopology_subbase_of:
assumes "subbase_of S 𝒪"
shows "subbase_of (subtopology S T) {T ∩ U | U. U ∈ 𝒪}"
using assms subtopology_generated_by
by(auto simp: subbase_of_def)
lemma subtopology_base_of:
assumes "base_of S 𝒪"
shows "base_of (subtopology S T) {T ∩ U | U. U ∈ 𝒪}"
unfolding base_of_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_of_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_of_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_of S 𝒪"
using assms second_countable_def by blast
thus ?thesis
by(auto intro!: exI[where x="{T ∩ U | U. U ∈ 𝒪}"] simp: second_countable_def Setcompr_eq_image dest: subtopology_base_of)
qed
lemma Lindelof_of:
assumes "second_countable S" "⋀u. u ∈ U ⟹ openin S u" "⋃ U = topspace S"
shows "∃U'. countable U' ∧ U' ⊆ U ∧ ⋃ U' = topspace S"
proof -
from assms(1) obtain 𝒪 where h: "countable 𝒪" "base_of S 𝒪"
by(auto simp: second_countable_def)
define B' where "B' ≡ {v∈𝒪. ∃u∈U. v ⊆ u}"
have B': "countable B'"
using h(1) by(auto simp: B'_def)
have "∀v. v ∈ B' ⟶ (∃u∈U. v ⊆ u)" by(auto simp: B'_def)
then obtain U' where U':"⋀v. v ∈ B' ⟹ U' v ∈ U" "⋀v. v ∈ B' ⟹ v ⊆ U' v"
by metis
show ?thesis
proof(rule exI[where x="U' ` B'"])
show "countable (U' ` B') ∧ U' ` B' ⊆ U ∧ ⋃ (U' ` B') = topspace S"
proof safe
fix x
assume "x ∈ topspace S"
then obtain u where u:"x ∈ u" "u ∈ U"
using assms(3) by auto
obtain v where v:"x ∈ v" "v ∈ 𝒪" "v ⊆ u"
using base_of_in_subset[OF h(2) assms(2)[OF u(2)] u(1)] by auto
show "x ∈ ⋃ (U' ` B')"
using u v U' by(auto intro!: bexI[where x=v]) (auto simp: B'_def intro!: exI[where x=u])
qed(use B' U' assms(2) openin_subset in blast)+
qed
qed
lemma open_map_with_base:
assumes "base_of 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_of_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.›
definition finite_intersections :: "'a set set ⇒ 'a set set" where
"finite_intersections 𝒪 ≡ { ⋂𝒪' | 𝒪'. 𝒪' ≠ {} ∧ finite 𝒪' ∧ 𝒪' ⊆ 𝒪}"
lemma finite_intersections_inI:
assumes "U = ⋂𝒪'" "𝒪' ≠ {}" " finite 𝒪'" and "𝒪' ⊆ 𝒪"
shows "U ∈ finite_intersections 𝒪"
using assms by(auto simp: finite_intersections_def)
lemma finite_intersections_Uin:
assumes "U ∈ 𝒪"
shows "U ∈ finite_intersections 𝒪"
using assms by(auto intro!: finite_intersections_inI[of U "{U}"])
lemma finite_intersections_int:
assumes "U ∈ finite_intersections 𝒪" and "V ∈ finite_intersections 𝒪"
shows "U ∩ V ∈ finite_intersections 𝒪"
proof -
obtain 𝒪U 𝒪V where
"U = ⋂𝒪U" "𝒪U ≠ {}" "finite 𝒪U" "𝒪U ⊆ 𝒪" "V = ⋂𝒪V" "finite 𝒪V" "𝒪V ⊆ 𝒪"
using assms by(auto simp: finite_intersections_def)
thus ?thesis
by(auto intro!: finite_intersections_inI[of _ "𝒪U ∪ 𝒪V"])
qed
lemma finite_intersections_countable:
assumes "countable 𝒪"
shows "countable (finite_intersections 𝒪)"
proof -
have "finite_intersections 𝒪 = (⋃i∈{𝒪'. 𝒪' ≠ {} ∧ finite 𝒪' ∧ 𝒪' ⊆ 𝒪}. {⋂ i})"
by(auto simp: finite_intersections_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_intersections_openin:
assumes "U ∈ finite_intersections 𝒪"
shows "openin (topology_generated_by 𝒪) U"
proof -
obtain 𝒪U where hu:
"U = ⋂𝒪U" "𝒪U ≠ {}" "finite 𝒪U" "𝒪U ⊆ 𝒪"
using assms by(auto simp: finite_intersections_def)
show ?thesis
using hu by(auto intro: topology_generated_by_Basis)
qed
lemma topology_generated_by_finite_intersections:
"topology_generated_by 𝒪 = topology_generated_by (finite_intersections 𝒪)"
proof(rule topology_generated_by_eq)
fix U
assume "U ∈ 𝒪"
then show "openin (topology_generated_by (finite_intersections 𝒪)) U"
by(auto intro!: topology_generated_by_Basis simp: finite_intersections_Uin)
qed (rule finite_intersections_openin)
lemma topology_generated_by_is_union_of_finite_intersections:
"openin (topology_generated_by 𝒪) U ⟷ (∃𝒰. U = ⋃𝒰 ∧ 𝒰 ⊆ finite_intersections 𝒪)"
proof
assume "openin (topology_generated_by 𝒪) U"
then have "generate_topology_on 𝒪 U"
by (simp add: openin_topology_generated_by_iff)
thus "∃𝒰. U = ⋃ 𝒰 ∧ 𝒰 ⊆ finite_intersections 𝒪"
proof induction
case Empty
then show ?case
by auto
next
case (Int a b)
then obtain 𝒰a 𝒰b where hab:
"a = ⋃ 𝒰a" "𝒰a ⊆ finite_intersections 𝒪" "b = ⋃ 𝒰b" "𝒰b ⊆ finite_intersections 𝒪"
by auto
then have "a ∩ b = ⋃{ Ua ∩ Ub | Ua Ub. Ua ∈ 𝒰a ∧ Ub ∈ 𝒰b}"
by blast
moreover have "{ Ua ∩ Ub | Ua Ub. Ua ∈ 𝒰a ∧ Ub ∈ 𝒰b} ⊆ finite_intersections 𝒪"
using hab(2,4) finite_intersections_int by blast
ultimately show ?case by auto
next
case (UN K)
then have "∃𝒰. ∀k∈K. k = ⋃ (𝒰 k) ∧ 𝒰 k ⊆ finite_intersections 𝒪"
by(auto intro!: bchoice)
then obtain 𝒰 where
"∀k∈K. k = ⋃ (𝒰 k) ∧ 𝒰 k ⊆ finite_intersections 𝒪" by auto
thus ?case
by(auto intro!: exI[where x="⋃k∈K. (𝒰 k)"]) (metis UnionE)
next
case (Basis s)
then show ?case
by(auto intro!: exI[where x="{s}"] finite_intersections_Uin)
qed
next
assume "∃𝒰. U = ⋃ 𝒰 ∧ 𝒰 ⊆ finite_intersections 𝒪"
then obtain 𝒰 where
"U = ⋃ 𝒰" "𝒰 ⊆ finite_intersections 𝒪" by auto
thus "openin (topology_generated_by 𝒪) U"
using finite_intersections_openin
by(auto simp: openin_topology_generated_by_iff intro!: generate_topology_on.UN)
qed
lemma base_from_subbase:
assumes "subbase_of S 𝒪"
shows "base_of S (finite_intersections 𝒪)"
using topology_generated_by_is_union_of_finite_intersections[of 𝒪,simplified assms[simplified subbase_of_def,symmetric]]
by(simp add: base_of_def)
lemma countable_base_from_countable_subbase:
assumes "countable 𝒪" and "subbase_of S 𝒪"
shows "second_countable S"
using finite_intersections_countable[OF assms(1)] base_from_subbase[OF assms(2)]
by(auto simp: second_countable_def)
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_of S 𝒪" "countable 𝒪'" "base_of S' 𝒪'"
using assms by(auto simp: second_countable_def)
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_of (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_of_def prod_topology_generated_by)
qed
qed
text ‹ Abstract version of the theorem @{thm product_topology_countable_basis}.›
lemma product_topology_countable_base_of:
assumes "countable I" and "⋀i. i ∈ I ⟹ second_countable (S i)"
shows "∃𝒪'. countable 𝒪' ∧ base_of (product_topology S I) 𝒪' ∧
(∀k ∈ 𝒪'. ∃X. k = (Π⇩E i∈I. X i) ∧ (∀i. openin (S i) (X i)) ∧ finite {i. X i ≠ topspace (S i)} ∧ {i. X i ≠ topspace (S i)} ⊆ I)"
proof -
obtain 𝒪 where ho:
"⋀i. i ∈ I ⟹ countable (𝒪 i)" "⋀i. i ∈ I ⟹ base_of (S i) (𝒪 i)"
using assms(2)[simplified second_countable_def] by metis
show ?thesis
unfolding second_countable_def
proof(intro exI[where x="{Π⇩E i∈I. U i | U. finite {i∈I. U i ≠ topspace (S i)} ∧ (∀i∈{i∈I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i)}"] conjI)
show "countable {Π⇩E i∈I. U i | U. finite {i∈I. U i ≠ topspace (S i)} ∧ (∀i∈{i∈I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i)}"
(is "countable ?X")
proof -
have "?X = {Π⇩E i∈I. U i | U. finite {i∈I. U i ≠ topspace (S i)} ∧ (∀i∈{i∈I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i) ∧ (∀i ∈(UNIV- I). U i = {undefined})}"
(is "_ = ?Y")
proof (rule set_eqI)
show "⋀x. x ∈ ?X ⟷ x ∈ ?Y"
proof
fix x
assume "x ∈ ?X"
then obtain U where hu:
"x = (Π⇩E i∈I. U i)" "finite {i∈I. U i ≠ topspace (S i)}" "(∀i∈{i∈I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i)"
by auto
define U' where "U' i ≡ (if i ∈ I then U i else {undefined})" for i
have "x = (Π⇩E i∈I. U' i)"
using hu(1) by(auto simp: U'_def PiE_def extensional_def Pi_def)
moreover have "finite {i∈I. U' i ≠ topspace (S i)}" "(∀i∈{i∈I. U' i ≠ topspace (S i)}. U' i ∈ 𝒪 i)" "∀i ∈(UNIV- I). U' i = {undefined}"
using hu(2,3) by(auto simp: U'_def) (metis (mono_tags, lifting) Collect_cong)
ultimately show "x ∈ ?Y" by auto
qed auto
qed
also have "... = (λU. Π⇩E i∈I. U i) ` {U. finite {i∈I. U i ≠ topspace (S i)} ∧ (∀i∈{i∈I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i) ∧ (∀i ∈(UNIV- I). U i = {undefined})}" by auto
also have "countable ..."
proof(rule countable_image)
have "{U. finite {i ∈ I. U i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i) ∧ (∀i∈UNIV - I. U i = {undefined})} = {U. ∃I'. finite I' ∧ I' ⊆ I ∧ (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈(I - I'). U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})}"
(is "?A = ?B")
proof (rule set_eqI)
show "⋀x. x ∈ ?A ⟷ x ∈ ?B"
proof
fix U
assume "U ∈ {U. finite {i ∈ I. U i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i) ∧ (∀i∈UNIV - I. U i = {undefined})}"
then show "U ∈ {U. ∃I'. finite I' ∧ I' ⊆ I ∧ (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈I - I'. U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})}"
by auto
next
fix U
assume assm:"U ∈ {U. ∃I'. finite I' ∧ I' ⊆ I ∧ (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈I - I'. U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})}"
then obtain I' where hi':
"finite I'" "I' ⊆ I" "∀i∈I'. U i ∈ 𝒪 i" "∀i∈I - I'. U i = topspace (S i)" "∀i∈UNIV - I. U i = {undefined}"
by auto
then have "⋀i. i ∈ I ⟹ U i ≠ topspace (S i) ⟹ i ∈ I'" by auto
hence "{i ∈ I. U i ≠ topspace (S i)} ⊆ I'" by auto
hence "finite {i ∈ I. U i ≠ topspace (S i)}"
using hi'(1) by (simp add: rev_finite_subset)
thus "U ∈ {U. finite {i ∈ I. U i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i) ∧ (∀i∈UNIV - I. U i = {undefined})}"
using hi' by auto
qed
qed
also have "... = (⋃I'∈{I'. finite I' ∧ I' ⊆ I}. {U. (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈I - I'. U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})})"
by auto
also have "countable ..."
proof(rule countable_UN[OF countable_Collect_finite_subset[OF assms(1)]])
fix I'
assume "I' ∈ {I'. finite I' ∧ I' ⊆ I}"
hence hi':"finite I'" "I' ⊆ I" by auto
have "(λU i. if i ∈ I' then U i else undefined) ` {U. (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈I - I'. U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})} ⊆ (Π⇩E i∈I'. 𝒪 i)"
by auto
moreover have "countable ..."
using hi' by(auto intro!: countable_PiE ho)
ultimately have "countable ((λU i. if i ∈ I' then U i else undefined) ` {U. (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈I - I'. U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})})"
by(simp add: countable_subset)
moreover have "inj_on (λU i. if i ∈ I' then U i else undefined) {U. (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈I - I'. U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})}"
(is "inj_on ?f ?X")
proof
fix x y
assume hxy: "x ∈ ?X" "y ∈ ?X" "?f x = ?f y"
show "x = y"
proof
fix i
consider "i ∈ I'" | "i ∈ I - I'" | "i ∈ UNIV - I"
using hi'(2) by blast
then show "x i = y i"
proof cases
case i:1
then show ?thesis
using fun_cong[OF hxy(3),of i] by auto
next
case i:2
then show ?thesis
using hxy(1,2) by auto
next
case i:3
then show ?thesis
using hxy(1,2) by auto
qed
qed
qed
ultimately show "countable {U. (∀i∈I'. U i ∈ 𝒪 i) ∧ (∀i∈I - I'. U i = topspace (S i)) ∧ (∀i∈UNIV - I. U i = {undefined})}"
using countable_image_inj_on by auto
qed
finally show "countable {U. finite {i ∈ I. U i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i) ∧ (∀i∈UNIV - I. U i = {undefined})}" .
qed
finally show ?thesis .
qed
next
show "base_of (product_topology S I) {Π⇩E i∈I. U i |U. finite {i ∈ I. U i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i)}"
(is "base_of (product_topology S I) ?X")
unfolding base_of_def
proof safe
fix U
assume "openin (product_topology S I) U"
then have "∀x∈U. ∃Ux. finite {i ∈ I. Ux i ≠ topspace (S i)} ∧ (∀i∈I. openin (S i) (Ux i)) ∧ x ∈ Pi⇩E I Ux ∧ Pi⇩E I Ux ⊆ U"
by(simp add: openin_product_topology_alt)
hence "∃Ux. ∀x∈U. finite {i ∈ I. Ux x i ≠ topspace (S i)} ∧ (∀i∈I. openin (S i) (Ux x i)) ∧ x ∈ Pi⇩E I (Ux x) ∧ Pi⇩E I (Ux x) ⊆ U"
by(rule bchoice)
then obtain Ux where hui:
"⋀x. x ∈ U ⟹ finite {i ∈ I. Ux x i ≠ topspace (S i)}" "⋀x i. x ∈ U ⟹ i ∈ I ⟹ openin (S i) (Ux x i)" "⋀x. x ∈ U ⟹ x ∈ Pi⇩E I (Ux x)" "⋀x. x ∈ U ⟹ Pi⇩E I (Ux x) ⊆ U"
by fastforce
then have 1:"∀x∈U. ∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. ∃𝒰xj. 𝒰xj ⊆ 𝒪 i ∧ Ux x i = ⋃ 𝒰xj"
using ho[simplified base_of_def] by (metis (no_types, lifting) mem_Collect_eq)
have "∀x∈U. ∃𝒰xj. ∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. 𝒰xj i ⊆ 𝒪 i ∧ Ux x i = ⋃ (𝒰xj i)"
by(standard, rule bchoice) (use 1 in simp)
hence "∃𝒰xj. ∀x∈U. ∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. 𝒰xj x i ⊆ 𝒪 i ∧ Ux x i = ⋃ (𝒰xj x i)"
by(rule bchoice)
then obtain 𝒰xj where
"∀x∈U. ∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. 𝒰xj x i ⊆ 𝒪 i ∧ Ux x i = ⋃ (𝒰xj x i)"
by auto
hence huxj: "⋀x i. x ∈ U ⟹ i ∈ {i ∈ I. Ux x i ≠ topspace (S i)} ⟹ 𝒰xj x i ⊆ 𝒪 i"
"⋀x i. x ∈ U ⟹ i ∈ {i ∈ I. Ux x i ≠ topspace (S i)} ⟹ Ux x i = ⋃ (𝒰xj x i)"
by blast+
show "∃𝒰. U = ⋃ 𝒰 ∧ 𝒰 ⊆ ?X"
proof(intro exI[where x="{Π⇩E i∈I. K i | K. ∃x∈U. finite {i ∈ I. Ux x i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. K i ∈ 𝒰xj x i) ∧ (∀i∈UNIV -{i ∈ I. Ux x i ≠ topspace (S i)}. K i = topspace (S i))}"] conjI)
show "U = ⋃ {Π⇩E i∈I. K i | K. ∃x∈U. finite {i ∈ I. Ux x i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. K i ∈ 𝒰xj x i) ∧ (∀i∈UNIV -{i ∈ I. Ux x i ≠ topspace (S i)}. K i = topspace (S i))}"
proof safe
fix x
assume hxu:"x ∈ U"
have "∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. Ux x i = ⋃ (𝒰xj x i)"
using huxj[OF hxu] by blast
hence "∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. ∃Uxj. Uxj ∈ 𝒰xj x i ∧ x i ∈ Uxj"
using hui(3)[OF hxu] by auto
hence "∃Uxj. ∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. Uxj i ∈ 𝒰xj x i ∧ x i ∈ Uxj i"
by(rule bchoice)
then obtain Uxj where huxj':
"⋀i. i ∈ {i ∈ I. Ux x i ≠ topspace (S i)} ⟹ Uxj i ∈ 𝒰xj x i"
"⋀i. i ∈ {i ∈ I. Ux x i ≠ topspace (S i)} ⟹ x i ∈ Uxj i"
by auto
define K where "K ≡ (λi. if i ∈ {i ∈ I. Ux x i ≠ topspace (S i)} then Uxj i else topspace (S i))"
have "x ∈ (Π⇩E i∈I. K i)"
using huxj'(2) hui(3,4)[OF hxu] openin_subset[OF hui(2)[OF hxu]]
by(auto simp: K_def PiE_def Pi_def)
moreover have "∃x∈U. finite {i ∈ I. Ux x i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. K i ∈ 𝒰xj x i) ∧ (∀i∈UNIV -{i ∈ I. Ux x i ≠ topspace (S i)}. K i = topspace (S i))"
by(rule bexI[OF _ hxu], rule conjI,simp add: hui(1)[OF hxu]) (use hui(2) hxu openin_subset huxj'(1) K_def in auto)
ultimately show "x ∈ ⋃ {Π⇩E i∈I. K i | K. ∃x∈U. finite {i ∈ I. Ux x i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. K i ∈ 𝒰xj x i) ∧ (∀i∈UNIV -{i ∈ I. Ux x i ≠ topspace (S i)}. K i = topspace (S i))}"
by auto
next
fix x X K u
assume hu: "x ∈ (Π⇩E i∈I. K i)" "u ∈ U" "finite {i ∈ I. Ux u i ≠ topspace (S i)}" "∀i∈{i ∈ I. Ux u i ≠ topspace (S i)}. K i ∈ 𝒰xj u i" "∀i∈UNIV -{i ∈ I. Ux u i ≠ topspace (S i)}. K i = topspace (S i)"
have "⋀i. i ∈ {i ∈ I. Ux u i ≠ topspace (S i)} ⟹ K i ⊆ Ux u i"
using huxj[OF hu(2)] hu(4) by blast
moreover have "⋀i. i ∈ I - {i ∈ I. Ux u i ≠ topspace (S i)} ⟹ K i = Ux u i"
using hu(5) by auto
ultimately have "⋀i. i ∈ I ⟹ K i ⊆ Ux u i"
by blast
thus "x ∈ U"
using hui(4)[OF hu(2)] hu(1) by blast
qed
next
show "{Π⇩E i∈I. K i | K. ∃x∈U. finite {i ∈ I. Ux x i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. K i ∈ 𝒰xj x i) ∧ (∀i∈UNIV -{i ∈ I. Ux x i ≠ topspace (S i)}. K i = topspace (S i))} ⊆ ?X"
proof
fix x
assume "x ∈ {Π⇩E i∈I. K i | K. ∃x∈U. finite {i ∈ I. Ux x i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. Ux x i ≠ topspace (S i)}. K i ∈ 𝒰xj x i) ∧ (∀i∈UNIV -{i ∈ I. Ux x i ≠ topspace (S i)}. K i = topspace (S i))}"
then obtain u K where hu:
"x = (Π⇩E i∈I. K i)" "u ∈ U" "finite {i ∈ I. Ux u i ≠ topspace (S i)}" "∀i∈{i ∈ I. Ux u i ≠ topspace (S i)}. K i ∈ 𝒰xj u i" "∀i∈UNIV -{i ∈ I. Ux u i ≠ topspace (S i)}. K i = topspace (S i)"
by auto
have hksubst:"{i ∈ I. K i ≠ topspace (S i)} ⊆ {i ∈ I. Ux u i ≠ topspace (S i)}"
using hu(5) by fastforce
hence "finite {i ∈ I. K i ≠ topspace (S i)}"
using hu(3) by (simp add: finite_subset)
moreover have "∀i∈{i ∈ I. K i ≠ topspace (S i)}. K i ∈ 𝒪 i"
using huxj(1)[OF hu(2)] hu(4) hksubst
by (meson subsetD)
ultimately show "x ∈ ?X"
using hu(1) by auto
qed
qed
next
fix 𝒰
assume "𝒰 ⊆ ?X"
have "openin (product_topology S I) u" if hu:"u ∈ 𝒰" for u
proof -
have hu': "u ∈ ?X"
using ‹𝒰 ⊆ ?X› hu by auto
then obtain U where hU:
"u = (Π⇩E i∈I. U i)" "finite {i ∈ I. U i ≠ topspace (S i)}" "∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i"
by auto
define U' where "U' ≡ (λi. if i ∈ {i ∈ I. U i ≠ topspace (S i)} then U i else topspace (S i))"
have hU': "u = (Π⇩E i∈I. U' i)"
by(auto simp: hU(1) U'_def PiE_def Pi_def)
have hUfinite : "finite {i. U' i ≠ topspace (S i)}"
using hU(2) by(auto simp: U'_def)
have hUoi: "∀i∈{i. U' i ≠ topspace (S i)}. U' i ∈ 𝒪 i"
using hU(3) by(auto simp: U'_def)
have hUi: "∀i∈{i. U' i ≠ topspace (S i)}. i ∈ I"
using hU(2) by(auto simp: U'_def)
have hallopen:"openin (S i) (U' i)" for i
proof -
consider "i ∈ {i. U' i ≠ topspace (S i)}" | "i ∉ {i. U' i ≠ topspace (S i)}" by auto
then show ?thesis
proof cases
case 1
then show ?thesis
using hUoi ho(2)[of i] base_of_openin[of "S i" "𝒪 i" "U' i"] hUi
by auto
next
case 2
then have "U' i = topspace (S i)" by auto
thus ?thesis by auto
qed
qed
show "openin (product_topology S I) u"
using hallopen hUfinite by(auto intro!: product_topology_basis simp: hU')
qed
thus "openin (product_topology S I) (⋃ 𝒰)"
by auto
qed
next
show "∀k∈{Pi⇩E I U |U. finite {i ∈ I. U i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i)}. ∃X. k = Pi⇩E I X ∧ (∀i. openin (S i) (X i)) ∧ finite {i. X i ≠ topspace (S i)} ∧ {i. X i ≠ topspace (S i)} ⊆ I"
proof
fix k
assume "k ∈ {Pi⇩E I U |U. finite {i ∈ I. U i ≠ topspace (S i)} ∧ (∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i)}"
then obtain U where hu:
"k = (Π⇩E i∈I. U i)" "finite {i ∈ I. U i ≠ topspace (S i)}" "∀i∈{i ∈ I. U i ≠ topspace (S i)}. U i ∈ 𝒪 i"
by auto
define X where "X ≡ (λi. if i ∈ {i ∈ I. U i ≠ topspace (S i)} then U i else topspace (S i))"
have hX1: "k = (Π⇩E i∈I. X i)"
using hu(1) by(auto simp: X_def PiE_def Pi_def)
have hX2: "openin (S i) (X i)" for i
using hu(3) base_of_openin[of "S i" _ "U i",OF ho(2)]
by(auto simp: X_def)
have hX3: "finite {i. X i ≠ topspace (S i)}"
using hu(2) by(auto simp: X_def)
have hX4: "{i. X i ≠ topspace (S i)} ⊆ I"
by(auto simp: X_def)
show "∃X. k = (Π⇩E i∈I. X i) ∧ (∀i. openin (S i) (X i)) ∧ finite {i. X i ≠ topspace (S i)} ∧ {i. X i ≠ topspace (S i)} ⊆ I"
using hX1 hX2 hX3 hX4 by(auto intro!: exI[where x=X])
qed
qed
qed
lemma product_topology_second_countable:
assumes "countable I" and "⋀i. i ∈ I ⟹ second_countable (S i)"
shows "second_countable (product_topology S I)"
using product_topology_countable_base_of[OF assms(1)] assms(2)
by(fastforce simp: second_countable_def)
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_of X 𝒪"
using assms by(auto simp: second_countable_def)
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_of_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_of_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_of_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_of_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 ‹ Dense and Separable in Abstract Topology›
definition dense_of :: "['a topology, 'a set] ⇒ bool" where
"dense_of S U ⟷ (U ⊆ topspace S ∧ (∀V. openin S V ⟶ V ≠ {} ⟶ U ∩ V ≠ {}))"
lemma dense_of_def2:
"dense_of S U ⟷ (U ⊆ topspace S ∧ (S closure_of U) = topspace S)"
using dense_intersects_open by(auto simp: dense_of_def closure_of_subset_topspace in_closure_of) auto
lemma dense_of_subset:
assumes "dense_of S U"
shows "U ⊆ topspace S"
using assms by(simp add: dense_of_def)
lemma dense_of_nonempty:
assumes "topspace S ≠ {}" "dense_of S U"
shows "U ≠ {}"
using assms by(auto simp: dense_of_def)
definition separable :: "'a topology ⇒ bool" where
"separable S ⟷ (∃U. countable U ∧ dense_of S U)"
lemma dense_ofI:
assumes "U ⊆ topspace S"
and "⋀V. openin S V ⟹ V ≠ {} ⟹ U ∩ V ≠ {}"
shows "dense_of S U"
using assms by(auto simp: dense_of_def)
lemma separable_if_second_countable:
assumes "second_countable S"
shows "separable S"
proof -
obtain 𝒪 where ho:
"countable 𝒪" "base_of S 𝒪" "⋀u. u ∈ 𝒪 ⟹ u ≠ {}"
using second_countable_ex_without_empty[OF assms] by auto
then obtain x where hx: "⋀u. u ∈ 𝒪 ⟹ x u ∈ u"
by (metis all_not_in_conv)
show ?thesis
unfolding separable_def
proof(intro exI[where x="{x u|u. u ∈ 𝒪}"] conjI)
show "countable {x u |u. u ∈ 𝒪}"
using ho(1) by (simp add: Setcompr_eq_image)
next
show "dense_of S {x u |u. u ∈ 𝒪}"
proof(rule dense_ofI)
show "{x u |u. u ∈ 𝒪} ⊆ topspace S"
using hx base_of_subset[OF ho(2)] by auto
next
fix V
assume "openin S V" "V ≠ {}"
then obtain B where hb:"B ⊆ 𝒪" "V = ⋃ B"
using base_of_def2' ho(2) by metis
with ‹V ≠ {}› obtain b where "b ∈ B"
by auto
hence "{x u |u. u ∈ 𝒪} ∩ b ⊆ {x u |u. u ∈ 𝒪} ∩ V"
using hb(2) by auto
moreover have "x b ∈ {x u |u. u ∈ 𝒪} ∩ b"
using hb(1) ‹b ∈ B› hx[of b] by auto
ultimately show "{x u |u. u ∈ 𝒪} ∩ V ≠ {}"
by auto
qed
qed
qed
lemma dense_of_prod:
assumes "dense_of S U" and "dense_of S' U'"
shows "dense_of (prod_topology S S') (U × U')"
proof(rule dense_ofI)
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_of_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_of_def)
qed
lemma separable_prod:
assumes "separable S" and "separable S'"
shows "separable (prod_topology S S')"
proof -
obtain U U' where
"countable U" "dense_of S U" "countable U'" "dense_of S' U'"
using assms by(auto simp: separable_def)
thus ?thesis
by(auto intro!: exI[where x="U×U'"] dense_of_prod simp: separable_def)
qed
lemma dense_of_product:
assumes "⋀i. i ∈ I ⟹ dense_of (T i) (U i)"
shows "dense_of (product_topology T I) (Π⇩E i∈I. U i)"
proof(rule dense_ofI)
fix V
assume h:"openin (product_topology T I) V" "V ≠ {}"
then obtain x where hx:"x ∈ V" by auto
then obtain K where hk:
"finite {i ∈ I. K i ≠ topspace (T i)}" "∀i∈I. openin (T i) (K i)" "x ∈ (Π⇩E i∈I. K i)" "(Π⇩E i∈I. K i) ⊆ V"
using h(1) openin_product_topology_alt[of T I V] by auto
hence "⋀i. i ∈ I ⟹ K i ≠ {}" by auto
hence "⋀i. i ∈ I ⟹ U i ∩ K i ≠ {}"
using assms hk by(auto simp: dense_of_def)
hence "(Π⇩E i∈I. U i) ∩ (Π⇩E i∈I. K i) ≠ {}"
by (simp add: PiE_Int PiE_eq_empty_iff)
thus "(Π⇩E i∈I. U i) ∩ V ≠ {}"
using hk by auto
next
show "(Π⇩E i∈I. U i) ⊆ topspace (product_topology T I)"
using assms by(auto simp: dense_of_def)
qed
lemma separable_countable_product:
assumes "countable I" and "⋀i. i ∈ I ⟹ separable (T i)"
shows "separable (product_topology T I)"
proof -
consider "∃i∈I. topspace (T i) = {}" | "⋀i. i ∈ I ⟹ topspace (T i) ≠ {}"
by auto
thus ?thesis
proof cases
case 1
then obtain i where i:"i ∈ I" "topspace (T i) = {}"
by auto
show ?thesis
unfolding separable_def dense_of_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 "topspace (product_topology T I) = {}"
by auto
with h(1) have "V = {}"
using openin_subset by blast
thus "x ∈ {}"
using h(2) by auto
qed
qed auto
next
case 2
then have "∃x. ∀i∈I. x i ∈ topspace (T i)"
by (meson all_not_in_conv)
moreover from "2"
have "∃U. ∀i∈I. countable (U i) ∧ dense_of (T i) (U i)"
using assms(2) by(auto intro!: bchoice simp: separable_def)
ultimately
obtain x U where hxu:
"⋀i. i ∈ I ⟹ x i ∈ topspace (T i)" "⋀i. i ∈ I ⟹ countable (U i)" "⋀i. i ∈ I ⟹ dense_of (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_def
proof(intro exI[where x="⋃{ Π⇩E i∈I. U' J i | J. finite J ∧ J ⊆ I}"] conjI)
have "(⋃{ Π⇩E i∈I. U' J i | J. finite J ∧ J ⊆ I}) = (⋃ ((λJ. Π⇩E i∈I. U' J i) ` {J. finite J ∧ J ⊆ I}))"
by auto
also have "countable ..."
proof(rule countable_UN)
fix J
assume hj:"J ∈ {J. finite J ∧ J ⊆ I}"
have "inj_on (λf. (λi∈J. f i, λi∈(I-J). f i)) (Π⇩E i∈I. U' J i)"
proof(rule inj_onI)
fix f g
assume h:"f ∈ Pi⇩E I (U' J)" "g ∈ Pi⇩E I (U' J)"
"(restrict f J, restrict f (I - J)) = (restrict g J, restrict g (I - J))"
then have "⋀i. i ∈ J ⟹ f i = g i" "⋀i. i ∈(I-J) ⟹ f i = g i"
by(auto simp: restrict_def) meson+
thus "f = g"
using h(1,2) by(auto simp: U'_def) (meson PiE_ext)
qed
moreover have "countable ((λf. (λi∈J. f i, λi∈(I-J). f i)) ` (Π⇩E i∈I. U' J i))" (is "countable ?K")
proof -
have 1:"?K ⊆ (Π⇩E i∈J. U i) × (Π⇩E i∈(I-J). {x i})"
using hj by(auto simp: U'_def PiE_def Pi_def)
have 2:"countable ..."
proof(rule countable_SIGMA)
show "countable (Pi⇩E J U)"
using hj hxu(2) by(auto intro!: countable_PiE)
next
have "(Π⇩E i∈I - J. {x i}) = { λi∈I-J. x i }"
by(auto simp: PiE_def extensional_def restrict_def Pi_def)
thus "countable (Π⇩E i∈I - J. {x i})"
by simp
qed
show ?thesis
by(rule countable_subset[OF 1 2])
qed
ultimately show "countable (Π⇩E i∈I. U' J i)"
by(simp add: countable_image_inj_eq)
qed(rule countable_Collect_finite_subset[OF assms(1)])
finally show "countable (⋃{ Π⇩E i∈I. U' J i | J. finite J ∧ J ⊆ I})" .
next
show "dense_of (product_topology T I) (⋃ {Π⇩E i∈I. U' J i |J. finite J ∧ J ⊆ I})"
proof(rule dense_ofI)
fix V
assume h:"openin (product_topology T I) V" "V ≠ {}"
then obtain y where hx:"y ∈ V" by auto
then obtain K where hk:
"finite {i ∈ I. K i ≠ topspace (T i)}" "⋀i. i∈I ⟹ openin (T i) (K i)" "y ∈ (Π⇩E i∈I. K i)" "(Π⇩E i∈I. K i) ⊆ V"
using h(1) openin_product_topology_alt[of T I V] by auto
hence 3:"⋀i. i ∈ I ⟹ K i ≠ {}" by auto
hence 4:"i ∈ {i ∈ I. K i ≠ topspace (T i)} ⟹ K i ∩ U' {i ∈ I. K i ≠ topspace (T i)} i ≠ {}" for i
using hxu(3)[of i] hk(2)[of i] by(auto simp: U'_def dense_of_def)
have "∃z. ∀i∈{i ∈ I. K i ≠ topspace (T i)}. z i ∈ K i ∩ U' {i ∈ I. K i ≠ topspace (T i)} i"
by(rule bchoice) (use 4 in auto)
then obtain z where hz: "∀i∈{i ∈ I. K i ≠ topspace (T i)}. z i ∈ K i ∩ U' {i ∈ I. K i ≠ topspace (T i)} i"
by auto
have 5: "i ∉ {i ∈ I. K i ≠ topspace (T i)} ⟹ i ∈ I ⟹ x i ∈ K i" for i
using hxu(1)[of i] by auto
have "(λi. if i ∈ {i ∈ I. K i ≠ topspace (T i)} then z i else if i ∈ I then x i else undefined) ∈ (Π⇩E i∈I. U' {i ∈ I. K i ≠ topspace (T i)} i) ∩ (Π⇩E i∈I. K i)"
using 4 5 hz by(auto simp: U'_def)
thus "⋃ {Pi⇩E I (U' J) |J. finite J ∧ J ⊆ I} ∩ V ≠ {}"
using hk(1,4) by blast
next
have "⋀J. J ⊆ I ⟹ (Π⇩E i∈I. U' J i) ⊆ topspace (product_topology T I)"
using hxu by(auto simp: dense_of_def U'_def PiE_def Pi_def) (metis subsetD)
thus "(⋃ {Π⇩E i∈I. U' J i |J. finite J ∧ J ⊆ I}) ⊆ topspace (product_topology T I)"
by auto
qed
qed
qed
qed
lemma separable_finite_product:
assumes "finite I" and "⋀i. i ∈ I ⟹ separable (T i)"
shows "separable (product_topology T I)"
using separable_countable_product[OF countable_finite[OF assms(1)]] assms by auto
lemma homeomorphic_separable:
assumes "separable X" "X homeomorphic_space Y"
shows "separable Y"
proof -
obtain f g where "homeomorphic_maps X Y f g"
using assms(2) by(auto simp: homeomorphic_space_def)
hence fg:"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)
obtain U where U: "countable U" "dense_of X U"
using assms(1) by(auto simp: separable_def)
show ?thesis
unfolding separable_def dense_of_def countable_image[OF U(1)]
proof(intro exI[where x="f ` U"] conjI)
show "f ` U ⊆ topspace Y"
using U(2) fg(1) by(auto simp: dense_of_def continuous_map_def)
next
show "∀V. openin Y V ⟶ V ≠ {} ⟶ f ` U ∩ V ≠ {}"
proof safe
fix V x
assume h:"openin Y V" "f ` U ∩ V = {}" "x ∈ V"
then have "U ∩ (f -` V ∩ topspace X) = {}"
by blast
moreover have "f -` V ∩ topspace X ≠ {}"
using continuous_map_preimage_topspace fg(2) fg(4) h(1) h(3) openin_subset by fastforce
moreover have "openin X (f -` V ∩ topspace X)"
using h(1) fg(1) by auto
ultimately show "x ∈ {}"
using U(2) by(auto simp: dense_of_def)
qed
qed(rule countable_image[OF U(1)])
qed
subsubsection ‹ $G_{\delta}$ Set in Abstract Topology›
definition g_delta_of :: "['a topology, 'a set] ⇒ bool" where
"g_delta_of S A ⟷ (∃𝒰. 𝒰 ≠ {} ∧ countable 𝒰 ∧ (∀b∈𝒰. openin S b) ∧ A = ⋂ 𝒰)"
lemma g_delta_ofI:
assumes "U ≠ {}" "countable U" "⋀b. b ∈ U ⟹ openin S b" "A = ⋂ U"
shows "g_delta_of S A"
using assms by(auto simp: g_delta_of_def)
lemma g_delta_ofD:
assumes "g_delta_of S A"
shows "∃𝒰. 𝒰 ≠ {} ∧ countable 𝒰 ∧ (∀b∈𝒰. openin S b) ∧ A = ⋂ 𝒰"
using assms by(simp add: g_delta_of_def)
lemma g_delta_ofD':
assumes "g_delta_of 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 g_delta_ofD[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 g_delta_of_subset:
assumes "g_delta_of S A"
shows "A ⊆ topspace S"
using assms openin_subset by(auto simp: g_delta_of_def)
lemma g_delta_of_open_set[simp]:
assumes "openin S A"
shows "g_delta_of S A"
using assms by(auto simp: g_delta_of_def intro!: exI[where x="{A}"])
lemma g_delta_of_empty[simp]: "g_delta_of S {}"
by simp
lemma g_delta_of_topspace[simp]: "g_delta_of S (topspace S)"
by simp
lemma g_delta_of_inter:
assumes "g_delta_of S A" and "g_delta_of S B"
shows "g_delta_of S (A ∩ B)"
proof -
obtain Ua Ub where hu:
"Ua ≠ {}" "countable Ua" "⋀b. b ∈ Ua ⟹ openin S b" "A = ⋂ Ua"
"countable Ub" "⋀b. b ∈ Ub ⟹ openin S b" "B = ⋂ Ub"
using assms by(auto simp: g_delta_of_def)
thus ?thesis
by(auto intro!: g_delta_ofI[where U="Ua ∪ Ub"])
qed
lemma g_delta_of_Int:
assumes "⋀a. a ∈ 𝒰 ⟹ g_delta_of X a" "countable 𝒰" "𝒰 ≠ {}"
shows "g_delta_of X (⋂ 𝒰)"
proof -
obtain Ua where u:
"⋀a. a ∈ 𝒰 ⟹ Ua a ≠ {}" "⋀a. a ∈ 𝒰 ⟹ countable (Ua a)" "⋀a b. a ∈ 𝒰 ⟹ b ∈ Ua a ⟹ openin X b" "⋀a. a ∈ 𝒰 ⟹ a = ⋂ (Ua a)"
using g_delta_ofD[OF assms(1)] by metis
have 1: "⋃ {Ua a |a. a ∈ 𝒰} ≠ {}"
using assms(3) u(1) by auto
have 2: "countable (⋃ {Ua a |a. a ∈ 𝒰})"
by (simp add: Setcompr_eq_image assms(2) u(2))
have 3: "⋀b. b ∈ ⋃ {Ua a |a. a ∈ 𝒰} ⟹ openin X b"
using u(3) by auto
show ?thesis
using u(4) by(fastforce intro!: g_delta_ofI[OF 1 2 3])
qed
lemma g_delta_of_continuous_map:
assumes "continuous_map X Y f" "g_delta_of Y a"
shows "g_delta_of X (f -` a ∩ topspace X)"
proof -
obtain Ua where u:
"Ua ≠ {}" "countable Ua" "⋀b. b ∈ Ua ⟹ openin Y b" "a = ⋂ Ua"
using g_delta_ofD[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
using g_delta_ofI[OF 1 2 3] by(simp add: 0)
qed
lemma g_delta_of_inj_open_map:
assumes "open_map X Y f" "inj_on f (topspace X)" "g_delta_of X a"
shows "g_delta_of Y (f ` a)"
proof -
obtain Ua where u:
"Ua ≠ {}" "countable Ua" "⋀b. b ∈ Ua ⟹ openin X b" "a = ⋂ Ua"
using g_delta_ofD[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
using g_delta_ofI[OF 1 2 3] by(simp add: 0)
qed
lemma g_delta_of_homeo_morphic:
assumes "g_delta_of X a" "homeomorphic_map X Y f"
shows "g_delta_of Y (f ` a)"
by(auto intro!: g_delta_of_inj_open_map[of X Y f] simp: assms(1) homeomorphic_imp_injective_map[OF assms(2)] homeomorphic_imp_open_map[OF assms(2)])
lemma g_delta_of_prod:
assumes "g_delta_of X A" "g_delta_of Y B"
shows "g_delta_of (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"
using assms by(auto simp: g_delta_of_def)
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
using g_delta_ofI[OF 1 2 3] by(simp add: 0)
qed
lemma g_delta_of_prod1:
assumes "g_delta_of X A"
shows "g_delta_of (prod_topology X Y) (A × topspace Y)"
by(auto intro!: g_delta_of_prod assms)
lemma g_delta_of_prod2:
assumes "g_delta_of Y B"
shows "g_delta_of (prod_topology X Y) (topspace X × B)"
by(auto intro!: g_delta_of_prod assms)
lemma g_delta_of_subtopology:
assumes "g_delta_of X A" "A ⊆ S"
shows "g_delta_of (subtopology X S) A"
proof -
obtain Ua where u:
"Ua ≠ {}" "countable Ua" "⋀b. b ∈ Ua ⟹ openin X b" "A = ⋂ Ua"
using g_delta_ofD[OF assms(1)] by metis
have 0: "⋂ Ua = ⋂ {ua ∩ S | ua. ua ∈ Ua } "
using assms(2) u(4) by auto
have 1: "{ua ∩ S | ua. ua ∈ Ua } ≠ {}"
using u(1) by auto
have 2: "countable {ua ∩ S | ua. ua ∈ Ua }"
using u(2) by (simp add: Setcompr_eq_image)
have 3: "⋀b. b ∈ {ua ∩ S | ua. ua ∈ Ua } ⟹ openin (subtopology X S) b"
using u(3) by(auto simp: openin_subtopology)
show ?thesis
using g_delta_ofI[OF 1 2 3 0] by(simp add: u(4))
qed
lemma g_delta_of_subtopology_inverse:
assumes "g_delta_of (subtopology X S) A" "g_delta_of X S"
shows "g_delta_of X A"
proof -
obtain Ua where ua:
"Ua ≠ {}" "countable Ua" "⋀b. b ∈ Ua ⟹ openin (subtopology X S) b" "A = ⋂ Ua"
using g_delta_ofD[OF assms(1)] by metis
then obtain T where t: "⋀b. b ∈ Ua ⟹ openin X (T b)" "⋀b. b ∈ Ua ⟹ b = T b ∩ S"
by(auto simp: openin_subtopology) metis
have 0: "A = ⋂ {T b|b. b ∈ Ua} ∩ S"
using ua(1,4) t(2) by blast
have "{T b |b. b ∈ Ua} ≠ {}" "countable {T b |b. b ∈ Ua}"
using ua(1,2) by(simp_all add: Setcompr_eq_image)
from g_delta_ofI[OF this] t(1) show ?thesis
by(auto intro!: g_delta_of_inter[OF _ assms(2)] simp: 0)
qed
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 ‹ Upper-Semicontinuous ›
definition upper_semicontinuous_map :: "['a topology, 'a ⇒ 'b :: linorder_topology] ⇒ bool" where
"upper_semicontinuous_map X f ⟷ (∀a. openin X {x∈topspace X. f x < a})"
lemma continuous_upper_semicontinuous:
assumes "continuous_map X (euclidean :: ('b :: linorder_topology) topology) f"
shows "upper_semicontinuous_map X f"
unfolding upper_semicontinuous_map_def
proof safe
fix a :: 'b
have *:"openin euclidean U ⟹ openin X {x ∈ topspace X. f x ∈ U}" for U
using assms by(simp add: continuous_map)
have "openin euclidean {..<a}" by auto
with *[of "{..<a}"] show "openin X {x ∈ topspace X. f x < a}" by auto
qed
lemma upper_semicontinuous_map_iff_closed:
"upper_semicontinuous_map X f ⟷ (∀a. closedin X {x∈topspace X. f x ≥ a})"
proof -
have "{x ∈ topspace X. f x < a} = topspace X - {x ∈ topspace X. f x ≥ a}" for a
by auto
thus ?thesis
by (simp add: closedin_def upper_semicontinuous_map_def)
qed
lemma upper_semicontinuous_map_real_iff:
fixes f :: "'a ⇒ real"
shows "upper_semicontinuous_map X f ⟷ upper_semicontinuous_map X (λx. ereal (f x))"
unfolding upper_semicontinuous_map_def
proof safe
fix a :: ereal
assume h:"∀a::real. openin X {x ∈ topspace X. f x < a}"
consider "a = - ∞" | "a = ∞" | "a ≠ - ∞ ∧ a ≠ ∞" by auto
then show "openin X {x ∈ topspace X. ereal (f x) < a}"
proof cases
case 3
then have "ereal (f x) < a ⟷ f x < real_of_ereal a" for x
by (metis ereal_less_eq(3) linorder_not_less real_of_ereal.elims)
thus ?thesis
using h by simp
qed simp_all
next
fix a :: real
assume h:"∀a::ereal. openin X {x ∈ topspace X. ereal (f x) < a}"
then have "openin X {x ∈ topspace X. ereal (f x) < ereal a}"
by blast
moreover have"ereal (f x) < real_of_ereal a ⟷ f x < a" for x
by auto
ultimately show "openin X {x ∈ topspace X. f x < a}" by auto
qed
subsection ‹ Lemmas for Limits›
lemma qlim_eq_lim_mono_at_bot:
fixes g :: "rat ⇒ 'a :: linorder_topology"
assumes "mono f" "(g ⤏ a) at_bot" "⋀r::rat. f (real_of_rat r) = g r"
shows "(f ⤏ a) at_bot"
proof -
have "mono g"
by(metis assms(1,3) mono_def of_rat_less_eq)
have ga:"⋀r. g r ≥ a"
proof(rule ccontr)
fix r
assume "¬ a ≤ g r"
then have "g r < a" by simp
from order_topology_class.order_tendstoD(1)[OF assms(2) this]
obtain Q :: rat where q: "⋀q. q ≤ Q ⟹ g r < g q"
by(auto simp: eventually_at_bot_linorder)
define q where "q ≡ min r Q"
show False
using q[of q] ‹mono g›
by(auto simp: q_def mono_def) (meson linorder_not_less min.cobounded1)
qed
show ?thesis
proof(rule decreasing_tendsto)
show "∀⇩F n in at_bot. a ≤ f n"
unfolding eventually_at_bot_linorder
by(rule exI[where x=undefined],auto) (metis Ratreal_def assms(1,3) dual_order.trans ga less_eq_real_def lt_ex monoD of_rat_dense)
next
fix x
assume "a < x"
with topological_space_class.topological_tendstoD[OF assms(2),of "{..<x}"]
obtain Q :: rat where q: "⋀q. q ≤ Q ⟹ g q < x"
by(auto simp: eventually_at_bot_linorder)
show "∀⇩F n in at_bot. f n < x"
using q assms(1,3) by(auto intro!: exI[where x="real_of_rat Q"] simp: eventually_at_bot_linorder) (metis dual_order.refl monoD order_le_less_trans)
qed
qed
lemma qlim_eq_lim_mono_at_top:
fixes g :: "rat ⇒ 'a :: linorder_topology"
assumes "mono f" "(g ⤏ a) at_top" "⋀r::rat. f (real_of_rat r) = g r"
shows "(f ⤏ a) at_top"
proof -
have "mono g"
by(metis assms(1,3) mono_def of_rat_less_eq)
have ga:"⋀r. g r ≤ a"
proof(rule ccontr)
fix r
assume "¬ g r ≤ a"
then have "a < g r" by simp
from order_topology_class.order_tendstoD(2)[OF assms(2) this]
obtain Q :: rat where q: "⋀q. Q ≤ q ⟹ g q < g r"
by(auto simp: eventually_at_top_linorder)
define q where "q ≡ max r Q"
show False
using q[of q] ‹mono g› by(auto simp: q_def mono_def leD)
qed
show ?thesis
proof(rule increasing_tendsto)
show "∀⇩F n in at_top. f n ≤ a"
unfolding eventually_at_top_linorder
by(rule exI[where x=undefined],auto) (metis (no_types, opaque_lifting) assms(1) assms(3) dual_order.trans ga gt_ex monoD of_rat_dense order_le_less)
next
fix x
assume "x < a"
with topological_space_class.topological_tendstoD[OF assms(2),of "{x<..}"]
obtain Q :: rat where q: "⋀q. Q ≤ q ⟹ x < g q"
by(auto simp: eventually_at_top_linorder)
show "∀⇩F n in at_top. x < f n"
using q assms(1,3) by(auto simp: eventually_at_top_linorder intro!: exI[where x="real_of_rat Q"]) (metis dual_order.refl monoD order_less_le_trans)
qed
qed
lemma tendsto_enn2real:
assumes "k < top" and "(f ⤏ k) F"
shows "((λn. enn2real (f n)) ⤏ enn2real k) F"
proof -
have 1:"ennreal (enn2real k) = k" "enn2real k ≥ 0"
using assms(1) by auto
show ?thesis
using assms tendsto_enn2real[OF _ 1(2),of f]
by(simp add: 1(1))
qed
lemma LIMSEQ_inverse_not0:
fixes xn :: "nat ⇒ real"
assumes "⋀n. xn n ≠ 0" "xn ⇢ x" "(λn. 1 / (xn n)) ⇢ b"
shows "x ≠ 0"
proof
assume x:"x = 0"
then have xn:"⋀e. e > 0 ⟹ ∃N. ∀n≥N. ¦xn n¦ < e"
using LIMSEQ_D[OF assms(2)] by simp
have "∃N. ∀n≥N. ¦1 / (xn n) - b¦ ≥ r" if r:"r > 0" for r
proof -
have "0 < 1 / (r + ¦b¦)"
using that by auto
with xn[OF this] obtain N where N':"⋀n. n ≥ N ⟹ ¦xn n¦ < 1 / (r + ¦b¦)"
by auto
show ?thesis
proof(rule exI[where x=N])
show "∀n≥N. r ≤ ¦1 / xn n - b¦"
proof safe
fix n
assume "n ≥ N"
note N'[OF this]
hence "(r + ¦b¦) * ¦xn n¦ < 1"
by (metis ‹0 < 1 / (r + ¦b¦)› mult.commute pos_less_divide_eq zero_less_divide_1_iff)
hence "1 / ¦xn n¦ > r + ¦b¦"
using assms(1)[of n] by (simp add: less_divide_eq)
hence "r + ¦b¦ - ¦b¦ < 1 / ¦xn n¦ - ¦b¦"
by simp
also have "... = ¦1 / xn n¦ - ¦b¦" by simp
also have "... ≤ ¦1 / xn n - b¦" by simp
finally show "r ≤ ¦1 / xn n - b¦"
by simp
qed
qed
qed
with LIMSEQ_D[OF assms(3)] show False
by (metis less_le_not_le linorder_le_cases real_norm_def zero_less_one)
qed
lemma obtain_subsequence:
fixes xn :: "nat ⇒ _"
assumes "infinite {n. P n (xn n)}"
obtains a :: "nat ⇒ nat" where "strict_mono a" "⋀n. P (a n) (xn (a n))"
proof -
have inf: "infinite {n. n > m ∧ P n (xn n)}" for m
proof
assume "finite {n. n > m ∧ P n (xn n)}"
then have "finite ({..m} ∪ {n. n > m ∧ P n (xn n)})" by auto
hence "finite {n. P n (xn n)}"
by(auto intro!: finite_subset[where B="{..m} ∪ {n. n > m ∧ P n (xn n)}"])
with assms show False by simp
qed
define an where "an ≡ rec_nat (SOME n. P n (xn n)) (λn an. SOME m. m > an ∧ P m (xn m))"
have anSome: "an (Suc n) = (SOME m. m > an n ∧ P m (xn m))" for n
by(auto simp: an_def)
have an1: "P (an n) (xn (an n))" for n
proof(cases n)
case 0
obtain m where m:"P m (xn m)"
using assms not_finite_existsD by blast
show ?thesis
by(simp add: an_def 0,rule someI,rule m)
next
case (Suc n')
obtain m where m:"m > an n'" "P m (xn m)"
using inf not_finite_existsD by blast
show ?thesis
by(simp add: Suc anSome, rule someI2[where a=m],auto simp: m)
qed
have an2: "strict_mono an"
unfolding strict_mono_Suc_iff anSome
proof safe
fix n
obtain m where m:"m > an n" "P m (xn m)"
using inf not_finite_existsD by blast
show "an n < (SOME m. an n < m ∧ P m (xn m))"
by (rule someI2[where a=m],auto simp: m)
qed
show ?thesis
using an1 that[OF an2] by auto
qed
subsection ‹Lemmas for Measure Theory›
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
lemma integral_measurable_subprob_algebra2:
fixes f :: "_ ⇒ _ ⇒ _::{banach,second_countable_topology}"
assumes [measurable]: "(λ(x, y). f x y) ∈ borel_measurable (M ⨂⇩M N)" "L ∈ measurable M (subprob_algebra N)"
shows "(λx. integral⇧L (L x) (f x)) ∈ borel_measurable M"
proof -
note integral_measurable_subprob_algebra[measurable]
note measurable_distr2[measurable]
have "(λx. integral⇧L (distr (L x) (M ⨂⇩M N) (λy. (x, y))) (λ(x, y). f x y)) ∈ borel_measurable M"
by measurable
then show "(λx. integral⇧L (L x) (f x)) ∈ borel_measurable M"
by (rule measurable_cong[THEN iffD1, rotated])
(simp add: integral_distr)
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
text ‹ Measurable isomorphisms.›
definition measurable_isomorphic_map::"['a measure, 'b measure, 'a ⇒ 'b] ⇒ bool" where
"measurable_isomorphic_map M N f ⟷ bij_betw f (space M) (space N) ∧ f ∈ M →⇩M N ∧ the_inv_into (space M) f ∈ N →⇩M M"
lemma measurable_isomorphic_map_sets_cong:
assumes "sets M = sets M'" "sets N = sets N'"
shows "measurable_isomorphic_map M N f ⟷ measurable_isomorphic_map M' N' f"
by(simp add: measurable_isomorphic_map_def sets_eq_imp_space_eq[OF assms(1)] sets_eq_imp_space_eq[OF assms(2)] measurable_cong_sets[OF assms] measurable_cong_sets[OF assms(2,1)])
lemma measurable_isomorphic_map_surj:
assumes "measurable_isomorphic_map M N f"
shows "f ` space M = space N"
using assms by(auto simp: measurable_isomorphic_map_def bij_betw_def)
lemma measurable_isomorphic_mapI:
assumes "bij_betw f (space M) (space N)" "f ∈ M →⇩M N" "the_inv_into (space M) f ∈ N →⇩M M"
shows "measurable_isomorphic_map M N f"
using assms by(simp add: measurable_isomorphic_map_def)
lemma measurable_isomorphic_map_byWitness:
assumes "f ∈ M →⇩M N" "g ∈ N →⇩M M" "⋀x. x ∈ space M ⟹ g (f x) = x" "⋀x. x ∈ space N ⟹ f (g x) = x"
shows "measurable_isomorphic_map M N f"
proof -
have *:"bij_betw f (space M) (space N)"
using assms by(auto intro!: bij_betw_byWitness[where f'=g] dest:measurable_space)
show ?thesis
proof(rule measurable_isomorphic_mapI)
have "the_inv_into (space M) f x = g x" if "x ∈ space N" for x
by (metis * assms(2) assms(4) bij_betw_imp_inj_on measurable_space that the_inv_into_f_f)
thus "the_inv_into (space M) f ∈ N →⇩M M"
using measurable_cong assms(2) by blast
qed (simp_all add: * assms(1))
qed
lemma measurable_isomorphic_map_restrict_space:
assumes "f ∈ M →⇩M N" "⋀A. A ∈ sets M ⟹ f ` A ∈ sets N" "inj_on f (space M)"
shows "measurable_isomorphic_map M (restrict_space N (f ` space M)) f"
proof(rule measurable_isomorphic_mapI)
show "bij_betw f (space M) (space (restrict_space N (f ` space M)))"
by (simp add: assms(2,3) inj_on_imp_bij_betw)
next
show "f ∈ M →⇩M restrict_space N (f ` space M)"
by (simp add: assms(1) measurable_restrict_space2)
next
show "the_inv_into (space M) f ∈ restrict_space N (f ` space M) →⇩M M"
proof(rule measurableI)
show "x ∈ space (restrict_space N (f ` space M)) ⟹ the_inv_into (space M) f x ∈ space M" for x
by (simp add: assms(2,3) the_inv_into_into)
next
fix A
assume "A ∈ sets M"
have "the_inv_into (space M) f -` A ∩ space (restrict_space N (f ` space M)) = f ` A"
by (simp add: ‹A ∈ sets M› assms(2,3) sets.sets_into_space the_inv_into_vimage)
also note assms(2)[OF ‹A ∈ sets M›]
finally show "the_inv_into (space M) f -` A ∩ space (restrict_space N (f ` space M)) ∈ sets (restrict_space N (f ` space M))"
by (simp add: assms(2) sets_restrict_space_iff)
qed
qed
lemma measurable_isomorphic_mapD':
assumes "measurable_isomorphic_map M N f"
shows "⋀A. A ∈ sets M ⟹ f ` A ∈ sets N" "f ∈ M →⇩M N"
"∃g. bij_betw g (space N) (space M) ∧ g ∈ N →⇩M M ∧ (∀x ∈ space M. g (f x) = x) ∧ (∀x∈ space N. f (g x) = x) ∧ (∀A∈sets N. g ` A ∈ sets M)"
proof -
have h:"bij_betw f (space M) (space N)" "f ∈ M →⇩M N" "the_inv_into (space M) f ∈ N →⇩M M"
using assms by(simp_all add: measurable_isomorphic_map_def)
show "f ` A ∈ sets N" if "A ∈ sets M" for A
proof -
have "f ` A = the_inv_into (space M) f -` A ∩ space N"
using the_inv_into_vimage[OF bij_betw_imp_inj_on[OF h(1)] sets.sets_into_space[OF that]]
by(simp add: bij_betw_imp_surj_on[OF h(1)])
also have "... ∈ sets N"
using that h(3) by auto
finally show ?thesis .
qed
show "f ∈ M →⇩M N"
using assms by(simp add: measurable_isomorphic_map_def)
show "∃g. bij_betw g (space N) (space M) ∧ g ∈ N →⇩M M ∧ (∀x ∈ space M. g (f x) = x) ∧ (∀x∈ space N. f (g x) = x) ∧ (∀A∈sets N. g ` A ∈ sets M)"
proof(rule exI[where x="the_inv_into (space M) f"])
have *:"the_inv_into (space M) f ` A ∈ sets M" if "A ∈ sets N" for A
proof -
have "⋀x. x ∈ space M ⟹ the_inv_into (space N) (the_inv_into (space M) f) x = f x"
by (metis bij_betw_imp_inj_on bij_betw_the_inv_into h(1) h(2) measurable_space the_inv_into_f_f)
from vimage_inter_cong[of "space M" _ f A,OF this] the_inv_into_vimage[OF bij_betw_imp_inj_on[OF bij_betw_the_inv_into[OF h(1)]] sets.sets_into_space[OF that]]
bij_betw_imp_surj_on[OF bij_betw_the_inv_into[OF h(1)]] measurable_sets[OF h(2) that]
show ?thesis
by fastforce
qed
show "bij_betw (the_inv_into (space M) f) (space N) (space M) ∧ the_inv_into (space M) f ∈ N →⇩M M ∧ (∀x∈space M. the_inv_into (space M) f (f x) = x) ∧ (∀x∈space N. f (the_inv_into (space M) f x) = x) ∧ (∀A∈sets N. the_inv_into (space M) f ` A ∈ sets M)"
using bij_betw_the_inv_into[OF h(1)]
by (meson * bij_betw_imp_inj_on f_the_inv_into_f_bij_betw h(1) h(3) the_inv_into_f_f)
qed
qed
lemma measurable_isomorphic_map_inv:
assumes "measurable_isomorphic_map M N f"
shows "measurable_isomorphic_map N M (the_inv_into (space M) f)"
using assms[simplified measurable_isomorphic_map_def]
by(auto intro!: measurable_isomorphic_map_byWitness[where g=f] bij_betw_the_inv_into f_the_inv_into_f_bij_betw[of f] bij_betw_imp_inj_on the_inv_into_f_f)
lemma measurable_isomorphic_map_comp:
assumes "measurable_isomorphic_map M N f" and "measurable_isomorphic_map N L g"
shows "measurable_isomorphic_map M L (g ∘ f)"
proof -
obtain f' g' where
[measurable]: "f' ∈ N →⇩M M" and hf:"⋀x. x∈space M ⟹ f' (f x) = x" "⋀x. x∈space N ⟹ f (f' x) = x"
and [measurable]: "g' ∈ L →⇩M N" and hg:"⋀x. x∈space N ⟹ g' (g x) = x" "⋀x. x∈space L ⟹ g (g' x) = x"
using measurable_isomorphic_mapD'[OF assms(1)] measurable_isomorphic_mapD'[OF assms(2)] by metis
have [measurable]: "f ∈ M →⇩M N" "g ∈ N →⇩M L"
using assms by(auto simp: measurable_isomorphic_map_def)
from hf hg measurable_space[OF ‹f ∈ M →⇩M N›] measurable_space[OF ‹g' ∈ L →⇩M N›] show ?thesis
by(auto intro!: measurable_isomorphic_map_byWitness[where g="f'∘g'"])
qed
definition measurable_isomorphic::"['a measure, 'b measure] ⇒ bool" (infixr "measurable'_isomorphic" 50) where
"M measurable_isomorphic N ⟷ (∃f. measurable_isomorphic_map M N f)"
lemma measurable_isomorphic_sets_cong:
assumes "sets M = sets M'" "sets N = sets N'"
shows "M measurable_isomorphic N ⟷ M' measurable_isomorphic N'"
using measurable_isomorphic_map_sets_cong[OF assms]
by(auto simp: measurable_isomorphic_def)
lemma measurable_isomorphicD:
assumes "M measurable_isomorphic N"
shows "∃f g. f ∈ M →⇩M N ∧ g ∈ N →⇩M M ∧ (∀x∈space M. g (f x) = x) ∧ (∀y∈space N. f (g y) = y) ∧ (∀A∈sets M. f ` A ∈ sets N) ∧ (∀A∈sets N. g ` A ∈ sets M)"
using assms measurable_isomorphic_mapD'[of M N]
by (metis (mono_tags, lifting) measurable_isomorphic_def)
lemma measurable_isomorphic_byWitness:
assumes "f ∈ M →⇩M N" "⋀x. x∈space M ⟹ g (f x) = x"
and "g ∈ N →⇩M M" "⋀y. y∈space N ⟹ f (g y) = y"
shows "M measurable_isomorphic N"
by(auto simp: measurable_isomorphic_def assms intro!: exI[where x = f] measurable_isomorphic_map_byWitness[where g=g])
lemma measurable_isomorphic_refl:
"M measurable_isomorphic M"
by(auto intro!: measurable_isomorphic_byWitness[where f=id and g=id])
lemma measurable_isomorphic_sym:
assumes "M measurable_isomorphic N"
shows "N measurable_isomorphic M"
using assms measurable_isomorphic_map_inv[of M N]
by(auto simp: measurable_isomorphic_def)
lemma measurable_isomorphic_trans:
assumes "M measurable_isomorphic N" and "N measurable_isomorphic L"
shows "M measurable_isomorphic L"
using assms measurable_isomorphic_map_comp[of M N _ L]
by(auto simp: measurable_isomorphic_def)
lemma measurable_isomorphic_empty:
assumes "space M = {}" "space N = {}"
shows "M measurable_isomorphic N"
using assms by(auto intro!: measurable_isomorphic_byWitness[where f=undefined and g=undefined] simp: measurable_empty_iff)
lemma measurable_isomorphic_empty1:
assumes "space M = {}" "M measurable_isomorphic N"
shows "space N = {}"
using measurable_isomorphicD[OF assms(2)] by(auto simp: measurable_empty_iff[OF assms(1)])
lemma measurable_ismorphic_empty2:
assumes "space N = {}" "M measurable_isomorphic N"
shows "space M = {}"
using measurable_isomorphic_sym[OF assms(2)] assms(1)
by(simp add: measurable_isomorphic_empty1)
lemma measurable_lift_product:
assumes "⋀i. i ∈ I ⟹ f i ∈ (M i) →⇩M (N i)"
shows "(λx i. if i ∈ I then f i (x i) else undefined) ∈ (Π⇩M i∈I. M i) →⇩M (Π⇩M i∈I. N i)"
using measurable_space[OF assms]
by(auto intro!: measurable_PiM_single' simp: assms measurable_PiM_component_rev space_PiM PiE_iff)
lemma measurable_isomorphic_map_lift_product:
assumes "⋀i. i ∈ I ⟹ measurable_isomorphic_map (M i) (N i) (h i)"
shows "measurable_isomorphic_map (Π⇩M i∈I. M i) (Π⇩M i∈I. N i) (λx i. if i ∈ I then h i (x i) else undefined)"
proof -
obtain h' where
"⋀i. i ∈ I ⟹ h' i ∈ (N i) →⇩M (M i)" "⋀i x. i ∈ I ⟹ x∈space (M i) ⟹ h' i (h i x) = x" "⋀i x. i ∈ I ⟹ x∈space (N i) ⟹ h i (h' i x) = x"
using measurable_isomorphic_mapD'(3)[OF assms] by metis
thus ?thesis
by(auto intro!: measurable_isomorphic_map_byWitness[OF measurable_lift_product[of I h M N,OF measurable_isomorphic_mapD'(2)[OF assms]] measurable_lift_product[of I h' N M,OF ‹⋀i. i ∈ I ⟹ h' i ∈ (N i) →⇩M (M i)›]]
simp: space_PiM PiE_iff extensional_def)
qed
lemma measurable_isomorphic_lift_product:
assumes "⋀i. i ∈ I ⟹ (M i) measurable_isomorphic (N i)"
shows "(Π⇩M i∈I. M i) measurable_isomorphic (Π⇩M i∈I. N i)"
proof -
obtain h where "⋀i. i ∈ I ⟹ measurable_isomorphic_map (M i) (N i) (h i)"
using assms by(auto simp: measurable_isomorphic_def) metis
thus ?thesis
by(auto intro!: measurable_isomorphic_map_lift_product exI[where x="λx i. if i ∈ I then h i (x i) else undefined"] simp: measurable_isomorphic_def)
qed
text ‹🌐‹https://math24.net/cantor-schroder-bernstein-theorem.html››
lemma Schroeder_Bernstein_measurable':
assumes "f ` (space M) ∈ sets N" "g ` (space N) ∈ sets M"
and "measurable_isomorphic_map M (restrict_space N (f ` (space M))) f" and "measurable_isomorphic_map N (restrict_space M (g ` (space N))) g"
shows "∃h. measurable_isomorphic_map M N h"
proof -
have hset:"⋀A. A ∈ sets M ⟹ f ` A ∈ sets (restrict_space N (f ` space M))"
"⋀A. A ∈ sets N ⟹ g ` A ∈ sets (restrict_space M (g ` space N))"
and hfg[measurable]:"f ∈ M →⇩M restrict_space N (f ` space M)"
"g ∈ N →⇩M restrict_space M (g ` space N)"
using measurable_isomorphic_mapD'(1,2)[OF assms(3)] measurable_isomorphic_mapD'(1,2)[OF assms(4)] assms(1,2)
by auto
have hset2:"⋀A. A ∈ sets M ⟹ f ` A ∈ sets N" "⋀A. A ∈ sets N ⟹ g ` A ∈ sets M"
and hfg2[measurable]: "f ∈ M →⇩M N" "g ∈ N →⇩M M"
using sets.Int_space_eq2[OF assms(1)] sets.Int_space_eq2[OF assms(2)] sets_restrict_space_iff[of "f ` space M" N] sets_restrict_space_iff[of "g ` space N" M] hset
measurable_restrict_space2_iff[of f M N] measurable_restrict_space2_iff[of g N M] hfg assms(1,2)
by auto
have bij1:"bij_betw f (space M) (f ` (space M))" "bij_betw g (space N) (g ` (space N))"
using assms(3,4) by(auto simp: measurable_isomorphic_map_def space_restrict_space sets.Int_space_eq2[OF assms(1)] sets.Int_space_eq2[OF assms(2)])
obtain f' g' where
hfg1'[measurable]: "f' ∈ restrict_space N (f ` (space M)) →⇩M M" "g' ∈ restrict_space M (g ` (space N)) →⇩M N"
and hfg':"⋀x. x∈space M ⟹ f' (f x) = x" "⋀x. x∈f ` space M ⟹ f (f' x) = x"
"⋀x. x∈space N ⟹ g' (g x) = x" "⋀x. x∈g ` space N ⟹ g (g' x) = x"
"bij_betw f' (f ` space M) (space M)" "bij_betw g' (g ` space N) (space N)"
using measurable_isomorphic_mapD'(3)[OF assms(3)] measurable_isomorphic_mapD'(3)[OF assms(4)] sets.Int_space_eq2[OF assms(1)] sets.Int_space_eq2[OF assms(2)]
by (metis space_restrict_space)
have hgfA:"(g ∘ f) ` A ∈ sets M" if "A ∈ sets M" for A
using hset2(2)[OF hset2(1)[OF that]] by(simp add: image_comp)
define An where "An ≡ (λn. ((g ∘ f)^^n) ` (space M - g ` (space N)))"
define A where "A ≡ (⋃n∈UNIV. An n)"
have "An n ∈ sets M" for n
proof(induction n)
case 0
thus ?case
using hset2[OF sets.top] by(simp add: An_def)
next
case ih:(Suc n)
have "An (Suc n) = (g ∘ f) ` (An n)"
by(auto simp add: An_def)
thus ?case
using hgfA[OF ih] by simp
qed
hence Asets:"A ∈ sets M"
by(simp add: A_def)
have Acompl:"space M - A ⊆ g ` space N"
proof -
have "space M - A ⊆ space M - An 0"
by(auto simp: A_def)
also have "... ⊆ g ` space N"
by(auto simp: An_def)
finally show ?thesis .
qed
define h where "h ≡ (λx. if x ∈ A ∪ (- space M) then f x else g' x)"
define h' where "h' ≡ (λx. if x ∈ f ` A then f' x else g x)"
have xinA_iff:"x ∈ A ⟷ h x ∈ f ` A" if "x ∈ space M" for x
proof
assume "h x ∈ f ` A"
show "x ∈ A"
proof(rule ccontr)
assume "x ∉ A"
then have "⋀n. x ∉ An n"
by(auto simp: A_def)
from this[of 0] have "x ∈ g ` (space N)"
using that by(auto simp: An_def)
have "g' x ∈ f ` A "
using ‹h x ∈ f ` A› ‹x ∉ A›
by (simp add: h_def that)
hence "g (g' x) ∈ (g ∘ f) ` A"
by auto
hence "x ∈ (g ∘ f) ` A"
using ‹x ∈ g ` (space N)› by (simp add: hfg'(4))
then obtain n where "x ∈ (g ∘ f) ` (An n)"
by(auto simp: A_def)
hence "x ∈ An (Suc n)"
by(auto simp: An_def)
thus False
using ‹⋀n. x ∉ An n› by simp
qed
qed(simp add: h_def)
show ?thesis
proof(intro exI[where x=h] measurable_isomorphic_map_byWitness[where g=h'])
have "{x ∈ space M. x ∈ A ∪ (- space M)} ∈ sets M"
using sets.Int_space_eq2[OF Asets] Asets by simp
moreover have "f ∈ restrict_space M {x. x ∈ A ∪ - space M} →⇩M N"
by (simp add: measurable_restrict_space1)
moreover have "g' ∈ restrict_space M {x. x ∉ A ∪ (- space M)} →⇩M N"
proof -
have "sets (restrict_space (restrict_space M (g ` space N)) {x. x ∉ A ∪ - space M}) = sets (restrict_space M (g ` space N ∩ {x. x ∉ A ∪ - space M}))"
by(simp add: sets_restrict_restrict_space)
also have "... = sets (restrict_space M (g ` space N ∩ {x. x ∈ space M - A}))"
by (metis Compl_iff DiffE DiffI Un_iff)
also have "... = sets (restrict_space M {x. x ∈ space M - A})"
by (metis Acompl le_inf_iff mem_Collect_eq subsetI subset_antisym)
also have "... = sets (restrict_space M {x. x ∉ A ∪ (- space M)})"
by (metis Compl_iff DiffE DiffI Un_iff)
finally have "sets (restrict_space (restrict_space M (g ` space N)) {x. x ∉ A ∪ - space M}) = sets (restrict_space M {x. x ∉ A ∪ - space M})" .
from measurable_cong_sets[OF this refl] measurable_restrict_space1[OF hfg1'(2),of " {x. x ∉ A ∪ - space M}"]
show ?thesis by auto
qed
ultimately show "h ∈ M →⇩M N"
by(simp add: h_def measurable_If_restrict_space_iff)
next
have "{x ∈ space N. x ∈ f ` A} ∈ sets N"
using sets.Int_space_eq2[OF hset2(1)[OF Asets]] hset2(1)[OF Asets] by simp
moreover have "f' ∈ restrict_space N {x. x ∈ f ` A} →⇩M M"
proof -
have "sets (restrict_space (restrict_space N (f ` space M)) {x. x ∈ f ` A}) = sets (restrict_space N (f ` space M ∩ {x. x ∈ f ` A}))"
by(simp add: sets_restrict_restrict_space)
also have "... = sets (restrict_space N {x. x ∈ f ` A})"
proof -
have "f ` space M ∩ {x. x ∈ f ` A} = {x. x ∈ f ` A}"
using sets.sets_into_space[OF Asets] by auto
thus ?thesis by simp
qed
finally have "sets (restrict_space (restrict_space N (f ` space M)) {x. x ∈ f ` A}) = sets (restrict_space N {x. x ∈ f ` A})" .
from measurable_cong_sets[OF this refl] measurable_restrict_space1[OF hfg1'(1),of "{x. x ∈ f ` A}"]
show ?thesis by auto
qed
moreover have "g ∈ restrict_space N {x. x ∉ f ` A} →⇩M M"
by (simp add: measurable_restrict_space1)
ultimately show "h' ∈ N →⇩M M"
by(simp add: h'_def measurable_If_restrict_space_iff)
next
fix x
assume "x ∈ space M"
then consider "x ∈ A" | "x ∈ space M - A" by auto
thus "h' (h x) = x"
proof cases
case xa:2
hence "h x ∉ f ` A"
using ‹x ∈ space M› xinA_iff by blast
thus ?thesis
using Acompl hfg'(4) xa by(auto simp add: h_def h'_def)
qed(simp add: h_def h'_def ‹x ∈ space M› hfg'(1))
next
fix x
assume "x ∈ space N"
then consider "x ∈ f ` A" | "x ∈ space N - f ` A" by auto
thus "h (h' x) = x"
proof cases
case hx:1
hence "x ∈ f ` (space M)"
using image_mono[OF sets.sets_into_space[OF Asets],of f] by auto
have "h' x = f' x"
using hx by(simp add: h'_def)
also have "... ∈ A"
using hx sets.sets_into_space[OF Asets] hfg'(1) by auto
finally show ?thesis
using hfg'(2)[OF ‹x ∈ f ` (space M)›] hx by(auto simp: h_def h'_def)
next
case hx:2
then have "h' x = g x"
by(simp add: h'_def)
also have "... ∉ A"
proof(rule ccontr)
assume "¬ g x ∉ A"
then have "g x ∈ A" by simp
then obtain n where hg:"g x ∈ An n" by(auto simp: A_def)
hence "0 < n" using hx by(auto simp: An_def)
then obtain n' where [simp]:"n = Suc n'"
using not0_implies_Suc by blast
then have "g x ∈ g ` f ` An n'"
using hg by(auto simp: An_def)
hence "x ∈ f ` An n'"
using inj_on_image_mem_iff[OF bij_betw_imp_inj_on[OF bij1(2)] ‹x ∈ space N›,of "f ` An n'"]
sets.sets_into_space[OF ‹An n' ∈ sets M›] measurable_space[OF hfg2(1)] by auto
also have "... ⊆ f ` A"
by(auto simp: A_def)
finally show False
using hx by simp
qed
finally show ?thesis
using hx hfg'(3)[OF ‹x ∈ space N›] measurable_space[OF hfg2(2) ‹x ∈ space N›]
by(auto simp: h_def h'_def)
qed
qed
qed
lemma Schroeder_Bernstein_measurable:
assumes "f ∈ M →⇩M N" "⋀A. A ∈ sets M ⟹ f ` A ∈ sets N" "inj_on f (space M)"
and "g ∈ N →⇩M M" "⋀A. A ∈ sets N ⟹ g ` A ∈ sets M" "inj_on g (space N)"
shows "∃h. measurable_isomorphic_map M N h"
using Schroeder_Bernstein_measurable'[OF assms(2)[OF sets.top] assms(5)[OF sets.top] measurable_isomorphic_map_restrict_space[OF assms(1-3)] measurable_isomorphic_map_restrict_space[OF assms(4-6)]]
by simp
lemma measurable_isomorphic_from_embeddings:
assumes "M measurable_isomorphic (restrict_space N B)" "N measurable_isomorphic (restrict_space M A)"
and "A ∈ sets M" "B ∈ sets N"
shows "M measurable_isomorphic N"
proof -
obtain f g where fg:"measurable_isomorphic_map M (restrict_space N B) f" "measurable_isomorphic_map N (restrict_space M A) g"
using assms(1,2) by(auto simp: measurable_isomorphic_def)
have [simp]:"f ` space M = B" "g ` space N = A"
using measurable_isomorphic_map_surj[OF fg(1)] measurable_isomorphic_map_surj[OF fg(2)] sets.sets_into_space[OF assms(3)] sets.sets_into_space[OF assms(4)]
by(auto simp: space_restrict_space)
obtain h where "measurable_isomorphic_map M N h"
using Schroeder_Bernstein_measurable'[of f M N g] assms(3,4) fg by auto
thus ?thesis
by(auto simp: measurable_isomorphic_def)
qed
lemma measurable_isomorphic_antisym:
assumes "B measurable_isomorphic (restrict_space C c)" "A measurable_isomorphic (restrict_space B b)"
and "c ∈ sets C" "b ∈ sets B" "C measurable_isomorphic A"
shows "C measurable_isomorphic B"
by(rule measurable_isomorphic_from_embeddings[OF measurable_isomorphic_trans[OF assms(5,2)] assms(1) assms(3,4)])
lemma countable_infinite_isomorphisc_to_nat_index:
assumes "countable I" and "infinite I"
shows "(Π⇩M x∈I. M) measurable_isomorphic (Π⇩M (x::nat)∈UNIV. M)"
proof(rule measurable_isomorphic_byWitness[where f="λx n. x (from_nat_into I n)" and g="λx. λi∈I. x (to_nat_on I i)"])
show "(λx n. x (from_nat_into I n)) ∈ (Π⇩M x∈I. M) →⇩M (Π⇩M (x::nat)∈UNIV. M)"
by(auto intro!: measurable_PiM_single' measurable_component_singleton[OF from_nat_into[OF infinite_imp_nonempty[OF assms(2)]]])
(simp add: PiE_iff infinite_imp_nonempty space_PiM from_nat_into[OF infinite_imp_nonempty[OF assms(2)]])
next
show "(λx. λi∈I. x (to_nat_on I i)) ∈ (Π⇩M (x::nat)∈UNIV. M) →⇩M (Π⇩M x∈I. M)"
by(auto intro!: measurable_PiM_single')
next
show "x ∈ space (Π⇩M x∈I. M) ⟹ (λi∈I. x (from_nat_into I (to_nat_on I i))) = x" for x
by (simp add: assms(1) restrict_ext space_PiM)
next
show "y ∈ space (Pi⇩M UNIV (λx. M)) ⟹ (λn. (λi∈I. y (to_nat_on I i)) (from_nat_into I n)) = y" for y
by (simp add: assms(1) assms(2) from_nat_into infinite_imp_nonempty)
qed
lemma PiM_PiM_isomorphic_to_PiM:
"(Π⇩M i∈I. Π⇩M j∈J. M i j) measurable_isomorphic (Π⇩M (i,j)∈I×J. M i j)"
proof(rule measurable_isomorphic_byWitness[where f="λx (i,j). if (i,j) ∈ I × J then x i j else undefined" and g="λx i j. if i ∉ I then undefined j else if j ∉ J then undefined else x (i,j)"])
have [simp]: "(λω. ω a b) ∈ (Π⇩M i∈I. Π⇩M j∈J. M i j) →⇩M M a b" if "a ∈ I" "b ∈ J" for a b
using measurable_component_singleton[OF that(1),of "λi. Π⇩M j∈J. M i j"] measurable_component_singleton[OF that(2),of "M a"]
by auto
show "(λx (i, j). if (i, j) ∈ I × J then x i j else undefined) ∈ (Π⇩M i∈I. Π⇩M j∈J. M i j) →⇩M (Π⇩M (i,j)∈I×J. M i j)"
apply(rule measurable_PiM_single')
apply auto[1]
apply(auto simp: PiE_def Pi_def space_PiM extensional_def;meson)
done
next
have [simp]: "(λω. ω (i, j)) ∈ Pi⇩M (I × J) (λ(i, j). M i j) →⇩M M i j" if "i ∈ I" "j ∈ J" for i j
using measurable_component_singleton[of "(i,j)" "I × J" "λ(i, j). M i j"] that by auto
show "(λx i j. if i ∉ I then undefined j else if j ∉ J then undefined else x (i, j)) ∈ (Π⇩M (i,j)∈I×J. M i j) →⇩M (Π⇩M i∈I. Π⇩M j∈J. M i j)"
by(auto intro!: measurable_PiM_single') (simp_all add: PiE_iff space_PiM extensional_def)
next
show "x ∈ space (Π⇩M i∈I. Π⇩M j∈J. M i j) ⟹ (λi j. if i ∉ I then undefined j else if j ∉ J then undefined else case (i, j) of (i, j) ⇒ if (i, j) ∈ I × J then x i j else undefined) = x" for x
by standard+ (auto simp: space_PiM PiE_def Pi_def extensional_def)
next
show "y ∈ space (Π⇩M (i,j)∈I×J. M i j) ⟹ (λ(i, j). if (i, j) ∈ I × J then if i ∉ I then undefined j else if j ∉ J then undefined else y (i, j) else undefined) = y" for y
by standard+ (auto simp: space_PiM PiE_def Pi_def extensional_def)
qed
lemma measurable_isomorphic_map_sigma_sets:
assumes "sets M = sigma_sets (space M) U" "measurable_isomorphic_map M N f"
shows "sets N = sigma_sets (space N) ((`) f ` U)"
proof -
from measurable_isomorphic_mapD'[OF assms(2)]
obtain g where h: "⋀A. A ∈ sets M ⟹ f ` A ∈ sets N" "f ∈ M →⇩M N" "bij_betw g (space N) (space M)" "g ∈ N →⇩M M" "⋀x. x∈space M ⟹ g (f x) = x" "⋀x. x∈space N ⟹ f (g x) = x" "⋀A. A∈sets N ⟹ g ` A ∈ sets M"
by metis
interpret s: sigma_algebra "space N" "sigma_sets (space N) ((`) f ` U)"
by(auto intro!: sigma_algebra_sigma_sets) (metis assms(1) h(2) measurable_space sets.sets_into_space sigma_sets_superset_generator subsetD)
show ?thesis
proof safe
fix x
assume "x ∈ sets N"
from h(7)[OF this] assms(1)
have "g ` x ∈ sigma_sets (space M) U" by simp
hence "f ` (g ` x) ∈ sigma_sets (space N) ((`) f ` U)"
proof induction
case h:(Compl a)
have "f ` (space M - a) = f ` (space M) - f ` a"
by(rule inj_on_image_set_diff[where C="space M"], insert assms h) (auto simp: measurable_isomorphic_map_def bij_betw_def sets.sets_into_space)
with h show ?case
by (metis assms(2) measurable_isomorphic_map_surj s.Diff s.top)
qed (auto simp: image_UN)
moreover have "f ` (g ` x) = x"
using sets.sets_into_space[OF ‹x ∈ sets N›] h(6) by(fastforce simp: image_def)
ultimately show "x ∈ sigma_sets (space N) ((`) f ` U)" by simp
next
interpret s': sigma_algebra "space M" "sigma_sets (space M) U"
by(simp add: assms(1)[symmetric] sets.sigma_algebra_axioms)
have 1:"⋀x. x ∈ U ⟹ x ⊆ space M"
by (simp add: s'.sets_into_space)
fix x
assume assm:"x ∈ sigma_sets (space N) ((`) f ` U)"
then show "x ∈ sets N"
by induction (auto simp: assms(1) h(1))
qed
qed
end