Theory Set_Based_Metric_Space
section ‹Set-Based Metric Spaces›
theory Set_Based_Metric_Space
imports Lemmas_StandardBorel
begin
subsection ‹Set-Based Metric Spaces ›
locale metric_set =
fixes S :: "'a set"
and dist :: "'a ⇒ 'a ⇒ real"
assumes dist_geq0: "⋀x y. dist x y ≥ 0"
and dist_notin: "⋀x y. x ∉ S ⟹ dist x y = 0"
and dist_0: "⋀x y. x ∈ S ⟹ y ∈ S ⟹ (x = y) = (dist x y = 0)"
and dist_sym: "⋀x y. dist x y = dist y x"
and dist_tr: "⋀x y z. x ∈ S ⟹ y ∈ S ⟹ z ∈ S ⟹ dist x z ≤ dist x y + dist y z"
lemma metric_class_metric_set[simp]: "metric_set UNIV dist"
by standard (auto simp: dist_commute dist_triangle)
context metric_set
begin
abbreviation "dist_typeclass ≡ Real_Vector_Spaces.dist"
lemma dist_notin':
assumes "y ∉ S"
shows "dist x y = 0"
by(auto simp: dist_sym[of x y] intro!: dist_notin assms)
lemma dist_ge0:
assumes "x ∈ S" "y ∈ S"
shows "x ≠ y ⟷ dist x y > 0"
using dist_0[OF assms] dist_geq0[of x y] by auto
lemma dist_0'[simp]: "dist x x = 0"
by(cases "x ∈ S") (use dist_notin dist_0 in auto)
lemma dist_tr_abs:
assumes "x ∈ S" "y ∈ S" "z ∈ S"
shows "¦dist x y - dist y z¦ ≤ dist x z"
using dist_tr[OF assms(1,3,2),simplified dist_sym[of z]] dist_tr[OF assms(2,1,3),simplified dist_sym[of _ x]]
by auto
text ‹ Ball ›
definition open_ball :: "'a ⇒ real ⇒ 'a set" where
"open_ball a r ≡ if a ∈ S then {x ∈ S. dist a x < r} else {}"
lemma open_ball_subset_ofS: "open_ball a ε ⊆ S"
by(auto simp: open_ball_def)
lemma open_ballD:
assumes "x ∈ open_ball a ε"
shows "dist a x < ε"
proof -
have [simp]:"a ∈ S"
apply(rule ccontr) using assms by(simp add: open_ball_def)
show ?thesis
using assms by(simp add: open_ball_def)
qed
lemma open_ballD':
assumes "x ∈ open_ball a ε"
shows "x ∈ S" "a ∈ S" "ε > 0"
proof -
have 1:"a ∈ S"
apply(rule ccontr)
using assms by(auto simp: open_ball_def)
have 2:"x ∈ S"
apply(rule ccontr)
using assms 1 by(auto simp: open_ball_def)
have 3: "dist a x < ε"
using assms by(simp add: 1 2 open_ball_def)
show "ε > 0"
apply(rule ccontr)
using 3 dist_geq0[of a x] by auto
show "x ∈ S" "a ∈ S"
by fact+
qed
lemma open_ball_inverse:
"x ∈ open_ball y ε ⟷ y ∈ open_ball x ε"
proof -
have 0:"⋀x y. x ∈ open_ball y ε ⟹ y ∈ open_ball x ε"
proof -
fix x y
assume 1:"x ∈ open_ball y ε"
show "y ∈ open_ball x ε"
using open_ballD'[OF 1] dist_sym[of y x] 1 by(simp add: open_ball_def)
qed
show ?thesis
using 0[of x y] 0[of y x] by auto
qed
lemma open_ball_ina[simp]:
assumes "a ∈ S" and "ε > 0"
shows "a ∈ open_ball a ε"
using assms dist_0[of a a] by(simp add: open_ball_def)
lemma open_ball_nin_le:
assumes "a ∈ S" "ε > 0" "b ∈ S" "b ∉ open_ball a ε"
shows "ε ≤ dist a b"
using assms by(simp add: open_ball_def)
lemma open_ball_le:
assumes "r ≤ l"
shows "open_ball a r ⊆ open_ball a l"
using assms by(auto simp: open_ball_def)
lemma open_ball_le_0:
assumes "ε ≤ 0"
shows "open_ball a ε = {}"
using assms dist_geq0[of a]
by(auto simp: open_ball_def) (meson linorder_not_less order_trans)
lemma open_ball_nin:
assumes "a ∉ S"
shows "open_ball a ε = {}"
by(simp add: open_ball_def assms)
definition closed_ball :: "'a ⇒ real ⇒ 'a set" where
"closed_ball a r ≡ if a ∈ S then {x ∈ S. dist a x ≤ r} else {}"
lemma closed_ball_subset_ofS:
"closed_ball a ε ⊆ S"
by(auto simp: closed_ball_def)
lemma closed_ballD:
assumes "x ∈ closed_ball a ε"
shows "dist a x ≤ ε"
proof -
have [simp]:"a ∈ S"
apply(rule ccontr) using assms by(simp add: closed_ball_def)
show ?thesis
using assms by(simp add: closed_ball_def)
qed
lemma closed_ballD':
assumes "x ∈ closed_ball a ε"
shows "x ∈ S" "a ∈ S" "ε ≥ 0"
proof -
have 1:"a ∈ S"
apply(rule ccontr)
using assms by(auto simp: closed_ball_def)
have 2:"x ∈ S"
apply(rule ccontr)
using assms 1 by(auto simp: closed_ball_def)
have 3: "dist a x ≤ ε"
using assms by(simp add: 1 2 closed_ball_def)
show "ε ≥ 0"
apply(rule ccontr)
using 3 dist_geq0[of a x] by auto
show "x ∈ S" "a ∈ S"
by fact+
qed
lemma closed_ball_ina[simp]:
assumes "a ∈ S" and "ε ≥ 0"
shows "a ∈ closed_ball a ε"
using assms dist_0[of a a] by(simp add: closed_ball_def)
lemma closed_ball_le:
assumes "r ≤ l"
shows "closed_ball a r ⊆ closed_ball a l"
using closed_ballD'[of _ a r] closed_ballD[of _ a r] assms
by(fastforce simp: closed_ball_def[of _ l])
lemma closed_ball_le_0:
assumes "ε < 0"
shows "closed_ball a ε = {}"
using assms dist_geq0[of a]
by(auto simp: closed_ball_def) (meson linorder_not_less order_trans)
lemma closed_ball_0:
assumes "a ∈ S"
shows "closed_ball a 0 = {a}"
using assms dist_0[OF assms assms] dist_0[OF assms] dist_geq0[of a] order_antisym_conv
by(auto simp: closed_ball_def)
lemma closed_ball_nin:
assumes "a ∉ S"
shows "closed_ball a ε = {}"
by(simp add: closed_ball_def assms)
lemma open_ball_closed_ball:
"open_ball a ε ⊆ closed_ball a ε"
using open_ballD'[of _ a ε] open_ballD[of _ a ε]
by(fastforce simp: closed_ball_def)
lemma closed_ball_open_ball:
assumes "e < f"
shows "closed_ball a e ⊆ open_ball a f"
using closed_ballD'[of _ a e] closed_ballD[of _ a e] assms
by(fastforce simp: open_ball_def)
lemma closed_ball_open_ball_un1:
assumes "e > 0"
shows "open_ball a e ∪ {x∈S. dist a x = e} = closed_ball a e"
using assms dist_notin by(auto simp: open_ball_def closed_ball_def)
lemma closed_ball_open_ball_un2:
assumes "a ∈ S"
shows "open_ball a e ∪ {x∈S. dist a x = e} = closed_ball a e"
using assms by(auto simp: open_ball_def closed_ball_def)
definition mtopology :: "'a topology" where
"mtopology = topology (λU. U ⊆ S ∧ (∀x∈U. ∃ε>0. open_ball x ε ⊆ U))"
lemma mtopology_istopology:
"istopology (λU. U ⊆ S ∧ (∀x∈U. ∃ε>0. open_ball x ε ⊆ U))"
unfolding istopology_def
proof safe
fix U1 U2 x
assume h1: "U1 ⊆ S" "∀y∈U1. ∃ε>0. open_ball y ε ⊆ U1"
and h2: "U2 ⊆ S" "∀y∈U2. ∃ε>0. open_ball y ε ⊆ U2"
and hx: "x ∈ U1" "x ∈ U2"
obtain ε1 ε2 where
"ε1 > 0" "ε2 > 0""open_ball x ε1 ⊆ U1" "open_ball x ε2 ⊆ U2"
using h1 h2 hx by blast
thus "∃ε>0. open_ball x ε ⊆ U1 ∩ U2"
using open_ball_le[of "min ε1 ε2" ε1 x] open_ball_le[of "min ε1 ε2" ε2 x]
by(auto intro!: exI[where x="min ε1 ε2"])
next
fix 𝒦 U x
assume h:"∀K∈𝒦. K ⊆ S ∧ (∀x∈K. ∃ε>0. open_ball x ε ⊆ K)"
"U ∈ 𝒦" "x ∈ U"
then obtain ε where
"ε > 0" "open_ball x ε ⊆ U"
by blast
thus "∃ε>0. open_ball x ε ⊆ ⋃ 𝒦"
using h(2) by(auto intro!: exI[where x=ε])
qed auto
lemma mtopology_openin_iff:
"openin mtopology U ⟷ U ⊆ S ∧ (∀x∈U. ∃ε>0. open_ball x ε ⊆ U)"
by (simp add: mtopology_def mtopology_istopology)
lemma mtopology_topspace: "topspace mtopology = S"
unfolding topspace_def mtopology_def topology_inverse'[OF mtopology_istopology]
proof -
have "∀x∈S. ∃ε>0. open_ball x ε ⊆ S"
by(auto intro!: exI[where x=1] simp: open_ball_def)
thus "⋃ {U. U ⊆ S ∧ (∀x∈U. ∃ε>0. open_ball x ε ⊆ U)} = S"
by auto
qed
lemma openin_S[simp]: "openin mtopology S"
by (metis openin_topspace mtopology_topspace)
lemma mtopology_open_ball_in':
assumes "x ∈ open_ball a ε"
shows "∃ε'>0. open_ball x ε' ⊆ open_ball a ε"
proof -
show "∃ε'>0. open_ball x ε' ⊆ open_ball a ε"
proof(intro exI[where x="ε - dist a x"] conjI)
show "0 < ε - dist a x"
using open_ballD'[OF assms] open_ballD[OF assms] by auto
next
show "open_ball x (ε - dist a x) ⊆ open_ball a ε"
proof
fix y
assume hy:"y ∈ open_ball x (ε - dist a x)"
show "y ∈ open_ball a ε"
using open_ballD[OF hy] open_ballD[OF assms] open_ballD'(2)[OF assms] dist_tr[OF open_ballD'(2)[OF assms] open_ballD'(1)[OF assms] open_ballD'(1)[OF hy]]
by(auto simp: open_ball_def assms(1) open_ballD'[OF hy])
qed
qed
qed
lemma mtopology_open_ball_in:
assumes "a ∈ S" and "ε > 0"
shows "openin mtopology (open_ball a ε)"
using mtopology_open_ball_in' topology_inverse'[OF mtopology_istopology] open_ball_subset_ofS mtopology_def
by auto
lemma openin_open_ball: "openin mtopology (open_ball a ε)"
proof -
consider "a ∈ S ∧ ε > 0" | "a ∉ S" | "ε ≤ 0" by fastforce
thus ?thesis
by cases (simp_all add: mtopology_open_ball_in open_ball_le_0 open_ball_nin)
qed
lemma closedin_closed_ball: "closedin mtopology (closed_ball a ε)"
unfolding closedin_def mtopology_topspace mtopology_openin_iff
proof safe
fix x
assume h:"x ∈ S" "x ∉ closed_ball a ε"
consider "a ∉ S" | "ε < 0" | "a ∈ S" "ε ≥ 0" by fastforce
thus "∃ε'>0. open_ball x ε' ⊆ S - closed_ball a ε"
proof cases
case 3
then have "dist a x > ε"
using h by(auto simp: closed_ball_def)
show ?thesis
proof(intro exI[where x="dist a x - ε"] conjI)
show "open_ball x (dist a x - ε) ⊆ S - closed_ball a ε"
proof safe
fix z
assume h':"z ∈ open_ball x (dist a x - ε)" "z ∈ closed_ball a ε"
have "dist a x ≤ dist a z + dist z x"
by(auto intro!: dist_tr 3 open_ballD'[OF h'(1)])
also have "... ≤ ε + dist z x"
using closed_ballD[OF h'(2)] by simp
also have "... < dist a x"
using open_ballD[OF h'(1),simplified dist_sym[of x]] by auto
finally show False ..
qed(use open_ball_subset_ofS ‹dist a x > ε› in auto)
qed(use open_ball_subset_ofS ‹dist a x > ε› in auto)
qed(auto simp: closed_ball_nin closed_ball_le_0 open_ball_subset_ofS intro!: exI[where x=1])
qed(use closed_ball_subset_ofS in auto)
lemma mtopology_def2:
"mtopology = topology_generated_by {open_ball a ε | a ε. a ∈ S ∧ ε > 0}"
(is "?lhs = ?rhs")
proof -
have "⋀U. openin ?lhs U = openin ?rhs U"
proof
fix U
assume h:"openin mtopology U"
then have "∀x∈ U. ∃ε > 0. open_ball x ε ⊆ U"
using topology_inverse'[OF mtopology_istopology]
by(simp add: mtopology_def)
then obtain ε where he:
"⋀x. x ∈ U ⟹ ε x > 0 ∧ open_ball x (ε x) ⊆ U"
using bchoice[of U "λx ε. ε > 0 ∧ open_ball x ε ⊆ U"]
by blast
have "U = ⋃{open_ball x (ε x)|x. x∈ U}"
proof
show "⋃ {open_ball x (ε x) |x. x ∈ U} ⊆ U"
using he by auto
next
show "U ⊆ ⋃ {open_ball x (ε x) |x. x ∈ U}"
proof
fix a
assume ha:"a ∈ U"
then have "a ∈ open_ball a (ε a)"
using he[of a] open_ball_ina[of a "ε a"] openin_subset[OF h,simplified]
by(auto simp: mtopology_topspace)
thus "a ∈ ⋃ {open_ball x (ε x) |x. x ∈ U}"
using ha by auto
qed
qed
also have "generate_topology_on {open_ball a ε |a ε. a ∈ S ∧ 0 < ε} ..."
apply(rule generate_topology_on.UN)
apply(rule generate_topology_on.Basis)
using he openin_subset[OF h,simplified]
by(fastforce simp: mtopology_topspace)
finally show "openin (topology_generated_by {open_ball a ε |a ε. a ∈ S ∧ 0 < ε}) U"
by (simp add: openin_topology_generated_by_iff)
next
fix U
assume "openin (topology_generated_by {open_ball a ε |a ε. a ∈ S ∧ 0 < ε}) U"
then have "generate_topology_on {open_ball a ε |a ε. a ∈ S ∧ 0 < ε} U"
by (simp add: openin_topology_generated_by_iff)
thus "openin mtopology U"
apply induction
using mtopology_open_ball_in
by auto
qed
thus ?thesis
by(simp add: topology_eq)
qed
abbreviation mtopology_subbasis :: "'a set set ⇒ bool" where
"mtopology_subbasis 𝒪 ≡ subbase_of mtopology 𝒪"
lemma mtopology_subbasis1:
"mtopology_subbasis {open_ball a ε | a ε. a ∈ S ∧ ε > 0}"
by(simp add: mtopology_def2 subbase_of_def)
abbreviation mtopology_basis :: "'a set set ⇒ bool" where
"mtopology_basis 𝒪 ≡ base_of mtopology 𝒪"
lemma mtopology_basis_ball:
"mtopology_basis {open_ball a ε | a ε. a ∈ S ∧ ε > 0}"
unfolding base_of_def
proof -
show "∀U. openin mtopology U = (∃𝒰. U = ⋃ 𝒰 ∧ 𝒰 ⊆ {open_ball a ε |a ε. a ∈ S ∧ 0 < ε})"
proof safe
fix U
assume "openin mtopology U"
then have "U ⊆ S" "⋀x. x∈U ⟹ ∃ε>0. open_ball x ε ⊆ U"
by(auto simp: mtopology_openin_iff)
then obtain ε where he:
"⋀x. x ∈ U ⟹ ε x > 0" "⋀x. x ∈ U ⟹ open_ball x (ε x) ⊆ U"
by metis
hence "(⋃ { open_ball x (ε x) | x. x ∈ U}) = U"
using ‹U ⊆ S› open_ball_ina[of _ "ε _"] by fastforce
thus "∃𝒰. U = ⋃ 𝒰 ∧ 𝒰 ⊆ {open_ball a ε |a ε. a ∈ S ∧ 0 < ε}"
using he(1) ‹U ⊆ S› by(fastforce intro!: exI[where x="{ open_ball x (ε x) | x. x ∈ U}"])
qed(use mtopology_open_ball_in in blast)
qed
abbreviation sequence :: "(nat ⇒ 'a) set" where
"sequence ≡ UNIV → S"
lemma sequence_comp:
"xn ∈ sequence ⟹ (λn. (xn (a n))) ∈ sequence"
"xn ∈ sequence ⟹ xn ∘ an ∈ sequence"
by auto
definition converge_to_inS :: "[nat ⇒ 'a, 'a] ⇒ bool" where
"converge_to_inS f s ≡ f ∈ sequence ∧ s ∈ S ∧ (λn. dist (f n) s) ⇢ 0"
lemma converge_to_inS_const:
assumes "x ∈ S"
shows "converge_to_inS (λn. x) x"
using assms dist_0[of x x] by(simp add: converge_to_inS_def)
lemma converge_to_inS_subseq:
assumes "strict_mono a" "converge_to_inS f s"
shows "converge_to_inS (f ∘ a) s"
proof -
have "((λn. dist (f n) s) ∘ a) ⇢ 0"
using assms by(auto intro!: LIMSEQ_subseq_LIMSEQ simp: converge_to_inS_def)
thus ?thesis
using assms by(auto simp: converge_to_inS_def comp_def)
qed
lemma converge_to_inS_ignore_initial:
assumes "converge_to_inS xn x"
shows "converge_to_inS (λn. xn (n + k)) x"
using LIMSEQ_ignore_initial_segment[of "λn. dist (xn n) x" 0 k] assms
by(auto simp: converge_to_inS_def)
lemma converge_to_inS_offset:
assumes "converge_to_inS (λn. xn (n + k)) x" "xn ∈ sequence"
shows "converge_to_inS xn x"
using LIMSEQ_offset[of "λn. dist (xn n) x" k] assms
by(auto simp: converge_to_inS_def)
lemma converge_to_inS_def2:
"converge_to_inS f s ⟷ (f ∈ sequence ∧ s ∈ S ∧ (∀ε>0. ∃N. ∀n≥N. dist (f n) s < ε))"
proof
assume h:"converge_to_inS f s "
show "f ∈ sequence ∧ s ∈ S ∧ (∀ε>0. ∃N. ∀n≥N. dist (f n) s < ε)"
proof safe
fix ε :: real
assume he:"0 < ε"
have hs:"⋀S. open S ⟹ 0 ∈ S ⟹ (∃N. ∀n≥N. dist (f n) s ∈ S)"
using h lim_explicit[of "λn. dist (f n) s" 0]
by(simp add: converge_to_inS_def)
then obtain N where
"∀n≥N. dist (f n) s ∈ {-1<..<ε}"
using hs[of "{-1<..<ε}"] he by fastforce
thus "∃N. ∀n≥N. dist (f n) s < ε"
by(auto intro!: exI[where x=N])
qed(use h[simplified converge_to_inS_def] in auto)
next
assume h:"f ∈ sequence ∧ s ∈ S ∧ (∀ε>0. ∃N. ∀n≥N. dist (f n) s < ε)"
have "∀S. open S ⟶ 0 ∈ S ⟶ (∃N. ∀n≥N. dist (f n) s ∈ S)"
proof safe
fix S :: "real set"
assume hs:"open S" "0 ∈ S"
then obtain ε where he:
"ε > 0" "ball 0 ε ⊆ S"
using open_contains_ball[of S] by fastforce
then obtain N where
"∀n≥N. dist (f n) s < ε"
using h by auto
thus "∃N. ∀n≥N. dist (f n) s ∈ S"
using he dist_geq0 by(auto intro!: exI[where x=N])
qed
thus "converge_to_inS f s "
using lim_explicit[of "λn. dist (f n) s" 0] h
by(simp add: converge_to_inS_def)
qed
lemma converge_to_inS_def2':
"converge_to_inS f s ⟷ (f ∈ sequence ∧ s ∈ S ∧ (∀ε>0. ∃N. ∀n≥N. (f n) ∈ open_ball s ε))"
unfolding converge_to_inS_def2 open_ball_def dist_sym[of s]
by fastforce
lemma converge_to_inS_unique:
assumes "converge_to_inS f x" "converge_to_inS f y"
shows "x = y"
proof -
have inS:"⋀n. f n ∈ S" "x ∈ S" "y ∈ S"
using assms by(auto simp: converge_to_inS_def)
have "¦dist x y¦ < ε" if "ε > 0" for ε
proof -
have "0 < ε / 2" using that by simp
then obtain N1 N2 where hn:
"⋀n. n ≥ N1 ⟹ dist (f n) x < ε / 2" "⋀n. n ≥ N2 ⟹ dist (f n) y < ε / 2"
using assms converge_to_inS_def2 by blast
have "dist x y ≤ dist (f (max N1 N2)) x + dist (f (max N1 N2)) y"
unfolding dist_sym[of "f (max N1 N2)" x] by(rule dist_tr[OF inS(2) inS(1)[of "max N1 N2"] inS(3)])
also have "... < ε / 2 + ε / 2"
by(rule add_strict_mono) (use hn[of "max N1 N2"] in auto)
finally show ?thesis
using dist_geq0[of x y] by simp
qed
hence "dist x y = 0"
using zero_less_abs_iff by blast
thus ?thesis
using dist_0[OF inS(2,3)] by simp
qed
lemma mtopology_closedin_iff: "closedin mtopology M ⟷ M ⊆ S ∧ (∀f∈(UNIV → M). ∀s. converge_to_inS f s ⟶ s ∈ M)"
proof
assume "closedin mtopology M"
then have h:"∀x∈S - M. ∃ε>0. open_ball x ε ⊆ S - M"
by (simp add: closedin_def mtopology_openin_iff mtopology_topspace)
show "M ⊆ S ∧ (∀f∈UNIV → M. ∀s. converge_to_inS f s ⟶ s ∈ M)"
proof safe
fix f :: "nat ⇒ 'a" and s
assume hf:"f ∈ UNIV → M" "converge_to_inS f s"
show "s ∈ M"
proof(rule ccontr)
assume "s ∉ M"
then have "s ∈ S - M"
using hf(2) by(auto simp: converge_to_inS_def)
then obtain ε where "ε > 0" "open_ball s ε ⊆ S - M"
using h by auto
then obtain N where "⋀n. n ≥ N ⟹ f n ∈ open_ball s ε"
using hf(2) by(auto simp: converge_to_inS_def2') metis
from ‹open_ball s ε ⊆ S - M› this[of N] hf(1)
show False by auto
qed
qed(rule subsetD[OF closedin_subset[OF ‹closedin mtopology M›,simplified mtopology_topspace]])
next
assume h:"M ⊆ S ∧ (∀f∈UNIV → M. ∀s. converge_to_inS f s ⟶ s ∈ M)"
show "closedin mtopology M"
unfolding closedin_def mtopology_openin_iff mtopology_topspace
proof safe
fix x
assume "x ∈ S" "x ∉ M"
show "∃ε>0. open_ball x ε ⊆ S - M"
proof(rule ccontr)
assume "¬ (∃ε>0. open_ball x ε ⊆ S - M)"
then have "∀ε>0. open_ball x ε ∩ M ≠ {}"
by (metis Diff_mono Diff_triv open_ball_subset_ofS subset_refl)
hence "∀n. ∃a. a ∈ open_ball x (1 / real (Suc n)) ∩ M"
by (meson of_nat_0_less_iff subsetI subset_empty zero_less_Suc zero_less_divide_1_iff)
then obtain f where hf:"⋀n. f n ∈ open_ball x (1 / (Suc n)) ∩ M" by metis
hence "f ∈ UNIV → M" by auto
moreover have "converge_to_inS f x"
unfolding converge_to_inS_def2'
proof safe
show "f x ∈ S" for x
using h hf by auto
next
fix ε
assume "(0::real) < ε"
then obtain N where "1 / real (Suc N) < ε"
using nat_approx_posE by blast
show "∃N. ∀n≥N. f n ∈ open_ball x ε"
proof(rule exI[where x=N])
show "∀n≥N. f n ∈ open_ball x ε"
proof safe
fix n
assume "N ≤ n"
then have "1 / real (Suc n) ≤ 1 / real (Suc N)"
by (simp add: frac_le)
also have "... ≤ ε"
using ‹1 / real (Suc N) < ε› by simp
finally show "f n ∈ open_ball x ε"
using open_ball_le[of "1 / real (Suc n)" ε x] hf by auto
qed
qed
qed fact
ultimately show False
using h ‹x ∉ M› by blast
qed
qed(use h in auto)
qed
lemma mtopology_closedin_iff2: "closedin mtopology M ⟷ M ⊆ S ∧ (∀x. x ∈ M ⟷ (∀ε>0. open_ball x ε ∩ M ≠ {}))"
proof
assume h:"closedin mtopology M"
have 1: "M ⊆ S"
using h by(auto simp add: mtopology_closedin_iff)
show "M ⊆ S ∧ (∀x. (x ∈ M) = (∀ε>0. open_ball x ε ∩ M ≠ {}))"
proof safe
fix ε x
assume "x ∈ M" "(0 :: real) < ε" "open_ball x ε ∩ M = {}"
thus False
using open_ball_ina[of x ε] 1 by blast
next
fix x
assume "∀ε>0. open_ball x ε ∩ M ≠ {}"
hence "∃f. f ∈ open_ball x (1 / real (Suc n)) ∩ M" for n
by (meson all_not_in_conv divide_pos_pos of_nat_0_less_iff zero_less_Suc zero_less_one)
then obtain f where hf:"⋀n. f n ∈ open_ball x (1 / real (Suc n)) ∩ M"
by metis
hence "x ∈ S" "f ∈ UNIV → M"
using open_ballD'(2)[of "f 0" x] by auto
have "converge_to_inS f x"
unfolding converge_to_inS_def2'
proof safe
show "⋀x. f x ∈ S"
using 1 ‹f ∈ UNIV → M› by auto
next
fix ε
assume "(0 :: real) < ε"
then obtain N where hN: "1 / real (Suc N) < ε"
using nat_approx_posE by blast
show "∃N. ∀n≥N. f n ∈ open_ball x ε"
proof(rule exI[where x="N"])
show "∀n≥N. f n ∈ open_ball x ε"
proof safe
fix n
assume "N ≤ n"
then have "1 / real (Suc n) ≤ 1 / real (Suc N)"
using inverse_of_nat_le by blast
thus "f n ∈ open_ball x ε "
using hf[of n] open_ball_le[of "1 / real (Suc n)" "ε" x] hN
by auto
qed
qed
qed fact
with ‹f ∈ UNIV → M› show "x ∈ M"
using h[simplified mtopology_closedin_iff] by simp
qed(use 1 in auto)
next
assume"M ⊆ S ∧ (∀x. (x ∈ M) ⟷ (∀ε>0. open_ball x ε ∩ M ≠ {}))"
hence h:"M ⊆ S" "⋀x. (x ∈ M) ⟷ (∀ε>0. open_ball x ε ∩ M ≠ {})"
by simp_all
show "closedin mtopology M"
unfolding mtopology_closedin_iff
proof safe
fix f s
assume h':"f ∈ UNIV → M" "converge_to_inS f s"
hence "s ∈ S" by(simp add: converge_to_inS_def)
have "open_ball s ε ∩ M ≠ {}" if "ε > 0" for ε
proof -
obtain N where hN:"⋀n. n ≥ N ⟹ dist (f n) s < ε"
using h'(2) ‹ε > 0› by(auto simp: converge_to_inS_def2) metis
have "f N ∈ open_ball s ε ∩ M"
using ‹f ∈ UNIV → M› ‹s ∈ S› hN[of N] that open_ball_def[of s ε] h(1) dist_sym[of s]
by auto
thus "open_ball s ε ∩ M ≠ {}" by auto
qed
with h(2)[of s] show "s ∈ M" by simp
qed(use h(1) in auto)
qed
lemma mtopology_openin_iff2:
"openin mtopology A ⟷ A ⊆ S ∧ (∀f x. converge_to_inS f x ∧ x ∈ A ⟶ (∃N. ∀n≥N. f n ∈ A))"
proof
show "openin mtopology A ⟹ A ⊆ S ∧ (∀f x. converge_to_inS f x ∧ x ∈ A ⟶ (∃N. ∀n≥N. f n ∈ A))"
unfolding mtopology_openin_iff
proof safe
fix f x
assume "∀x∈A. ∃ε>0. open_ball x ε ⊆ A" "converge_to_inS f x" "x ∈ A"
then obtain ε where "ε > 0" "open_ball x ε ⊆ A"
by auto
then obtain N where "⋀n. n ≥ N ⟹ dist (f n) x < ε"
using ‹converge_to_inS f x› by(fastforce simp: converge_to_inS_def2)
hence "⋀n. n ≥ N ⟹ f n ∈ open_ball x ε"
using ‹converge_to_inS f x› by(auto simp: dist_sym[of _ x] open_ball_def converge_to_inS_def)
with ‹open_ball x ε ⊆ A› show "∃N. ∀n≥N. f n ∈ A"
by(auto intro!: exI[where x=N])
qed
next
assume "A ⊆ S ∧ (∀f x. converge_to_inS f x ∧ x ∈ A ⟶ (∃N. ∀n≥N. f n ∈ A))"
hence h:"A ⊆ S" "⋀f x. converge_to_inS f x ⟹ x ∈ A ⟹ ∃N. ∀n≥N. f n ∈ A"
by auto
have "closedin mtopology (S - A)"
unfolding mtopology_closedin_iff
proof safe
fix f s
assume hf:"f ∈ UNIV → S - A"
"converge_to_inS f s"
have False if "s ∈ A"
proof -
from h(2)[OF hf(2) that]
obtain N where "⋀n. n ≥ N ⟹ f n ∈ A" by auto
from hf (1) this[of N] show False by auto
qed
thus "s ∈ S" "s ∈ A ⟹ False"
using hf(2) by (auto simp: converge_to_inS_def)
qed
thus "openin mtopology A"
using h(1) mtopology_topspace by(simp add: openin_closedin_eq)
qed
lemma closure_of_mtopology: "mtopology closure_of A = {a. ∀ε>0. open_ball a ε ∩ A ≠ {}}"
proof safe
fix x ε
assume "x ∈ mtopology closure_of A" "(0 :: real) < ε" "open_ball x ε ∩ A = {}"
then show False
using mtopology_closedin_iff2[of "mtopology closure_of A",simplified]
by (simp add: mtopology_open_ball_in' mtopology_openin_iff open_ball_subset_ofS openin_Int_closure_of_eq_empty)
next
fix x
assume "∀ε>0. open_ball x ε ∩ A ≠ {}"
then have "∀ε>0. open_ball x ε ∩ mtopology closure_of A ≠ {}"
by (simp add: mtopology_open_ball_in' mtopology_openin_iff open_ball_subset_ofS openin_Int_closure_of_eq_empty)
thus "x ∈ mtopology closure_of A"
using mtopology_closedin_iff2[of "mtopology closure_of A",simplified]
by auto
qed
lemma closure_of_mtopology':
"mtopology closure_of A = {a. ∃an∈UNIV → A. converge_to_inS an a}"
proof safe
fix a
assume "a ∈ mtopology closure_of A"
then have "∀ε>0. open_ball a ε ∩ A ≠ {}"
by(simp add: closure_of_mtopology)
hence "⋀n. ∃an. an ∈ open_ball a (1/real (Suc n)) ∩ A"
by (meson all_not_in_conv divide_pos_pos of_nat_0_less_iff zero_less_Suc zero_less_one)
then obtain an where han:"⋀n. an n ∈ open_ball a (1/real (Suc n)) ∩ A" by metis
hence "an ∈ UNIV → A" by auto
show "∃an∈UNIV → A. converge_to_inS an a"
proof(safe intro!: bexI[where x=an] ‹an ∈ UNIV → A›)
show "converge_to_inS an a"
unfolding converge_to_inS_def2'
proof safe
show "an n ∈ S" "a ∈ S" for n
using open_ballD'(2)[of "an 0" a] open_ballD'(1)[of "an n"] han by auto
next
fix ε
assume "(0 :: real) < ε"
then obtain N where "1 / real (Suc N) ≤ ε"
by (meson less_eq_real_def nat_approx_posE)
show "∃N. ∀n≥N. an n ∈ open_ball a ε"
proof(safe intro!: exI[where x=N])
fix n
assume "N ≤ n"
then have "1 / real (Suc n) ≤ 1 / real (Suc N)"
by (simp add: frac_le)
from open_ball_le[OF order_trans[OF this ‹1 / real (Suc N) ≤ ε›]]
show "an n ∈ open_ball a ε"
using han by auto
qed
qed
qed
next
fix a an
assume h:"an ∈ UNIV → A" "converge_to_inS an a"
have "∀ε>0. open_ball a ε ∩ A ≠ {}"
proof safe
fix ε
assume "(0 :: real) < ε" "open_ball a ε ∩ A = {}"
then obtain N where "an N ∈ open_ball a ε"
using h(2) converge_to_inS_def2' by blast
with ‹open_ball a ε ∩ A = {}› h(1) show False by auto
qed
thus "a ∈ mtopology closure_of A"
by(simp add: closure_of_mtopology)
qed
lemma closure_of_mtopology_an:
assumes "a ∈ mtopology closure_of A"
obtains an where "an∈UNIV → A" "converge_to_inS an a"
using assms by(auto simp: closure_of_mtopology')
lemma closure_of_open_ball: "mtopology closure_of open_ball a ε ⊆ closed_ball a ε"
by(rule closure_of_minimal_eq[THEN iffD2]) (auto simp: open_ball_subset_ofS mtopology_topspace closedin_closed_ball open_ball_closed_ball)
lemma interior_of_closed_ball: "open_ball a e ⊆ mtopology interior_of closed_ball a e"
by(auto simp: interior_of_maximal_eq openin_open_ball open_ball_closed_ball)
lemma derived_set_of_mtopology:
"mtopology derived_set_of A = {a. ∃an∈UNIV → A. (∀n. an n ≠ a) ∧ converge_to_inS an a}"
proof safe
fix a
assume "a ∈ mtopology derived_set_of A"
then have h:"a ∈ S" "⋀v. a ∈ v ⟹ openin mtopology v ⟹ ∃y. y ≠ a ∧ y ∈ v ∧ y ∈ A"
by(auto simp: in_derived_set_of mtopology_topspace)
hence "a ∈ open_ball a (1 / real (Suc n))" for n
by(auto intro!: open_ball_ina)
from h(2)[OF this openin_open_ball[of a]]
obtain an where an:"⋀n. an n ≠ a" "⋀n. an n ∈ open_ball a (1 / real (Suc n))" "⋀n. an n ∈ A"
by metis
show "∃an∈UNIV → A. (∀n. an n ≠ a) ∧ converge_to_inS an a"
proof(safe intro!: bexI[where x=an] an(1))
show "converge_to_inS an a"
unfolding converge_to_inS_def2'
proof safe
show "⋀x. an x ∈ S"
using an(2) open_ball_subset_ofS by auto
next
fix ε
assume "(0 :: real) < ε"
then obtain N where hN:"1 / real (Suc N) < ε"
using nat_approx_posE by blast
show "∃N. ∀n≥N. an n ∈ open_ball a ε"
proof(safe intro!: exI[where x=N])
fix n
assume "N ≤ n"
then have "1 / real (Suc n) ≤ 1 / real (Suc N)"
by (simp add: frac_le)
from order.strict_trans1[OF this hN] open_ball_le[of _ ε a] an(2)[of n]
show "an n ∈ open_ball a ε" by(auto simp: less_le)
qed
qed(use h in auto)
qed(use an in auto)
next
fix a an
assume h:"an ∈ UNIV → A" "∀n. an n ≠ a" "converge_to_inS an a"
have "∃y. y ≠ a ∧ y ∈ v ∧ y ∈ A" if "a ∈ v" "openin mtopology v" for v
proof -
obtain ε where he:"ε > 0" "a ∈ open_ball a ε" "open_ball a ε ⊆ v"
by (meson ‹a ∈ v› ‹openin mtopology v› converge_to_inS_def2 h(3) mtopology_openin_iff open_ball_ina)
then obtain N where hn:"⋀n. n ≥ N ⟹ an n ∈ open_ball a ε"
using h(3) by(fastforce simp: converge_to_inS_def2')
show " ∃y. y ≠ a ∧ y ∈ v ∧ y ∈ A"
using h(1,2) he hn by(auto intro!: exI[where x="an N"])
qed
thus "a ∈ mtopology derived_set_of A"
using h(3) by(auto simp: in_derived_set_of converge_to_inS_def mtopology_topspace)
qed
lemma isolated_points_of_mtopology:
"mtopology isolated_points_of A = {a∈S∩A. ∀an∈UNIV → A. converge_to_inS an a ⟶ (∃no. ∀n≥no. an n = a)}"
proof safe
fix a an
assume h:"a ∈ mtopology isolated_points_of A" "converge_to_inS an a" "an ∈ UNIV → A"
then have ha:"a ∈ topspace mtopology" "a ∈ A" "∃U. a ∈ U ∧ openin mtopology U ∧ U ∩ (A - {a}) = {}"
by(simp_all add: in_isolated_points_of)
then obtain U where u:"a ∈ U" "openin mtopology U" "U ∩ (A - {a}) = {}"
by auto
then obtain ε where e: "ε > 0" "open_ball a ε ⊆ U"
by(auto simp: mtopology_openin_iff)
then obtain N where "⋀n. n ≥ N ⟹ an n ∈ open_ball a ε"
using h(2) by(fastforce simp: converge_to_inS_def2')
thus "∃no. ∀n≥no. an n = a"
using h(3) e(2) u(3) by(auto intro!: exI[where x=N])
qed (auto simp: derived_set_of_mtopology isolated_points_of_def mtopology_topspace)
lemma perfect_set_open_ball_infinite:
assumes "perfect_set mtopology A"
shows "closedin mtopology A ∧ (∀a∈A. ∀ε>0. infinite (open_ball a ε))"
proof safe
fix a ε
assume h: "a ∈ A" "0 < ε" "finite (open_ball a ε)"
then have "a ∈ S"
using open_ball_ina[OF _ ‹0 < ε›,of a] perfect_setD(2)[OF assms]
by(auto simp: mtopology_topspace)
have "∃e > 0. open_ball a e = {a}"
proof -
consider "open_ball a ε = {a}" | "{a} ⊂ open_ball a ε"
using open_ball_ina[OF ‹a ∈ S› h(2)] by blast
thus ?thesis
proof cases
case 1
with h(2) show ?thesis by auto
next
case 2
then have nen:"{dist a b |b. b ∈ open_ball a ε ∧ a ≠ b} ≠ {}"
by auto
have fin: "finite {dist a b |b. b ∈ open_ball a ε ∧ a ≠ b}"
using h(3) by auto
define e where "e ≡ Min {dist a b |b. b ∈ open_ball a ε ∧ a ≠ b}"
have "e > 0"
using dist_0[OF ‹a ∈ S› open_ballD'(1)[of _ a ε]] dist_geq0[of a]
by(auto simp: e_def Min_gr_iff[OF fin nen] order_neq_le_trans)
have bd:"⋀b. b ∈ open_ball a ε ⟹ a ≠ b ⟹ e ≤ dist a b"
by(auto simp: e_def Min_le_iff[OF fin nen])
have "e ≤ ε"
using nen open_ballD[of _ a ε]
by(fastforce simp add: e_def Min_le_iff[OF fin nen])
show ?thesis
proof(safe intro!: exI[where x=e])
fix x
assume x:"x ∈ open_ball a e"
then show "x = a"
using open_ball_le[OF ‹e ≤ ε›,of a] open_ballD[OF x] bd[of x]
by auto
qed (simp_all add: open_ball_ina[OF ‹a ∈ S› ‹e > 0›] ‹0 < e›)
qed
qed
then obtain e where e:"e > 0" "open_ball a e = {a}" by auto
show False
using perfect_setD(3)[OF assms h(1) open_ball_ina[OF ‹a ∈ S› ‹e > 0›]]
by(auto simp: openin_open_ball) (use e(2) in auto)
qed(use perfect_setD[OF assms] in simp)
lemma nbh_subset:
assumes A: "A ⊆ S" and e: "e > 0"
shows "A ⊆ (⋃a∈A. open_ball a e)"
using A open_ball_ina[OF _ e] by auto
lemma nbh_decseq:
assumes "decseq an"
shows "decseq (λn. ⋃a∈A. open_ball a (an n))"
proof(safe intro!: decseq_SucI)
fix n a b
assume "a ∈ A" "b ∈ open_ball a (an (Suc n))"
with open_ball_le[OF decseq_SucD[OF assms]] show "b ∈ (⋃c∈A. open_ball c (an n))"
by(auto intro!: bexI[where x=a] simp: frac_le)
qed
lemma nbh_Int:
assumes A: "A ≠ {}" "A ⊆ S"
and an:"⋀n. an n > 0" "decseq an" "an ⇢ 0"
shows "(⋂n. ⋃a∈A. open_ball a (an n)) = mtopology closure_of A"
proof safe
fix x
assume "x ∈ (⋂n. ⋃a∈A. open_ball a (an n))"
then have h:"∀n. ∃a∈A. x ∈ open_ball a (an n)"
by auto
hence x:"x ∈ S"
using open_ball_subset_ofS by auto
show "x ∈ mtopology closure_of A"
unfolding closure_of_mtopology
proof safe
fix e :: real
assume h':"e > 0" "open_ball x e ∩ A = {}"
then obtain n where n:"an n < e"
using an(1,3) by(auto simp: LIMSEQ_def abs_of_pos) (metis dual_order.refl)
from h obtain a where "a ∈ A" "x ∈ open_ball a (an n)"
by auto
with h'(2) open_ball_le[of "an n" e x] n
show False
by(auto simp: open_ball_inverse[of x])
qed
next
fix x n
assume "x ∈ mtopology closure_of A"
with an(1) have "open_ball x (an n) ∩ A ≠ {}"
by(auto simp: closure_of_mtopology)
thus "x ∈ (⋃a∈A. open_ball a (an n))"
by(auto simp: open_ball_inverse[of x])
qed
lemma nbh_add: "(⋃b∈(⋃a∈A. open_ball a e). open_ball b f) ⊆ (⋃a∈A. open_ball a (e + f))"
proof safe
fix a x b
assume h:"a ∈ A" "b ∈ open_ball a e" "x ∈ open_ball b f"
show "x ∈ (⋃a∈A. open_ball a (e + f))"
proof(rule UN_I[OF h(1)])
have "dist a x ≤ dist a b + dist b x"
by(auto intro!: dist_tr open_ballD'(2)[OF h(2)] open_ballD'[OF h(3)])
also have "... < e + f"
using open_ballD[OF h(2)] open_ballD[OF h(3)] by auto
finally show "x ∈ open_ball a (e + f)"
using open_ballD'[OF h(2)] open_ballD'[OF h(3)]
by(auto simp: open_ball_def)
qed
qed
definition convergent_inS :: "(nat ⇒ 'a) ⇒ bool" where
"convergent_inS f ≡ ∃s. converge_to_inS f s"
lemma convergent_inS_const:
assumes "x ∈ S"
shows "convergent_inS (λn. x)"
using converge_to_inS_const[OF assms] by(auto simp: convergent_inS_def)
lemma convergent_inS_ignore_initial:
assumes "convergent_inS xn"
shows "convergent_inS (λn. xn (n + k))"
using converge_to_inS_ignore_initial[of xn] assms
by(auto simp: convergent_inS_def)
lemma convergent_inS_offset:
assumes "convergent_inS (λn. xn (n + k))" "xn ∈ sequence"
shows "convergent_inS xn"
using converge_to_inS_offset[of xn k] assms
by(auto simp: convergent_inS_def)
definition the_limit_of :: "(nat ⇒ 'a) ⇒ 'a" where
"the_limit_of xn ≡ THE x. converge_to_inS xn x"
lemma the_limit_if_converge:
assumes "convergent_inS xn"
shows "converge_to_inS xn (the_limit_of xn)"
unfolding the_limit_of_def
by(rule theI') (auto simp: assms[simplified convergent_inS_def] converge_to_inS_unique)
lemma the_limit_of_eq:
assumes "converge_to_inS xn x"
shows "the_limit_of xn = x"
using assms converge_to_inS_unique the_limit_of_def by auto
lemma the_limit_of_inS:
assumes "convergent_inS xn"
shows "the_limit_of xn ∈ S"
using the_limit_if_converge[OF assms] by(simp add:converge_to_inS_def)
lemma the_limit_of_const:
assumes "x ∈ S"
shows "the_limit_of (λn. x) = x"
by(rule the_limit_of_eq[OF converge_to_inS_const[OF assms]])
lemma convergent_inS_dest1:
assumes "convergent_inS f"
shows "f n ∈ S"
using assms by(auto simp: convergent_inS_def converge_to_inS_def2)
definition Cauchy_inS:: "(nat ⇒ 'a) ⇒ bool" where
"Cauchy_inS f ≡ f ∈ sequence ∧ (∀ε>0. ∃N. ∀n≥N. ∀m≥N. dist (f n) (f m) < ε)"
lemma Cauchy_inS_def2:
"Cauchy_inS f ⟷ f ∈ sequence ∧ (∀ε>0. ∃N. ∀n≥N. f n ∈ open_ball (f N) ε)"
unfolding Cauchy_inS_def
proof safe
fix ε :: real
assume h:"f ∈ sequence" " ∀ε>0. ∃N. ∀n≥N. ∀m≥N. dist (f n) (f m) < ε" "0 < ε"
then obtain N where hn:
"⋀n m. n ≥ N ⟹ m≥N ⟹ dist (f n) (f m) < ε"
by fastforce
show "∃N. ∀n≥N. f n ∈ open_ball (f N) ε"
proof(safe intro!: exI[where x=N])
fix n
assume "N ≤ n"
then show "f n ∈ open_ball (f N) ε"
using h(1) hn[of N n] by(auto simp: open_ball_def)
qed
next
fix ε :: real
assume h:"f ∈ sequence" "∀ε>0. ∃N. ∀n≥N. f n ∈ open_ball (f N) ε" "0 < ε"
then obtain N where hn:
"⋀n. n ≥ N ⟹ f n ∈ open_ball (f N) (ε/2)"
using linordered_field_class.half_gt_zero[OF h(3)] by blast
show "∃N. ∀n≥N. ∀m≥N. dist (f n) (f m) < ε"
proof(safe intro!: exI[where x=N])
fix n m
assume "N ≤ n" "N ≤ m"
from order.strict_trans1[OF dist_tr [of "f n" "f N" "f m"] strict_ordered_ab_semigroup_add_class.add_strict_mono[OF open_ballD[OF hn[OF this(1)],simplified dist_sym[of _ "f n"]] open_ballD[OF hn[OF this(2)]],simplified]]
show "dist (f n) (f m) < ε"
using h(1) by auto
qed
qed
lemma Cauchy_inS_def2':
"Cauchy_inS f ⟷ f ∈ sequence ∧ (∀ε>0. ∃x∈S. ∃N. ∀n≥N. f n ∈ open_ball x ε)"
unfolding Cauchy_inS_def2
proof safe
fix ε :: real
assume h:"f ∈ sequence" "∀ε>0. ∃N. ∀n≥N. f n ∈ open_ball (f N) ε" "0 < ε"
then obtain N where "∀n≥N. f n ∈ open_ball (f N) ε" by auto
thus "∃x∈S. ∃N. ∀n≥N. f n ∈ open_ball x ε"
using h(1) by(auto intro!: exI[where x=N] bexI[where x="f N"])
next
fix ε :: real
assume h:"f ∈ sequence" "∀ε>0. ∃x∈S. ∃N. ∀n≥N. f n ∈ open_ball x ε" "0 < ε"
then obtain x N where hxn:
"x ∈ S" "⋀n. n ≥ N ⟹ f n ∈ open_ball x (ε/2)"
using linordered_field_class.half_gt_zero[OF h(3)] by blast
show "∃N. ∀n≥N. f n ∈ open_ball (f N) ε"
proof(safe intro!: exI[where x=N])
fix n
assume "N ≤ n"
from order.strict_trans1[OF dist_tr strict_ordered_ab_semigroup_add_class.add_strict_mono[OF open_ballD[OF hxn(2)[OF order.refl],simplified dist_sym[of x]] open_ballD[OF hxn(2)[OF this]],simplified]]
show "f n ∈ open_ball (f N) ε"
using hxn(1) h(1) by(auto simp: open_ball_def)
qed
qed
lemma Cauchy_inS_def2'':
"Cauchy_inS f ⟷ f ∈ sequence ∧ (∀ε>0. ∃x∈S. ∃N. ∀n≥N. dist x (f n) < ε)"
unfolding Cauchy_inS_def2'
proof safe
fix ε :: real
assume h:"f ∈ sequence" "∀ε>0. ∃x∈S. ∃N. ∀n≥N. f n ∈ open_ball x ε" "0 < ε"
then obtain x N where
"x ∈ S" "⋀n. n ≥ N ⟹ f n ∈ open_ball x ε"
by blast
then show "∃x∈S. ∃N. ∀n≥N. dist x (f n) < ε"
by(auto intro!: bexI[where x=x] exI[where x=N] simp: open_ballD[of _ x ε])
next
fix ε :: real
assume h:"f ∈ sequence" "∀ε>0. ∃x∈S. ∃N. ∀n≥N. dist x (f n) < ε" "0 < ε"
then obtain x N where
"x ∈ S" "⋀n. n ≥ N ⟹ dist x (f n) < ε" by blast
then show "∃x∈S. ∃N. ∀n≥N. f n ∈ open_ball x ε"
using h(1) by(auto intro!: bexI[where x=x] exI[where x=N] simp: open_ball_def)
qed
lemma Cauchy_inS_dest1:
assumes "Cauchy_inS f"
shows "f n ∈ S"
using assms by(auto simp: Cauchy_inS_def)
lemma Cauchy_if_convergent_inS:
assumes "convergent_inS f"
shows "Cauchy_inS f"
unfolding Cauchy_inS_def
proof safe
fix ε :: real
assume h:"0 < ε"
obtain s where hs:
"s ∈ S" "∀ε>0. ∃N. ∀n≥N. dist (f n) s < ε"
using assms by(auto simp: convergent_inS_def converge_to_inS_def2)
then obtain N where hn:
"⋀n. n≥N ⟹ dist (f n) s < ε/2"
using half_gt_zero[OF h] by blast
show "∃N. ∀n≥N. ∀m≥N. dist (f n) (f m) < ε"
proof(safe intro!: exI[where x=N])
fix n m
assume hnm:"N ≤ n" "N ≤ m"
have "dist (f n) (f m) ≤ dist (f n) s + dist s (f m)"
using convergent_inS_dest1[OF assms] hs
by(auto intro!: dist_tr)
also have "... = dist (f n) s + dist (f m) s"
by(simp add: dist_sym[of s])
also have "... < ε"
using hn[OF hnm(1)] hn[OF hnm(2)] by auto
finally show "dist (f n) (f m) < ε" .
qed
next
show "⋀x. f x ∈ S"
using assms[simplified convergent_inS_def converge_to_inS_def]
by auto
qed
corollary Cauchy_inS_const: "a ∈ S ⟹ Cauchy_inS (λn. a)"
by(auto intro!: Cauchy_if_convergent_inS convergent_inS_const)
lemma converge_if_Cauchy_and_subconverge:
assumes "strict_mono a" "converge_to_inS (f ∘ a) s" "Cauchy_inS f"
shows "converge_to_inS f s"
unfolding converge_to_inS_def2
proof safe
fix ε
assume "(0 :: real) < ε"
then have 1:"0 < ε/2" by auto
then obtain N where hn:"⋀n. n ≥ N ⟹ dist (f (a n)) s < ε/2"
using assms(2) by(simp only: comp_def converge_to_inS_def2) metis
obtain N' where hn':"⋀n m. n ≥ N' ⟹ m ≥ N' ⟹ dist (f n) (f m) < ε/2"
using assms(3) 1 by(simp only: Cauchy_inS_def) metis
show "∃N. ∀n≥N. dist (f n) s < ε"
proof(safe intro!: exI[where x="max N N'"])
fix n
assume "max N N' ≤ n"
then have "N ≤ n" "N' ≤ n" by auto
show "dist (f n) s < ε"
using add_strict_mono[OF hn'[OF ‹N' ≤ n› order_trans[OF ‹N' ≤ n› seq_suble[OF assms(1),of n]]] hn[OF ‹N ≤ n›]] assms(2)
by(auto simp: converge_to_inS_def intro!: order.strict_trans1[OF dist_tr[OF Cauchy_inS_dest1[OF assms(3),of n] Cauchy_inS_dest1[OF assms(3),of "a n"],of s],of ε])
qed
qed(auto simp: Cauchy_inS_dest1[OF assms(3)] assms(2)[simplified converge_to_inS_def])
lemma subCauchy_Cahcuy:
assumes "Cauchy_inS xn" "strict_mono a"
shows "Cauchy_inS (xn ∘ a)"
unfolding Cauchy_inS_def
proof safe
show "⋀x. (xn ∘ a) x ∈ S"
using assms(1) by(simp add: Cauchy_inS_dest1)
next
fix ε
assume "(0 :: real) < ε"
then obtain N where "⋀n m. n ≥ N ⟹ m ≥ N ⟹ dist (xn n) (xn m) < ε"
using assms(1) by(auto simp: Cauchy_inS_def) metis
thus "∃N. ∀n≥N. ∀m≥N. dist ((xn ∘ a) n) ((xn ∘ a) m) < ε"
by(auto intro!: exI[where x=N] dest: order_trans[OF seq_suble[OF assms(2)] strict_mono_leD[OF assms(2)]])
qed
corollary Cauchy_inS_ignore_initial:
assumes "Cauchy_inS xn"
shows "Cauchy_inS (λn. xn (n + k))"
using subCauchy_Cahcuy[OF assms,of "λn. n + k"]
by(auto simp: comp_def strict_monoI)
lemma Cauchy_inS_dist_Cauchy:
assumes "Cauchy_inS xn" "Cauchy_inS yn"
shows "Cauchy (λn. dist (xn n) (yn n))"
unfolding metric_space_class.Cauchy_altdef2 dist_real_def
proof safe
have h:"⋀n. xn n ∈ S" "⋀n. yn n ∈ S"
using assms by(auto simp: Cauchy_inS_dest1)
fix e :: real
assume e:"0 < e"
with assms obtain N1 N2 where N: "⋀n m. n ≥ N1 ⟹ m ≥ N1 ⟹ dist (xn n) (xn m) < e / 2" "⋀n m. n ≥ N2 ⟹ m ≥ N2 ⟹ dist (yn n) (yn m) < e / 2"
by (metis Cauchy_inS_def zero_less_divide_iff zero_less_numeral)
define N where "N ≡ max N1 N2"
then have N': "N ≥ N1" "N ≥ N2" by auto
show "∃N. ∀n≥N. ¦dist (xn n) (yn n) - dist (xn N) (yn N)¦ < e"
proof(safe intro!: exI[where x=N])
fix n
assume n:"N ≤ n"
have "dist (xn n) (yn n) ≤ dist (xn n) (xn N) + dist (xn N) (yn N) + dist (yn N) (yn n)"
"dist (xn N) (yn N) ≤ dist (xn N) (xn n) + dist (xn n) (yn n) + dist (yn n) (yn N)"
using dist_tr[OF h(1)[of n] h(1)[of N] h(2)[of n]] dist_tr[OF h(1)[of N] h(2)[of N] h(2)[of n]]
dist_tr[OF h(1)[of N] h(2)[of n] h(2)[of N]] dist_tr[OF h(1)[of N] h(1)[of n] h(2)[of n]] by auto
thus "¦dist (xn n) (yn n) - dist (xn N) (yn N)¦ < e"
using N(1)[OF N'(1) order.trans[OF N'(1) n]] N(2)[OF N'(2) order.trans[OF N'(2) n]] N(1)[OF order.trans[OF N'(1) n] N'(1)] N(2)[OF order.trans[OF N'(2) n] N'(2)]
by auto
qed
qed
corollary Cauchy_inS_dist_convergent:
assumes "Cauchy_inS xn" "Cauchy_inS yn"
shows "convergent (λn. dist (xn n) (yn n))"
using Cauchy_inS_dist_Cauchy[OF assms] Cauchy_convergent_iff by blast
text ‹🌐‹https://people.bath.ac.uk/mw2319/ma30252/sec-dense.html.››
abbreviation "dense_set ≡ dense_of mtopology"
lemma dense_set_def:
"dense_set U ⟷ U ⊆ S ∧ (∀x∈S. ∀ε>0. open_ball x ε ∩ U ≠ {})"
proof
assume h:" U ⊆ S ∧(∀x∈S. ∀ε>0. open_ball x ε ∩ U ≠ {})"
show "dense_of mtopology U"
proof(rule dense_ofI)
fix V
assume h':"openin mtopology V" "V ≠ {}"
then obtain x where 1:"x ∈ V" by auto
then obtain ε where 2:"ε>0" "open_ball x ε ⊆ V"
using h' mtopology_openin_iff[of V] by blast
have "open_ball x ε ∩ U ≠ {}"
using h 1 2 openin_subset[OF h'(1), simplified mtopology_topspace]
by auto
thus "U ∩ V ≠ {}" using 2 by auto
next
show "U ⊆ topspace mtopology"
using h mtopology_topspace by auto
qed
next
assume h:"dense_of mtopology U"
have "∀x∈S. ∀ε>0. open_ball x ε ∩ U ≠ {}"
proof safe
fix x ε
assume "x ∈ S" "(0 :: real) < ε" "open_ball x ε ∩ U = {}"
then have "open_ball x ε ≠ {}" "openin mtopology (open_ball x ε)"
using open_ball_ina[of x ε] mtopology_open_ball_in[of x ε]
by blast+
thus False
using h ‹open_ball x ε ∩ U = {}› by(auto simp: dense_of_def)
qed
thus "U ⊆ S ∧ (∀x∈S. ∀ε>0. open_ball x ε ∩ U ≠ {})"
using h mtopology_topspace by(auto simp: dense_of_def)
qed
corollary dense_set_balls_cover:
assumes "dense_set U" and "e > 0"
shows "(⋃u∈U. open_ball u e) = S"
using assms open_ball_subset_ofS by(auto simp: dense_set_def) (meson Int_emptyI open_ball_inverse)
lemma dense_set_empty_iff: "dense_set {} ⟷ S = {}"
by(auto simp: dense_set_def ) (use zero_less_one in blast)
lemma dense_set_S: "dense_set S"
using open_ball_ina dense_set_def by blast
lemma dense_set_def2:
"dense_set U ⟷ U ⊆ S ∧ (∀x∈S. ∀ε>0.∃y∈U. dist x y < ε)"
proof
assume h: "dense_set U"
show "U ⊆ S ∧ (∀x∈S. ∀ε>0. ∃y∈U. dist x y < ε)"
proof safe
fix x ε
assume hxe: "x ∈ S" "(0 :: real) < ε"
then obtain z where
"z ∈ open_ball x ε ∩ U"
using h by(fastforce simp: dense_set_def)
thus "∃y∈U. dist x y < ε"
by(auto intro!: bexI[where x=z] simp: open_ball_def hxe)
qed(use h[simplified dense_set_def] in auto)
next
assume h:"U ⊆ S ∧ (∀x∈S. ∀ε>0. ∃y∈U. dist x y < ε)"
show "dense_set U"
unfolding dense_set_def
proof safe
fix x ε
assume hxe: "x ∈ S" "(0 :: real) < ε" "open_ball x ε ∩ U = {}"
then obtain y where
"y ∈ U" "y ∈ S" "dist x y < ε"
using h by blast
hence "y ∈ open_ball x ε ∩ U"
by(auto simp: open_ball_def hxe)
thus False
using hxe(3) by auto
qed(use h in auto)
qed
lemma dense_set_def2':
"dense_set U ⟷ U ⊆ S ∧ (∀x∈S. ∃f∈UNIV → U. converge_to_inS f x)"
unfolding dense_set_def
proof
show "U ⊆ S ∧ (∀x∈S. ∀ε>0. open_ball x ε ∩ U ≠ {}) ⟹ U ⊆ S ∧ (∀x∈S. ∃f∈UNIV → U. converge_to_inS f x)"
proof safe
fix x
assume h: "U ⊆ S" "∀x∈S. ∀ε>0. open_ball x ε ∩ U ≠ {}" "x ∈ S"
then have "⋀n::nat. open_ball x (1 / (real n + 1)) ∩ U ≠ {}"
by auto
hence "∀n. ∃k. k ∈ open_ball x (1 / (real n + 1)) ∩ U" by auto
hence "∃a. ∀n. a n ∈ open_ball x (1 / (real n + 1)) ∩ U" by(rule choice)
then obtain a where hf: "⋀n :: nat. a n ∈ open_ball x (1 / (real n + 1)) ∩ U"
by auto
show "∃f∈UNIV → U. converge_to_inS f x"
unfolding converge_to_inS_def2'
proof(safe intro!: bexI[where x=a])
fix ε :: real
assume he:"0 < ε"
then obtain N where hn: "1 / ε < real N"
using reals_Archimedean2 by blast
have hn': "0 < real N"
by(rule ccontr) (use hn he in fastforce)
hence "1 / real N < ε"
using he hn by (metis divide_less_eq mult.commute)
hence hn'':"1 / (real N + 1) < ε"
using hn' by(auto intro!: order.strict_trans[OF linordered_field_class.divide_strict_left_mono[of "real N" "real N + 1" 1]])
show "∃N. ∀n≥N. a n ∈ open_ball x ε"
proof(safe intro!: exI[where x="N"])
fix n
assume "N ≤ n"
then have 1:"1 / (real n + 1) ≤ 1 / (real N + 1)"
using hn' by(auto intro!: linordered_field_class.divide_left_mono)
show "a n ∈ open_ball x ε"
using open_ball_le[OF 1,of x] open_ball_le[OF order.strict_implies_order[OF hn''],of x] hf[of n]
by auto
qed
next
show "⋀x. a x ∈ S" "x ∈ S" "⋀x. a x ∈ U"
using h(1,3) hf by auto
qed
qed
next
assume h:"U ⊆ S ∧ (∀x∈S. ∃f∈UNIV → U. converge_to_inS f x)"
have "∀x∈S. ∀ε>0. open_ball x ε ∩ U ≠ {}"
proof safe
fix x ε
assume hxe:"x ∈ S" "(0 :: real) < ε" "open_ball x ε ∩ U = {}"
then obtain f N where
"f∈UNIV → U" "∀n≥N :: nat. f n ∈ open_ball x ε"
using h[simplified converge_to_inS_def2'] by blast
hence "f N ∈ open_ball x ε ∩ U"
by auto
thus False using hxe by auto
qed
thus "U ⊆ S ∧ (∀x∈S. ∀ε>0. open_ball x ε ∩ U ≠ {})"
using h by auto
qed
lemma dense_set_infinite:
assumes "infinite S" "dense_set U"
shows "infinite U"
proof
assume finu:"finite U"
with assms(1) obtain x where x:"x ∈ S" "x ∉ U"
by (meson finite_subset subset_iff)
define e where "e ≡ Min {dist x y |y. y ∈ U}"
have nen: "{dist x y |y. y ∈ U} ≠ {}"
using dense_set_empty_iff assms by auto
have fin: "finite {dist x y |y. y ∈ U}"
using finu by auto
have epos: "0 < e"
unfolding Min_gr_iff[OF fin nen] e_def
proof safe
fix y
assume "y ∈ U"
then have "y ∈ S" "x ≠ y"
using assms(2) x(2) by(auto simp: dense_set_def)
thus "0 < dist x y"
using dist_0[OF x(1),of y] dist_geq0[of x y] by auto
qed
then obtain y where y:"y∈U" "dist x y < e"
using assms(2) x(1) by(fastforce simp: dense_set_def2)
thus False
using Min_le[OF fin,of "dist x y"] by(auto simp: e_def)
qed
lemma mtopology_Hausdorff: "Hausdorff_space mtopology"
unfolding Hausdorff_space_def
proof safe
fix x y
assume "x ∈ topspace mtopology" "y ∈ topspace mtopology" "x ≠ y"
then have [simp]:"x ∈ S" "y ∈ S"
using mtopology_topspace by auto
with ‹x ≠ y› have 1:"dist x y > 0"
using dist_0[of x y] dist_geq0[of x y] by auto
show "∃U V. openin mtopology U ∧ openin mtopology V ∧ x ∈ U ∧ y ∈ V ∧ disjnt U V"
proof(rule exI[where x="open_ball x (dist x y/2)"])
show "∃V. openin mtopology (open_ball x (dist x y / 2)) ∧ openin mtopology V ∧ x ∈ open_ball x (dist x y / 2) ∧ y ∈ V ∧ disjnt (open_ball x (dist x y / 2)) V"
proof(safe intro!: exI[where x="open_ball y (dist x y/2)"])
show "disjnt (open_ball x (dist x y / 2)) (open_ball y (dist x y / 2))"
unfolding disjnt_iff
proof safe
fix z
assume h:"z ∈ open_ball x (dist x y / 2)" "z ∈ open_ball y (dist x y / 2)"
show False
using dist_tr[OF ‹x ∈ S› open_ballD'(1)[OF h(1)] ‹y ∈ S›] open_ballD[OF h(1)] open_ballD[OF h(2)]
by (simp add: dist_sym)
qed
qed(auto intro!: mtopology_open_ball_in 1 open_ball_ina)
qed
qed
text ‹ Diameter›
definition diam :: "'a set ⇒ ennreal" where
"diam A ≡ ⨆ {ennreal (dist x y) | x y. x ∈ A ∩ S ∧ y ∈ A ∩ S}"
lemma diam_empty[simp]:
"diam {} = 0"
by(simp add: diam_def bot_ennreal)
lemma diam_def2:
assumes "A ⊆ S"
shows "diam A = ⨆ {ennreal (dist x y) | x y. x ∈ A ∧ y ∈ A}"
using assms by(auto simp: diam_def) (meson subset_eq)
lemma diam_subset:
assumes "A ⊆ B"
shows "diam A ≤ diam B"
unfolding diam_def using assms by(auto intro!: Sup_subset_mono)
lemma diam_cball_leq: "diam (closed_ball a ε) ≤ ennreal (2 * ε)"
unfolding Sup_le_iff diam_def
proof safe
fix x y
assume h:"x ∈ closed_ball a ε" "y ∈ closed_ball a ε" "x ∈ S" "y ∈ S"
have "dist x y ≤ 2 * ε"
using dist_tr[OF h(3) closed_ballD'(2)[OF h(1)] h(4)] closed_ballD[OF h(1),simplified dist_sym[of a x]] closed_ballD[OF h(2)]
by auto
thus "ennreal (dist x y) ≤ ennreal (2 * ε)"
using dist_geq0[of x y] ennreal_leI[of _ "2*ε"] by simp
qed
lemma diam_ball_leq:
"diam (open_ball a ε) ≤ ennreal (2 * ε)"
using diam_subset[OF open_ball_closed_ball[of a ε]] diam_cball_leq[of a ε]
by auto
lemma diam_is_sup:
assumes "x ∈ A ∩ S" "y ∈ A ∩ S"
shows "dist x y ≤ diam A"
using assms by(auto simp: diam_def intro!:Sup_upper)
lemma diam_is_sup':
assumes "x ∈ A ∩ S" "y ∈ A ∩ S" "diam A ≤ ennreal r" "r ≥ 0"
shows "dist x y ≤ r"
using order.trans[OF diam_is_sup[OF assms(1,2)] assms(3)] assms(4) by simp
lemma diam_le:
assumes "⋀x y. x ∈ A ⟹ y ∈ A ⟹ dist x y ≤ r"
shows "diam A ≤ r"
using assms by(auto simp: diam_def Sup_le_iff ennreal_leI)
lemma diam_eq_closure: "diam (mtopology closure_of A) = diam A"
proof(rule antisym)
show "diam A ≤ diam (mtopology closure_of A)"
by(auto intro!: Sup_subset_mono simp: diam_def) (metis in_closure_of mtopology_topspace)
next
have "{ennreal (dist x y) |x y. x ∈ A ∩ S ∧ y ∈ A ∩ S} = ennreal ` {dist x y |x y. x ∈ A ∩ S ∧ y ∈ A ∩ S}"
by auto
also have "diam (mtopology closure_of A) ≤ ⨆ ..."
unfolding le_Sup_iff_less
proof safe
fix r
assume "r < diam (mtopology closure_of A)"
then obtain x y where xy:"x ∈ mtopology closure_of A" "x ∈ S" "y ∈ mtopology closure_of A" "y ∈ S" "r < ennreal (dist x y)"
by(auto simp: diam_def less_Sup_iff)
hence "r < ⊤"
using dual_order.strict_trans ennreal_less_top by blast
define e where "e ≡ (dist x y - enn2real r)/2"
have "e > 0"
using xy(5) ‹r < ⊤› by(simp add: e_def)
then obtain x' y' where xy':"x' ∈ open_ball x e" "x'∈ A" "y' ∈ open_ball y e" "y'∈ A"
using xy by(fastforce simp: closure_of_mtopology)
show "∃i∈{dist x y |x y. x ∈ A ∩ S ∧ y ∈ A ∩ S}. r ≤ ennreal i"
proof(safe intro!: bexI[where x="dist x' y'"])
have "dist x y ≤ dist x x' + dist x' y' + dist y y'"
using dist_tr[OF xy(2) open_ballD'(1)[OF xy'(1)] xy(4)] dist_tr[OF open_ballD'(1)[OF xy'(1)] open_ballD'(1)[OF xy'(3)] xy(4)]
by(simp add: dist_sym)
also have "... < dist x y - enn2real r + dist x' y'"
using open_ballD[OF xy'(1)] open_ballD[OF xy'(3)]
by(simp add: e_def)
finally have "enn2real r < dist x' y'" by simp
thus "r ≤ ennreal (dist x' y')"
by (simp add: ‹r < ⊤›)
qed(use open_ballD'(1)[OF xy'(1)] open_ballD'(1)[OF xy'(3)] xy'(2,4) in auto)
qed
finally show "diam (mtopology closure_of A) ≤ diam A"
by(simp add: diam_def)
qed
definition bounded_set :: "'a set ⇒ bool" where
"bounded_set A ⟷ diam A < ∞"
lemma bounded_set_def2': "bounded_set A ⟷ (∃e. ∀x∈A∩S. ∀y∈A∩S. dist x y < e)"
proof
assume "bounded_set A"
consider "A ∩ S = {}" | "A ∩ S ≠ {}" by auto
then show " ∃e. ∀x∈A ∩ S. ∀y∈A ∩ S. dist x y < e"
proof cases
case h:2
then have 1:"{dist x y |x y. x ∈ A ∩ S ∧ y ∈ A ∩ S} ≠ {}" by auto
have eq:"{ennreal (dist x y) | x y. x ∈ A ∩ S ∧ y ∈ A ∩ S} = ennreal ` {dist x y | x y. x ∈ A ∩ S ∧ y ∈ A ∩ S}"
by auto
hence 2:"diam A = ⨆ (ennreal ` {dist x y | x y. x ∈ A ∩ S ∧ y ∈ A ∩ S})"
by(simp add: diam_def)
obtain x y where hxy:
"x ∈ A ∩ S" "y ∈ A ∩ S" "diam A < ennreal (dist x y) + ennreal 1"
using SUP_approx_ennreal[OF _ 1 2,of 1] ‹bounded_set A›
by(fastforce simp: bounded_set_def)
hence "diam A < ennreal (dist x y + 1)"
using dist_geq0 by simp
from SUP_lessD[OF this[simplified 2]]
have "⋀w z. w ∈ A ∩ S ⟹ z ∈ A ∩ S ⟹ ennreal (dist w z) < ennreal (dist x y + 1)"
by blast
thus "∃e. ∀x∈A ∩ S. ∀y∈A ∩ S. dist x y < e"
by(auto intro!: exI[where x="dist x y + 1"] simp: ennreal_less_iff[OF dist_geq0])
qed simp
next
assume "∃e. ∀x∈A∩S. ∀y∈A∩S. dist x y < e"
then obtain e where he: "⋀x y. x ∈ A ∩ S ⟹ y ∈ A ∩ S ⟹ dist x y < e"
by auto
hence "⋀z. z ∈ {ennreal (dist x y) | x y. x ∈ A ∩ S ∧ y ∈ A ∩ S} ⟹ z < ennreal e"
using ennreal_less_iff[OF dist_geq0] by auto
hence "⨆ {ennreal (dist x y) | x y. x ∈ A ∩ S ∧ y ∈ A ∩ S} ≤ ennreal e"
by (meson Sup_least order_less_le)
thus "bounded_set A"
by(simp add: bounded_set_def diam_def order_le_less_trans[OF _ ennreal_less_top])
qed
lemma bounded_set_def2:
assumes "A ⊆ S"
shows "bounded_set A ⟷ (∃e. ∀x∈A. ∀y∈A. dist x y < e)"
using assms by(fastforce simp: bounded_set_def2')
lemma bounded_set_def3':
assumes "S ≠ {}"
shows "bounded_set A ⟷ (∃e. ∃x∈S. ∀y∈A∩S. dist x y < e)"
unfolding bounded_set_def2'
proof
assume h:"∃e. ∀x∈A ∩ S. ∀y∈A ∩ S. dist x y < e"
obtain s where [simp]:"s ∈ S" using assms by auto
consider "A ∩ S = {}" | "A ∩ S ≠ {}" by auto
then show "∃e. ∃x∈S. ∀y∈A ∩ S. dist x y < e"
proof cases
case 1
then show ?thesis
by(auto intro!: exI[where x=0] exI[where x=s])
next
case 2
then obtain sa where [simp]:"sa ∈ A" "sa ∈ S" by auto
obtain e where "∀x∈A ∩ S. ∀y∈A ∩ S. dist x y < e"
using h by auto
then show ?thesis
by(auto intro!: exI[where x=e] bexI[where x=sa])
qed
next
assume "∃e. ∃x∈S. ∀y∈A ∩ S. dist x y < e"
then obtain e a where
[simp]:"a ∈ S" and hea:"⋀y. y ∈ A ⟹ y ∈ S ⟹ dist a y < e" by auto
show "∃e. ∀x∈A ∩ S. ∀y∈A ∩ S. dist x y < e"
proof(safe intro!: exI[where x="2*e"])
fix x y
assume [simp]:"x ∈ A" "x ∈ S" "y ∈ A" "y ∈ S"
show "dist x y < 2 * e"
using dist_tr[of x a y] hea[of x] hea[of y]
by(simp add: dist_sym[of x a])
qed
qed
lemma bounded_set_def4':
"bounded_set A ⟷ (∃x e. A ∩ S ⊆ open_ball x e)"
proof
assume h:"bounded_set A"
consider "A ∩ S = {}" | "A ∩ S ≠ {}" by auto
then show "∃x e. A ∩ S ⊆ open_ball x e"
proof cases
case 1
then show ?thesis by auto
next
case 2
then have "∃e. ∃x∈S. ∀y∈A∩S. dist x y < e"
using bounded_set_def3' h by blast
then obtain e x where
[simp]: "x ∈ S" and hex: "⋀y. y ∈ A ⟹ y ∈ S ⟹ dist x y < e"
by auto
thus ?thesis
by(auto intro!: exI[where x=x] exI[where x=e] simp:open_ball_def)
qed
next
assume "∃x e. A ∩ S ⊆ open_ball x e"
then obtain a e where hxe:"A ∩ S ⊆ open_ball a e" by auto
show "bounded_set A"
unfolding bounded_set_def2'
proof(safe intro!: exI[where x="2*e"])
fix x y
assume [simp]:"x ∈ A" "x ∈ S" "y ∈ A" "y ∈ S"
then have "x ∈ open_ball a e" "y ∈ open_ball a e"
using hxe by auto
hence "dist a x < e" "dist a y < e" "a ∈ S"
by(auto dest: open_ballD open_ballD')
thus "dist x y < 2 * e"
using dist_tr[of x a y] by(simp add: dist_sym[of x a])
qed
qed
lemma bounded_set_def4:
assumes "A ⊆ S"
shows "bounded_set A ⟷ (∃x e. A ⊆ open_ball x e)"
using bounded_set_def4'[of A] assms by blast
text ‹ Distance between a point and a set. ›
definition dist_set :: "'a set ⇒ 'a ⇒ real" where
"dist_set A ≡ (λx. if A = {} then 0 else Inf {dist x y |y. y ∈ A})"
lemma dist_set_geq0:
"dist_set A x ≥ 0"
proof -
have "{dist x y |y. y ∈ A} = dist x ` A" by auto
thus ?thesis
using dist_geq0[of x] by(auto simp: dist_set_def intro!: cINF_greatest[of _ _ "dist x"])
qed
lemma dist_set_bdd_below[simp]:
"bdd_below {dist x y |y. y ∈ A}"
by(auto simp: bdd_below_def dist_geq0 intro!: exI[where x=0])
lemma dist_set_singleton[simp]:
"dist_set {y} x = dist x y"
by(auto simp: dist_set_def)
lemma dist_set_singleton'[simp]:
"dist_set {y} = (λx. dist x y)"
by auto
lemma dist_set_empty[simp]:
"dist_set {} x = 0"
by(simp add: dist_set_def)
lemma dist_set_nsubset0[simp]:
assumes "¬ (A ⊆ S)"
shows "dist_set A x = 0"
proof -
obtain a where "a ∈ A" "a ∉ S"
using assms by auto
hence "A ≠ {}" "0 ∈ {dist x y |y. y ∈ A}"
using dist_notin'[of a x] by auto
thus ?thesis
using ‹A ≠ {}› dist_set_geq0[of A x] cInf_lower[OF ‹0 ∈ {dist x y |y. y ∈ A}›]
by(auto simp: dist_set_def)
qed
lemma dist_set_notin[simp]:
assumes "x ∉ S"
shows "dist_set A x = 0"
proof -
have "A ≠ {} ⟹ {dist x y |y. y ∈ A} = {0}"
using dist_notin[OF ‹x ∉ S›] by auto
thus ?thesis
by(simp add: dist_set_def)
qed
lemma dist_set_inA:
assumes "x ∈ A"
shows "dist_set A x = 0"
proof(cases "A ⊆ S")
case h:True
hence "A ≠ {}" "0 ∈ {dist x y |y. y ∈ A}"
using dist_0[of x x] assms by force+
thus ?thesis
using cInf_lower[OF ‹0 ∈ {dist x y |y. y ∈ A}›] dist_set_geq0[of A x]
by(auto simp: dist_set_def)
qed (simp add: dist_geq0)
lemma dist_set_nzeroD:
assumes "dist_set A x ≠ 0"
shows "A ⊆ S" "x ∉ A"
by(rule ccontr, use assms dist_set_inA in auto)
lemma dist_set_antimono:
assumes "A ⊆ B" "A ≠ {}"
shows "dist_set B x ≤ dist_set A x"
proof(cases "B = {}")
case h:False
with assms have "{dist x y |y. y ∈ B} ≠ {}" "{dist x y |y. y ∈ A} ⊆ {dist x y |y. y ∈ B}"
by auto
thus ?thesis
by(simp add: dist_set_def cInf_superset_mono assms(2))
qed(use assms in simp)
lemma dist_set_bounded:
assumes "⋀y. y ∈ A ⟹ dist x y < K" "K > 0"
shows "dist_set A x < K"
proof(cases "A = {}")
case True
then show ?thesis
by(simp add: assms)
next
case 1:False
then have 2:"{dist x y |y. y ∈ A} ≠ {}" by auto
show ?thesis
using assms by (auto simp add: dist_set_def cInf_lessD[OF 2] cInf_less_iff[OF 2])
qed
lemma dist_set_tr:
assumes "x ∈ S" "y ∈ S"
shows "dist_set A x ≤ dist x y + dist_set A y"
proof(cases "A ⊆ S")
case h:True
consider "A = {}" | "A ≠ {}" by auto
then show ?thesis
proof cases
case 1
then show ?thesis
by(simp add: dist_set_def dist_geq0)
next
case 2
have "dist_set A x ≤ Inf {dist x y + dist y a |a. a∈A}"
proof -
have "⨅ {dist x y |y. y ∈ A} ≤ ⨅ {dist x y + dist y a |a. a ∈ A}"
proof(rule cInf_mono)
fix b
assume "b ∈ {dist x y + dist y a |a. a ∈ A}"
then obtain a where "a ∈ A" "b = dist x y + dist y a"
by auto
thus "∃a∈{dist x y |y. y ∈ A}. a ≤ b"
using h assms by(auto intro!: exI[where x="dist x a"] dist_tr)
qed(simp_all add: 2)
thus ?thesis
by(simp add: dist_set_def 2)
qed
also have "... = dist x y + Inf {dist y a |a. a∈A}"
proof -
have "ereal (Inf {dist x y + dist y a |a. a∈A}) = ereal (dist x y + Inf {dist y a |a. a∈A})"
(is "?lhs = ?rhs")
proof -
have "?lhs = Inf (ereal ` {(dist x y + dist y a) |a. a∈A})"
using dist_geq0 by(auto intro!: ereal_Inf' bdd_belowI[where m=0] simp: 2)
also have "... = Inf {ereal (dist x y + dist y a) |a. a∈A}"
proof -
have "ereal ` {(dist x y + dist y a) |a. a∈A} = {ereal (dist x y + dist y a) |a. a∈A}"
by auto
thus ?thesis by simp
qed
also have "... = (⨅a∈A. ereal (dist x y) + ereal (dist y a))"
by (simp add: Setcompr_eq_image)
also have "... = ereal (dist x y) + (⨅a∈A. ereal (dist y a))"
by(rule INF_ereal_add_right) (use 2 dist_geq0 in auto)
also have "... = ereal (dist x y) + (⨅ (ereal ` {dist y a | a. a ∈ A}))"
by (simp add: Setcompr_eq_image image_image)
also have "... = ereal (dist x y) + ereal (Inf {dist y a |a. a∈A})"
proof -
have "ereal (Inf {dist y a |a. a∈A}) = (⨅ (ereal ` {dist y a | a. a ∈ A}))"
using dist_geq0 by(auto intro!: ereal_Inf' simp: 2)
thus ?thesis by simp
qed
also have "... = ?rhs" by simp
finally show ?thesis .
qed
thus ?thesis by simp
qed
also have "... = dist x y + dist_set A y"
by(simp add: 2 dist_set_def)
finally show ?thesis .
qed
qed (simp add: dist_geq0)
lemma dist_set_abs_le:
assumes "x ∈ S" "y ∈ S"
shows "¦dist_set A x - dist_set A y¦ ≤ dist x y"
using dist_set_tr[OF assms,of A] dist_set_tr[OF assms(2,1),of A,simplified dist_sym[of y x]]
by auto
lemma dist_set_inA_le:
assumes "y ∈ A"
shows "dist_set A x ≤ dist x y"
proof -
consider "x ∉ S ∨ y ∉ S" | "x ∈ S ∧ y ∈ S" by auto
thus ?thesis
proof cases
case 1
have "y ∉ S ⟹ ¬ (A ⊆ S)"
using assms by auto
with 1 dist_geq0 show ?thesis
by auto
next
case 2
with dist_set_tr[of x y A] dist_set_inA[OF assms]
show ?thesis by simp
qed
qed
lemma dist_set_ball_open:
"openin mtopology {x∈S. dist_set A x < ε}"
unfolding mtopology_openin_iff
proof safe
fix x
assume h:"x ∈ S" "dist_set A x < ε"
show "∃ε'>0. open_ball x ε' ⊆ {x ∈ S. dist_set A x < ε}"
proof(safe intro!: exI[where x="ε - dist_set A x"])
fix y
assume h':"y ∈ open_ball x (ε - dist_set A x)"
have "dist_set A y ≤ dist x y + dist_set A x"
by(rule dist_set_tr[OF open_ballD'(1)[OF h'] h(1),simplified dist_sym[of y x]])
also have "... < ε"
using open_ballD[OF h'] by auto
finally show "dist_set A y < ε" .
qed(use h open_ballD'(1) in auto)
qed
lemma dist_set_ball_empty:
assumes "A ≠ {}" "A ⊆ S" "e > 0" "x ∈ S" "open_ball x e ∩ A = {}"
shows "dist_set A x ≥ e"
using assms by(auto simp: dist_set_def assms(1) le_cInf_iff intro!: open_ball_nin_le[OF assms(4,3)])
lemma dist_set_closed_ge0:
assumes "closedin mtopology A" "A ≠ {}" "x ∈ S" "x ∉ A"
shows "dist_set A x > 0"
proof -
have a:"A ⊆ S" "openin mtopology (S - A)"
using closedin_subset[OF assms(1)] assms(1)
by(auto simp: closedin_def mtopology_topspace)
with assms(3,4) obtain e where e: "e > 0" "open_ball x e ⊆ S - A"
by(auto simp: mtopology_openin_iff) (meson Diff_iff)
thus ?thesis
by(auto intro!: order.strict_trans2[OF e(1) dist_set_ball_empty[OF assms(2) a(1) e(1) assms(3)]])
qed
lemma g_delta_of_closed:
assumes "closedin mtopology M"
shows "g_delta_of mtopology M"
proof(cases "M = {}")
case True
then show ?thesis by simp
next
case M_ne:False
have "M ⊆ S"
using assms mtopology_topspace by (simp add: closedin_def)
define U where "U ≡ (λn. {x∈S. dist_set M x < 1 / real n})"
define 𝒰 where "𝒰 ≡ {U n| n. n > 0}"
have mun:"M ⊆ U n" if "n > 0" for n
using dist_set_inA[of _ M] that ‹M ⊆ S› by(auto simp: U_def)
show ?thesis
proof(rule g_delta_ofI[of "𝒰"])
show "𝒰 ≠ {}"
by(auto simp: 𝒰_def)
next
have "𝒰 = U ` {0<..}" by(auto simp: 𝒰_def)
thus "countable 𝒰" by simp
next
fix b
assume "b ∈ 𝒰"
then show "openin mtopology b"
using dist_set_ball_open by(auto simp: 𝒰_def U_def)
next
show "M = ⋂ 𝒰"
proof(standard;standard)
fix x
assume "x ∈ M"
with mun
show "x ∈ ⋂ 𝒰"
by(auto simp: 𝒰_def)
next
fix x
assume "x ∈ ⋂ 𝒰"
then have "Inf {dist x m|m. m∈M} < 1 / real n" if "n > 0" for n
using that by(auto simp: 𝒰_def U_def M_ne dist_set_def)
hence 1:"Inf {dist x m|m. m∈M} < 1 / real (Suc n)" for n
by blast
have "∃m∈M. dist x m < 1 / real (Suc n)" for n
using 1[of n] cInf_less_iff[of "{dist x m |m. m ∈ M}" "1 / real (Suc n)"] M_ne
by auto
then obtain m where hm: "⋀n. m n ∈ M" "⋀n. dist x (m n) < 1 / real (Suc n)"
by metis
hence "m ∈ UNIV → M" by auto
have "converge_to_inS m x"
unfolding converge_to_inS_def2
proof safe
show "⋀x. m x ∈ S" "x ∈ S"
using ‹x ∈ ⋂ 𝒰› ‹m ∈ UNIV → M› ‹M ⊆ S›
by(auto simp: 𝒰_def U_def)
next
fix ε
assume "(0 :: real) < ε"
then obtain N where hN: "1 / real (Suc N) < ε"
using nat_approx_posE by blast
show "∃N. ∀n≥N. dist (m n) x < ε"
proof(safe intro!: exI[where x=N])
fix n
assume "N ≤ n"
then have "1 / real (Suc n) ≤ 1 / real (Suc N)"
by (simp add: frac_le)
from order.strict_trans1[OF this hN] hm(2)[of n]
show "dist (m n) x < ε"
by(simp add: dist_sym[of x])
qed
qed
thus "x ∈ M"
using assms[simplified mtopology_closedin_iff] ‹m ∈ UNIV → M›
by simp
qed
qed
qed
text ‹ Oscillation›
definition osc_on :: "['b set, 'b topology, 'b ⇒ 'a, 'b] ⇒ ennreal" where
"osc_on A X f ≡ (λy. ⨅ {diam (f ` (A ∩ U)) |U. y ∈ U ∧ openin X U})"
abbreviation "osc X ≡ osc_on (topspace X) X"
lemma osc_def: "osc X f = (λy. ⨅ {diam (f ` U) |U. y ∈ U ∧ openin X U})"
by(standard,auto simp: osc_on_def) (metis (no_types, opaque_lifting) inf.absorb2 openin_subset)
lemma osc_on_less_iff:
"osc_on A X f x < t ⟷ (∃v. x ∈ v ∧ openin X v ∧ diam (f ` (A ∩ v)) < t)"
by(auto simp add: osc_on_def Inf_less_iff)
lemma osc_less_iff:
"osc X f x < t ⟷ (∃v. x ∈ v ∧ openin X v ∧ diam (f ` v) < t)"
by(auto simp add: osc_def Inf_less_iff)
definition sequentially_compact :: bool where
"sequentially_compact ⟷ (∀xn∈sequence. ∃a. strict_mono a ∧ convergent_inS (xn ∘ a))"
definition eps_net_on :: "'a set ⇒ real ⇒ 'a set ⇒ bool" where
"eps_net_on B ε A ⟷ ε > 0 ∧ finite A ∧ A ⊆ S ∧ B ⊆ (⋃a∈A. open_ball a ε)"
abbreviation "eps_net ≡ eps_net_on S"
lemma eps_net_def: "eps_net ε A ⟷ ε > 0 ∧ finite A ∧ A ⊆ S ∧ S = ⋃ ((λa. open_ball a ε) ` A)"
using open_ball_subset_ofS by(auto simp: eps_net_on_def)
lemma eps_net_onD:
assumes "eps_net_on B e A"
shows "e > 0" "finite A" "A ⊆ S" "B ⊆ (⋃a∈A. open_ball a e)" "B ⊆ S"
using assms open_ball_subset_ofS by(auto simp: eps_net_on_def) blast
lemma eps_netD:
assumes "eps_net ε A"
shows "ε > 0" "finite A" "A ⊆ S" "S = ⋃ ((λa. open_ball a ε) ` A)"
using assms by(auto simp: eps_net_def)
lemma eps_net_le:
assumes "eps_net e A" "e ≤ e'"
shows "eps_net e' A"
using assms open_ball_le[OF assms(2)] open_ballD'(1)
by(auto simp: eps_net_def) blast
definition totally_bounded_on :: "'a set ⇒ bool" where
"totally_bounded_on B ⟷ (∀e>0. ∃A. eps_net_on B e A)"
abbreviation "totally_boundedS ≡ totally_bounded_on S"
lemma totally_boundedS_def: "totally_boundedS ⟷ (∀e>0. ∃A. eps_net e A)"
by(auto simp: totally_bounded_on_def)
lemma totally_bounded_onD_sub:
assumes "totally_bounded_on B"
shows "B ⊆ S"
by (meson assms eps_net_onD(5) gt_ex totally_bounded_on_def)
lemma totally_bounded_onD:
assumes "totally_bounded_on B" "e > 0"
obtains A where "finite A" "A ⊆ S" "B ⊆ (⋃a∈A. open_ball a e)"
by (metis assms that eps_net_on_def totally_bounded_on_def)
lemma totally_boundedSD:
assumes totally_boundedS "e > 0"
obtains A where "finite A" "A ⊆ S" "S = (⋃a∈A. open_ball a e)"
by (metis assms that eps_net_def totally_boundedS_def)
lemma totally_bounded_on_iff:
"totally_bounded_on B ⟷ B ⊆ S ∧ (∀xn∈(UNIV :: nat set) → B. ∃a. strict_mono a ∧ Cauchy_inS (xn ∘ a))"
proof safe
fix xn :: "nat ⇒ 'a"
assume h:"totally_bounded_on B" "xn ∈ UNIV → B"
then have h': "B ⊆ S"
by (auto dest: totally_bounded_onD_sub)
have 1: "∃b::nat ⇒ nat. strict_mono b ∧ (∀n m. dist (yn (b n)) (yn (b m)) < e)" if "yn ∈ UNIV → B" "e > 0" for e yn
proof -
obtain A where A: "finite A" "A ⊆ S" "B ⊆ (⋃a∈A. open_ball a (e/2))"
using totally_bounded_onD[OF h(1) half_gt_zero[OF ‹e > 0›]] by metis
have "¬ (∀a∈A. finite {n. yn n ∈ open_ball a (e/2)})"
proof
assume "∀a∈A. finite {n. yn n ∈ open_ball a (e/2)}"
then have "finite (⋃a∈A. {n. yn n ∈ open_ball a (e/2)})"
using A by auto
moreover have "UNIV = (⋃a∈A. {n. yn n ∈ open_ball a (e/2)})"
using that(1) A(3) by auto
ultimately show False by simp
qed
then obtain a where a:"a ∈ A" "infinite {n. yn n ∈ open_ball a (e/2)}"
by auto
then obtain b where b:"strict_mono b" "⋀n::nat. yn (b n) ∈ open_ball a (e/2)"
using obtain_subsequence[of "λ_ ynn. ynn ∈ open_ball a (e/2)" yn] by auto
show ?thesis
using a A by(auto intro!: exI[where x=b] b order.strict_trans1[OF dist_tr[OF open_ballD'(1)[OF b(2)] _ open_ballD'(1)[OF b(2)],of a] add_strict_mono[OF open_ballD[OF b(2),simplified dist_sym[of a]] open_ballD[OF b(2)]],simplified])
qed
define anm where "anm ≡ rec_nat (xn ∘ (SOME b::nat ⇒ nat. strict_mono b ∧ (∀n m. dist (xn (b n)) (xn (b m)) < 1))) (λn an. an ∘ (SOME b. strict_mono b ∧ (∀l k. dist (an (b l)) (an (b k)) < 1 / Suc (Suc n))))"
have anm_Suc:"anm (Suc n) = anm n ∘ (SOME b. strict_mono b ∧ (∀l k. dist (anm n (b l)) (anm n (b k)) < 1 / Suc (Suc n)))" for n
by(simp add: anm_def)
have anm1:"anm n ∈ UNIV → B ∧ (∀l k. dist (anm n l) (anm n k) < 1 / Suc n)" for n
proof(induction n)
case 0
obtain b ::"nat ⇒ nat" where b:"strict_mono b" "∀l k. dist (xn (b l)) (xn (b k)) < 1"
using 1[OF h(2),of 1] by auto
show ?case
by(simp add: anm_def,rule someI2[where a=b]) (use b h(2) in auto)
next
case ih:(Suc n')
obtain b ::"nat ⇒ nat" where b:"strict_mono b" "∀l k. dist (anm n' (b l)) (anm n' (b k)) < 1 / real (Suc (Suc n'))"
using 1[of "anm n'" "1 / Suc (Suc n')"] ih by auto
show ?case
by(simp only: anm_Suc,rule someI2[where a=b]) (use ih b in auto)
qed
define bnm :: "nat ⇒ nat ⇒ nat" where "bnm ≡ rec_nat (SOME b. strict_mono b ∧ anm 0 = xn ∘ b) (λn bn. SOME b. strict_mono b ∧ anm (Suc n) = anm n ∘ b)"
have bnm_Suc:"bnm (Suc n) = (SOME b. strict_mono b ∧ anm (Suc n) = anm n ∘ b)" for n
by(simp add: bnm_def)
have bnm0:"strict_mono (bnm 0) ∧ anm 0 = xn ∘ (bnm 0)"
proof -
have b0:"∃b::nat ⇒ nat. strict_mono b ∧ anm 0 = xn ∘ b"
proof -
obtain b ::"nat ⇒ nat" where b:"strict_mono b" "∀l k. dist (xn (b l)) (xn (b k)) < 1"
using 1[OF h(2),of 1] by auto
show ?thesis
by(simp add: anm_def,rule someI2[where a=b],auto simp: b)
qed
thus ?thesis
unfolding bnm_def by(simp,rule someI_ex)
qed
have bnm_S: "strict_mono (bnm (Suc n)) ∧ anm (Suc n) = anm n ∘ (bnm (Suc n))" for n
proof -
have bn:"∃b::nat ⇒ nat. strict_mono b ∧ anm (Suc m) = anm m ∘ b" for m
proof -
obtain b ::"nat ⇒ nat" where b:"strict_mono b" "∀l k. dist (anm m (b l)) (anm m (b k)) < 1 / real (Suc (Suc m))"
using 1[of "anm m" "1 / Suc (Suc m)"] anm1 by auto
show ?thesis
by(simp only: anm_Suc,rule someI2[where a=b]) (auto simp: b[simplified])
qed
thus ?thesis
by(simp add: bnm_Suc, rule someI_ex)
qed
define bnm_r where "bnm_r ≡ rec_nat (bnm 0) (λn bn. bn ∘ (bnm (Suc n)))"
have bnm_r_Suc: "bnm_r (Suc n) = bnm_r n ∘ (bnm (Suc n))" for n
by(simp add: bnm_r_def)
have anm_bnm_r:"anm n = xn ∘ (bnm_r n)" for n
by(induction n,simp add: bnm0 bnm_r_def) (auto simp: bnm_S bnm_r_Suc)
have bnm_r_sm:"strict_mono (bnm_r n)" for n
by(induction n, simp add: bnm0 bnm_r_def) (insert bnm_S, auto simp: bnm_r_Suc strict_mono_def)
have bnm_r_Suc_le:"bnm_r n l ≤ bnm_r (Suc n) l" for l n
using bnm_S bnm_r_sm by(auto simp: bnm_r_Suc strict_mono_imp_increasing strict_mono_leD)
have sm:"strict_mono (λn. bnm_r n n)"
by(auto simp add: strict_mono_Suc_iff) (meson lessI order_le_less_trans strict_monoD bnm_r_sm bnm_r_Suc_le)
have bnm_r_de:"∃l. bnm_r (n + k) = bnm_r n ∘ l" for n k
by(induction k) (auto simp: bnm_r_Suc)
show "∃a::nat ⇒ nat. strict_mono a ∧ Cauchy_inS (xn ∘ a)"
unfolding Cauchy_inS_def
proof(safe intro!: exI[where x="λn. bnm_r n n"] sm)
fix e :: real
assume "e > 0"
then obtain N where N:"1 / Suc N < e"
using nat_approx_posE by blast
show "∃N. ∀n≥N. ∀m≥N. dist ((xn ∘ (λn. bnm_r n n)) n) ((xn ∘ (λn. bnm_r n n)) m) < e"
proof(safe intro!: exI[where x=N])
fix n m
assume "N ≤ n" "N ≤ m"
then have "n = N + (n - N)" "m = N + (m - N)" by auto
then obtain l1 l2 where l:"bnm_r n = bnm_r N ∘ l1" "bnm_r m = bnm_r N ∘ l2"
by (metis bnm_r_de)
have "dist (xn (bnm_r n n)) (xn (bnm_r m m)) = dist (anm N (l1 n)) (anm N (l2 m))"
by(simp add: l anm_bnm_r)
also have "... < 1 / Suc N"
using anm1 by auto
finally show "dist ((xn ∘ (λn. bnm_r n n)) n) ((xn ∘ (λn. bnm_r n n)) m) < e"
using N by simp
qed
qed(use h h' in auto)
next
assume h:"∀xn∈(UNIV :: nat set) → B. ∃a. strict_mono a ∧ Cauchy_inS (xn ∘ a)" "B ⊆ S"
show "totally_bounded_on B"
proof(rule ccontr)
assume "¬ totally_bounded_on B"
then obtain e where e:"e > 0" "⋀A. ¬ eps_net_on B e A"
by(auto simp: totally_bounded_on_def)
have A:"¬ B ⊆ (⋃a∈A. open_ball a e)" if "finite A" for A
proof -
have [simp]:"(⋃a∈A. open_ball a e) = (⋃a∈A∩ S. open_ball a e)"
using Collect_cong IntD1 IntI Sup_set_def UN_iff open_ballD'(2) by auto
have "finite (A ∩ S)" using that by auto
thus ?thesis
using e by(auto simp: eps_net_on_def)
qed
obtain a0 where a0:"a0 ∈ B"
using A by fastforce
define xnl where "xnl ≡ rec_nat [a0] (λn ln. (SOME x. x ∈ B ∧ x ∉ (⋃a∈set ln. open_ball a e)) # ln)"
have xnl_Suc:"xnl (Suc n) = (SOME x. x ∈ B ∧ x ∉ (⋃a∈set (xnl n). open_ball a e)) # xnl n" for n
by(simp add: xnl_def)
define xn where "xn = (λn. (xnl n) ! 0)"
have xn:"xn (Suc n) ∈ B ∧ xn (Suc n) ∉ (⋃a∈set (xnl n). open_ball a e)" for n
proof -
have "∃y. y ∈ B ∧ (∀x∈set (xnl n). y ∉ open_ball x e)"
using A[OF finite_set] by fastforce
thus ?thesis
by(simp add: xn_def xnl_Suc,rule someI_ex)
qed
have xn0:"xn 0 ∈ B"
by(auto simp: xnl_def xn_def a0)
with xn have xns:"xn ∈ UNIV → B"
by auto (metis old.nat.exhaust)
have xnll:"length (xnl n) = Suc n" for n
by(induction n) (simp add: xnl_def, auto simp: xnl_Suc)
have xnin:"xn m ∈ set (xnl (m + k))" for m k
by(induction k) (auto simp: xn_def xnl_Suc xnll intro!: nth_mem)
obtain a where a:"strict_mono a" "Cauchy_inS (xn ∘ a)"
using h xns by auto
then obtain N where "⋀n m. n ≥ N ⟹ m ≥ N ⟹ dist (xn (a n)) (xn (a m)) < e"
using e Cauchy_inS_def by fastforce
hence e1:"dist (xn (a N)) (xn (a (Suc N))) < e"
by auto
have "xn (a (Suc N)) ∉ (⋃a∈set (xnl (a (Suc N) - 1)). open_ball a e)"
by (metis a(1) diff_Suc_1 le_0_eq not0_implies_Suc strict_mono_less_eq xn zero_le)
moreover have "xn (a N) ∈ set (xnl (a (Suc N) - 1))"
using a(1)[simplified strict_mono_Suc_iff] xnin[of "a N" "a (Suc N) - a N - 1"]
by (simp add: Suc_leI)
ultimately have "xn (a (Suc N)) ∉ open_ball (xn (a N)) e"
by auto
from open_ball_nin_le[OF _ e(1) _ this] xns e1 h(2)
show False by auto
qed
qed(auto dest: totally_bounded_onD_sub)
corollary totally_boundedS_iff: "totally_boundedS ⟷ (∀xn∈sequence. ∃a. strict_mono a ∧ Cauchy_inS (xn ∘ a))"
by(auto simp: totally_bounded_on_iff)
text ‹ Metric embedding›
definition embed_dist_on :: "['b set, 'b ⇒ 'a, 'b, 'b] ⇒ real" where
"embed_dist_on B f a b ≡ (if a ∈ B ∧ b ∈ B then dist (f a) (f b) else 0)"
context
fixes f B
assumes f: "f ∈ B → S" "inj_on f B"
begin
abbreviation "ed ≡ embed_dist_on B f"
lemma embed_dist_dist: "metric_set B (embed_dist_on B f)"
proof
fix x y
assume "x ∈ B" "y ∈ B"
then show "x = y ⟷ embed_dist_on B f x y = 0"
using inj_onD[OF f(2)] dist_0[of "f x" "f y"] f(1)
by(auto simp: embed_dist_on_def)
next
fix x y
show "embed_dist_on B f x y = embed_dist_on B f y x"
by(simp add: embed_dist_on_def dist_sym[of "f x" "f y"])
next
fix x y z
assume "x ∈ B" "y ∈ B" "z ∈ B"
then show "embed_dist_on B f x z ≤ embed_dist_on B f x y + embed_dist_on B f y z"
using dist_tr[of "f x" "f y" "f z"] f(1) by(auto simp: embed_dist_on_def)
qed(simp_all add: embed_dist_on_def dist_geq0)
interpretation ed : metric_set B ed
by(rule embed_dist_dist)
lemma embed_dist_open_ball:
assumes "a ∈ B"
shows"f ` (ed.open_ball a e) = open_ball (f a) e ∩ f ` B"
using assms f by(auto simp: ed.open_ball_def open_ball_def embed_dist_on_def)
lemma embed_dist_closed_ball:
assumes "a ∈ B"
shows"f ` (ed.closed_ball a e) = closed_ball (f a) e ∩ f ` B"
using assms f by(auto simp: ed.closed_ball_def closed_ball_def embed_dist_on_def)
lemma embed_dist_topology_homeomorphic_maps:
assumes g1:"⋀x. x ∈ B ⟹ g (f x) = x"
shows "homeomorphic_maps ed.mtopology (subtopology mtopology (f ` B)) f g"
proof -
have g2: "⋀x. x ∈ f ` B ⟹ f (g x) = x" "g ∈ (f ` B) → B"
by(auto simp: g1)
show ?thesis
unfolding homeomorphic_maps_def mtopology_topspace ed.mtopology_topspace
proof safe
show "continuous_map ed.mtopology (subtopology mtopology (f ` B)) f"
unfolding mtopology_def2 subtopology_generated_by
proof(rule continuous_on_generated_topo)
show "⋀U. U ∈ {f ` B ∩ U |U. U ∈ {open_ball a ε |a ε. a ∈ S ∧ 0 < ε}} ⟹ openin ed.mtopology (f -` U ∩ topspace ed.mtopology)"
unfolding ed.mtopology_topspace
proof safe
fix a and e :: real
assume h:"a ∈ S" "0 < e"
have 1:"(f -` (f ` B ∩ open_ball a e) ∩ B) = f -` open_ball a e ∩ B" by blast
show "openin ed.mtopology (f -` (f ` B ∩ open_ball a e) ∩ B)"
unfolding 1 ed.mtopology_openin_iff
proof safe
fix x
assume h':"x ∈ B" "f x ∈ open_ball a e"
then obtain e' where e':"e' > 0" "open_ball (f x) e' ⊆ open_ball a e"
using mtopology_open_ball_in' by blast
show "∃ε>0. ed.open_ball x ε ⊆ f -` open_ball a e ∩ B"
proof(safe intro!: exI[where x=e'])
fix y
assume "y ∈ ed.open_ball x e'"
with e'(2) show "y ∈ f -` open_ball a e"
using embed_dist_open_ball[OF h'(1),of e'] by blast
qed(use e' ed.open_ball_subset_ofS in auto)
qed
qed
next
show "f ` topspace ed.mtopology ⊆ ⋃ {f ` B ∩ U |U. U ∈ {open_ball a ε |a ε. a ∈ S ∧ 0 < ε}} "
by(auto simp: ed.mtopology_topspace) (metis (mono_tags, opaque_lifting) IntE IntI closed_ball_def ed.closed_ball_ina ed.dist_set_geq0 ed.dist_set_inA embed_dist_closed_ball ennreal_le_epsilon ennreal_zero_less_top image_eqI le_zero_eq not_gr_zero open_ballD'(2) open_ball_ina open_ball_le_0)
qed
next
show "continuous_map (subtopology mtopology (f ` B)) ed.mtopology g"
unfolding ed.mtopology_def2
proof(rule continuous_on_generated_topo)
show "⋀U. U ∈ {ed.open_ball a ε |a ε. a ∈ B ∧ 0 < ε} ⟹ openin (subtopology mtopology (f ` B)) (g -` U ∩ topspace (subtopology mtopology (f ` B)))"
proof safe
fix a and e :: real
assume h: "a ∈ B" "0 < e"
then have 1: "g -` ed.open_ball a e ∩ (S ∩ f ` B) = open_ball (f a) e ∩ f ` B"
using f(1) g1 g2 by(auto simp: ed.open_ball_def open_ball_def embed_dist_on_def)
show "openin (subtopology mtopology (f ` B)) (g -` ed.open_ball a e ∩ (topspace (subtopology mtopology (f ` B))))"
by(auto simp: 1 openin_subtopology openin_open_ball mtopology_topspace intro!: exI[where x="open_ball (f a) e"])
qed
show "g ` topspace (subtopology mtopology (f ` B)) ⊆ ⋃ {ed.open_ball a ε |a ε. a ∈ B ∧ 0 < ε}"
by(auto simp: mtopology_topspace) (metis ed.mtopology_openin_iff ed.open_ball_ina ed.openin_S g1)
qed
qed(use g1 g2 in auto)
qed
lemma embed_dist_topology_homeomorphic_map:
"homeomorphic_map ed.mtopology (subtopology mtopology (f ` B)) f"
proof -
define g where "g ≡ (λy. THE x. x ∈ B ∧ f x = y)"
have g1: "g (f b) = b" if "b ∈ B" for b
unfolding g_def by(rule theI2[of _ b]) (insert that f(2), auto simp: inj_on_def)
thus ?thesis
using embed_dist_topology_homeomorphic_maps homeomorphic_map_maps by blast
qed
corollary embed_dist_topology_homeomorphic:
"ed.mtopology homeomorphic_space (subtopology mtopology (f ` B))"
using embed_dist_topology_homeomorphic_map
by(rule homeomorphic_map_imp_homeomorphic_space)
corollary embed_dist_topology_homeomorphic_map':
assumes "f ` B = S"
shows "homeomorphic_map ed.mtopology mtopology f"
using embed_dist_topology_homeomorphic_map[simplified assms]
by(simp add:subtopology_topspace[of mtopology, simplified mtopology_topspace])
corollary embed_dist_topology_homeomorphic':
assumes "f ` B = S"
shows "ed.mtopology homeomorphic_space mtopology"
using embed_dist_topology_homeomorphic_map'[OF assms]
by(rule homeomorphic_map_imp_homeomorphic_space)
lemma embed_dist_converge_to_inS_iff:
"ed.converge_to_inS xn x ⟷ xn ∈ ed.sequence ∧ x ∈ B ∧ converge_to_inS (λn. f (xn n)) (f x)"
proof safe
assume h:"ed.converge_to_inS xn x"
then show h':"x ∈ B" "⋀n. xn n ∈ B"
by(auto simp: ed.converge_to_inS_def)
thus "converge_to_inS (λn. f (xn n)) (f x)"
using h f by(auto simp: converge_to_inS_def2 ed.converge_to_inS_def2 embed_dist_on_def)
next
assume h:"xn ∈ ed.sequence" "x ∈ B" "converge_to_inS (λn. f (xn n)) (f x)"
show "ed.converge_to_inS xn x"
using h f by(fastforce simp: ed.converge_to_inS_def2 h embed_dist_on_def converge_to_inS_def2)
qed
lemma embed_dist_convergent_inS_iff:
assumes "closedin mtopology (f ` B)"
shows "ed.convergent_inS xn ⟷ xn ∈ ed.sequence ∧ convergent_inS (λn. f (xn n))"
proof -
{
fix s
assume h:"xn ∈ ed.sequence" "converge_to_inS (λn. f (xn n)) s"
with f have "(λn. f (xn n)) ∈ UNIV → f ` B" by auto
hence "s ∈ f ` B"
using assms h(2) by(auto simp: mtopology_closedin_iff)
hence "∃b ∈ B. s = f b" by auto
}
thus ?thesis
using embed_dist_converge_to_inS_iff[of xn] f(1)
by(fastforce simp: ed.convergent_inS_def convergent_inS_def)
qed
lemma embed_dist_Cauchy_inS_iff:
"ed.Cauchy_inS xn ⟷ xn ∈ ed.sequence ∧ Cauchy_inS (λn. f (xn n))"
using f(1) by(auto simp: ed.Cauchy_inS_def Cauchy_inS_def embed_dist_on_def; meson PiE UNIV_I)
end
end
text ‹ Relations to elementary topology. ›
lemma ball_def_set: "ball a ε = metric_set.open_ball UNIV dist a ε"
using metric_set.open_ball_def metric_class_metric_set
by fastforce
lemma converge_to_def_set:
fixes xn :: "nat ⇒ ('a::metric_space)"
shows "xn ⇢ x ⟷ metric_set.converge_to_inS UNIV dist xn x"
proof -
interpret m: metric_set UNIV dist
by simp
show ?thesis
by(simp add: lim_sequentially m.converge_to_inS_def)
qed
lemma the_limit_of_limit:
fixes xn :: "nat ⇒ ('a::metric_space)"
shows "metric_set.the_limit_of UNIV dist xn = lim xn"
by(simp add: metric_set.the_limit_of_def lim_def converge_to_def_set)
lemma convergent_def_set:
fixes f :: "nat ⇒ ('a::metric_space)"
shows "convergent f ⟷ metric_set.convergent_inS UNIV dist f"
proof -
interpret m: metric_set UNIV dist
by(rule metric_class_metric_set)
show "convergent f ⟷ m.convergent_inS f"
using converge_to_def_set[of f]
by(auto simp: convergent_def m.convergent_inS_def)
qed
lemma Cahuchy_def_set: "Cauchy f ⟷ metric_set.Cauchy_inS UNIV dist f"
proof -
interpret m: metric_set UNIV dist
by(rule metric_class_metric_set)
show "Cauchy f = m.Cauchy_inS f"
by(simp add: Cauchy_def m.Cauchy_inS_def dist_real_def)
qed
lemma open_openin_set: "open U ⟷ openin (metric_set.mtopology UNIV dist) U"
(is "?LHS ⟷ ?RHS")
proof -
interpret m: metric_set UNIV dist
by(rule metric_class_metric_set)
have "?LHS ⟷ (∀x∈U. ∃e>0. ball x e ⊆ U)"
by(simp add: open_contains_ball)
also have "... ⟷ (∀x∈U. ∃e>0. m.open_ball x e ⊆ U)"
by(simp add: ball_def_set)
also have "... ⟷ ?RHS"
by(simp add: m.mtopology_openin_iff[of U])
finally show ?thesis .
qed
lemma topological_basis_set: "topological_basis 𝒪 ⟷ metric_set.mtopology_basis UNIV dist 𝒪"
(is "?LHS = ?RHS")
proof -
interpret m: metric_set UNIV dist
by(rule metric_class_metric_set)
have "?LHS ⟷ (∀b∈𝒪. open b) ∧ (∀x. open x ⟶ (∃B'⊆𝒪. ⋃ B' = x))"
by(simp add: topological_basis_def)
also have "... ⟷ (∀b∈𝒪. openin m.mtopology b) ∧ (∀x. openin m.mtopology x ⟶ (∃B'⊆𝒪. ⋃ B' = x))"
by(simp add: open_openin_set)
also have "... ⟷ ?RHS"
by(simp add: base_of_def2')
finally show ?thesis .
qed
lemma euclidean_mtopology: "metric_set.mtopology UNIV dist = euclidean"
using open_openin open_openin_set topology_eq by blast
text ‹ Distances generate the same topological space.›
lemma metric_generates_same_topology:
assumes "metric_set S d" "metric_set S d'"
"⋀x U. U ⊆ S ⟹ (∀y∈U. ∃ε>0. metric_set.open_ball S d y ε ⊆ U) ⟹ x ∈ U ⟹ ∃ε>0. metric_set.open_ball S d' x ε ⊆ U"
and "⋀x U. U ⊆ S ⟹ (∀y∈U. ∃ε>0. metric_set.open_ball S d' y ε ⊆ U) ⟹ x ∈ U ⟹ ∃ε>0. metric_set.open_ball S d x ε ⊆ U"
shows "metric_set.mtopology S d = metric_set.mtopology S d'"
proof -
interpret m1: metric_set S d by fact
interpret m2: metric_set S d' by fact
have "(λU. U ⊆ S ∧ (∀x∈U. ∃ε>0. m1.open_ball x ε ⊆ U)) = (λU. U ⊆ S ∧ (∀x∈U. ∃ε>0. m2.open_ball x ε ⊆ U))"
by standard (use assms(3,4) in auto)
thus ?thesis
using topology.topology_inject m1.mtopology_istopology m2.mtopology_istopology
by(simp add: m2.mtopology_def m1.mtopology_def)
qed
lemma metric_generates_same_topology_inverse:
assumes "metric_set S d" "metric_set S d'"
and "metric_set.mtopology S d = metric_set.mtopology S d'"
shows "U ⊆ S ⟹ (∀y∈U. ∃ε>0. metric_set.open_ball S d y ε ⊆ U) ⟹ x ∈ U ⟹ ∃ε>0. metric_set.open_ball S d' x ε ⊆ U"
and "U ⊆ S ⟹ (∀y∈U. ∃ε>0. metric_set.open_ball S d' y ε ⊆ U) ⟹ x ∈ U ⟹ ∃ε>0. metric_set.open_ball S d x ε ⊆ U"
proof -
interpret m1: metric_set S d by fact
interpret m2: metric_set S d' by fact
have "(λU. U ⊆ S ∧ (∀x∈U. ∃ε>0. m1.open_ball x ε ⊆ U)) = (λU. U ⊆ S ∧ (∀x∈U. ∃ε>0. m2.open_ball x ε ⊆ U))"
using topology.topology_inject[of "λU. U ⊆ S ∧ (∀x∈U. ∃ε>0. m1.open_ball x ε ⊆ U)" "λU. U ⊆ S ∧ (∀x∈U. ∃ε>0. m2.open_ball x ε ⊆ U)"] m1.mtopology_istopology m2.mtopology_istopology assms(3)
by(auto simp: m2.mtopology_def m1.mtopology_def)
thus "U ⊆ S ⟹ ∀y∈U. ∃ε>0. m1.open_ball y ε ⊆ U ⟹ x ∈ U ⟹ ∃ε>0. m2.open_ball x ε ⊆ U"
"U ⊆ S ⟹ ∀y∈U. ∃ε>0. m2.open_ball y ε ⊆ U ⟹ x ∈ U ⟹ ∃ε>0. m1.open_ball x ε ⊆ U"
by(auto dest: fun_cong[where x=U])
qed
lemma metric_generates_same_topology_converges':
assumes "metric_set S d" "metric_set S d'"
"metric_set.mtopology S d = metric_set.mtopology S d'"
and "metric_set.converge_to_inS S d f x"
shows "metric_set.converge_to_inS S d' f x"
proof -
interpret m1: metric_set S d by fact
interpret m2: metric_set S d' by fact
show ?thesis
unfolding m2.converge_to_inS_def2'
proof safe
fix ε :: real
assume h:"0 < ε"
obtain ε' where he:
"ε'>0" "m1.open_ball x ε' ⊆ m2.open_ball x ε"
using m2.mtopology_open_ball_in'[of _ x] assms(4)[simplified m1.converge_to_inS_def2'] metric_generates_same_topology_inverse(2)[OF assms(1-3) m2.open_ball_subset_ofS, of x ε,OF _ m2.open_ball_ina[OF _ h,of x]]
by auto
then obtain N where hn:
"∀n≥N. f n ∈ m1.open_ball x ε'"
using assms(4)[simplified m1.converge_to_inS_def2'] by auto
show "∃N. ∀n≥N. f n ∈ m2.open_ball x ε"
using hn he(2) by(auto intro!: exI[where x=N])
next
show "⋀x. f x ∈ S" "x ∈ S"
using assms(4)[simplified m1.converge_to_inS_def2'] by auto
qed
qed
lemma metric_generates_same_topology_converges:
assumes "metric_set S d" "metric_set S d'"
and "metric_set.mtopology S d = metric_set.mtopology S d'"
shows "metric_set.converge_to_inS S d f x ⟷ metric_set.converge_to_inS S d' f x"
using metric_generates_same_topology_converges'[OF assms(2,1) assms(3)[symmetric]] metric_generates_same_topology_converges'[OF assms(1-3)]
by auto
lemma metric_generates_same_topology_convergent:
assumes "metric_set S d" "metric_set S d'"
and "metric_set.mtopology S d = metric_set.mtopology S d'"
shows "metric_set.convergent_inS S d f ⟷ metric_set.convergent_inS S d' f"
using metric_generates_same_topology_converges[OF assms,of f]
by (simp add: assms(1) assms(2) metric_set.convergent_inS_def)
subsubsection ‹ Sub-Metric Spaces›
definition submetric :: "['a set, 'a ⇒ 'a ⇒ real] ⇒ 'a ⇒ 'a ⇒ real" where
"submetric S' d ≡ (λx y. if x ∈ S' ∧ y ∈ S' then d x y else 0)"
lemma(in metric_set) submetric_metric_set:
assumes "S' ⊆ S"
shows "metric_set S' (submetric S' dist)"
proof
show "⋀x y. 0 ≤ submetric S' dist x y"
"⋀x y. x ∉ S' ⟹ submetric S' dist x y = 0"
"⋀x y. x ∈ S' ⟹ y ∈ S' ⟹ (x = y) = (submetric S' dist x y = 0)"
"⋀x y. submetric S' dist x y = submetric S' dist y x"
using assms dist_geq0 dist_tr dist_0 dist_sym
by(fastforce simp: submetric_def)+
next
show "⋀x y z. x ∈ S' ⟹ y ∈ S' ⟹ z ∈ S' ⟹ submetric S' dist x z ≤ submetric S' dist x y + submetric S' dist y z"
by (metis assms dist_tr submetric_def subset_iff)
qed
lemma(in metric_set) submetric_open_ball:
assumes "S' ⊆ S" and "a ∈ S'"
shows "open_ball a ε ∩ S' = metric_set.open_ball S' (submetric S' dist) a ε"
proof -
interpret m: metric_set S' "submetric S' dist"
by(rule submetric_metric_set[OF assms(1)])
show ?thesis
using assms by(auto simp: open_ball_def m.open_ball_def,simp_all add: submetric_def)
qed
lemma(in metric_set) submetric_open_ball_subset:
assumes "S' ⊆ S"
shows "metric_set.open_ball S' (submetric S' dist) a ε ⊆ open_ball a ε"
proof -
interpret m: metric_set S' "submetric S' dist"
by(rule submetric_metric_set[OF assms(1)])
show ?thesis
by (metis assms empty_subsetI inf_commute inf_sup_ord(2) m.open_ball_nin submetric_open_ball)
qed
lemma(in metric_set) submetric_subtopology:
assumes "S' ⊆ S"
shows "subtopology mtopology S' = metric_set.mtopology S' (submetric S' dist)"
proof -
interpret m: metric_set S' "submetric S' dist"
by(rule submetric_metric_set[OF assms(1)])
show ?thesis
unfolding topology_eq
proof safe
fix U
assume "openin (subtopology mtopology S') U"
then obtain T where ht: "openin mtopology T" "U = T ∩ S'"
by(auto simp: openin_subtopology)
have "U ⊆ S'"
by (simp add: ht(2))
show "openin m.mtopology U"
unfolding m.mtopology_openin_iff
proof safe
fix x
assume "x ∈ U"
then obtain ε where he: "ε > 0" "open_ball x ε ⊆ T"
using ht by(auto simp: mtopology_openin_iff)
thus "∃ε>0. m.open_ball x ε ⊆ U"
using ht(2) ‹x ∈ U› submetric_open_ball[OF assms(1),of x ε]
by(auto intro!: exI[where x=ε])
qed(use ‹U ⊆ S'› in auto)
next
fix U
assume "openin m.mtopology U"
then have "∀x∈U. ∃ε>0. m.open_ball x ε ⊆ U"
by(simp add: m.mtopology_openin_iff)
then obtain ε where he:
"⋀x. x ∈ U ⟹ ε x > 0" "⋀x. x ∈ U ⟹ m.open_ball x (ε x) ⊆ U"
by metis
have "U ⊆ S'"
using ‹openin m.mtopology U› m.mtopology_openin_iff by auto
show "openin (subtopology mtopology S') U"
unfolding openin_subtopology
proof(intro exI[where x="⋃ { open_ball x (ε x) | x. x∈U}"] conjI)
show "openin mtopology (⋃ { open_ball x (ε x) | x. x∈U})"
by(rule openin_Union) (use he(1) open_ball_def mtopology_open_ball_in in fastforce)
next
have *:"U = (⋃ { m.open_ball x (ε x) | x. x∈U})"
using he m.open_ball_ina ‹U ⊆ S'› by fastforce
also have "... = (⋃ { open_ball x (ε x) ∩ S' | x. x∈U})"
using submetric_open_ball[OF assms(1)] ‹U ⊆ S'› by auto
also have "... = (⋃ { open_ball x (ε x) | x. x∈U}) ∩ S'"
by auto
finally show "U = ⋃ {open_ball x (ε x) |x. x ∈ U} ∩ S' " .
qed
qed
qed
lemma(in metric_set) converge_to_insub_converge_to_inS:
assumes "S' ⊆ S" and "metric_set.converge_to_inS S' (submetric S' dist) f x"
shows "converge_to_inS f x"
proof -
interpret m: metric_set S' "submetric S' dist"
by(rule submetric_metric_set[OF assms(1)])
have *:"f ∈ m.sequence" "x ∈ S'"
using assms(2) by(auto simp: m.converge_to_inS_def)
show ?thesis
unfolding converge_to_inS_def2 using * assms[simplified m.converge_to_inS_def2]
by(auto simp: submetric_def funcset_mem)
qed
lemma(in metric_set) convergent_insub_convergent_inS:
assumes "S' ⊆ S" and "metric_set.convergent_inS S' (submetric S' dist) f"
shows "convergent_inS f"
by (meson assms(1) assms(2) converge_to_insub_converge_to_inS convergent_inS_def in_mono metric_set.convergent_inS_def submetric_metric_set)
lemma(in metric_set) Cauchy_insub_Cauchy:
assumes "S' ⊆ S" and "metric_set.Cauchy_inS S' (submetric S' dist) f"
shows "Cauchy_inS f"
proof -
interpret m: metric_set S' "submetric S' dist"
by(rule submetric_metric_set[OF assms(1)])
have *:"f ∈ m.sequence"
using assms(2) by(auto simp: m.Cauchy_inS_def)
show ?thesis
unfolding Cauchy_inS_def using * assms[simplified m.Cauchy_inS_def]
by(auto simp: submetric_def funcset_mem[OF *])
qed
lemma(in metric_set) Cauchy_insub_Cauchy_inverse:
assumes "S' ⊆ S" "f ∈ UNIV → S'" "Cauchy_inS f"
shows "metric_set.Cauchy_inS S' (submetric S' dist) f"
proof -
interpret m: metric_set S' "submetric S' dist"
by(rule submetric_metric_set[OF assms(1)])
show ?thesis
using assms by(auto simp: m.Cauchy_inS_def Cauchy_inS_def,simp add: submetric_def) metis
qed
lemma(in metric_set) convergent_insubmetric:
assumes "S' ⊆ S" "f ∈ UNIV → S'" "x ∈ S'" "converge_to_inS f x"
shows "metric_set.converge_to_inS S' (submetric S' dist) f x"
proof -
interpret m: metric_set S' "submetric S' dist"
by(rule submetric_metric_set[OF assms(1)])
show ?thesis
unfolding m.converge_to_inS_def using assms
by(auto simp: converge_to_inS_def funcset_mem[OF assms(2)] submetric_def)
qed
lemma(in metric_set) the_limit_of_submetric_eq:
assumes "S' ⊆ S" "metric_set.convergent_inS S' (submetric S' dist) f"
shows "metric_set.the_limit_of S' (submetric S' dist) f = the_limit_of f"
by (meson assms(1) assms(2) converge_to_insub_converge_to_inS convergent_insub_convergent_inS metric_set.converge_to_inS_unique metric_set.the_limit_if_converge metric_set_axioms submetric_metric_set)
lemma submetric_of_euclidean:
"metric_set A (submetric A dist)" "metric_set.mtopology A (submetric A dist) = top_of_set A"
using metric_set.submetric_metric_set[OF metric_class_metric_set,of A] metric_set.submetric_subtopology[OF metric_class_metric_set,of A]
by(auto simp: euclidean_mtopology)
lemma(in metric_set)
assumes "B ⊆ S"
shows totally_bounded_on_submetric: "totally_bounded_on B ⟷ metric_set.totally_boundedS B (submetric B dist)"
proof -
interpret m: metric_set B "submetric B dist"
by(rule submetric_metric_set[OF assms(1)])
show ?thesis
unfolding totally_bounded_on_def m.totally_boundedS_def
proof safe
fix e :: real
assume h:"∀e>0. ∃A. eps_net_on B e A" "e > 0"
then obtain A where A:"eps_net_on B (e / 2) A"
by fastforce
define A' where "A' ≡ A ∩ {z. open_ball z (e / 2) ∩ B ≠ {}}"
have A': "eps_net_on B (e / 2) A'"
unfolding eps_net_on_def
proof safe
fix x
assume x:"x ∈ B"
then obtain a where a:"a ∈ A" "x ∈ open_ball a (e / 2)"
using A by(auto dest: eps_net_onD)
with x have "a ∈ A'"
by(auto simp: A'_def)
with a show "x ∈ (⋃a∈A'. open_ball a (e / 2))" by auto
qed(use h eps_net_on_def A'_def A in auto)
define b where "b ≡ (λa. SOME b. b ∈ B ∧ b ∈ open_ball a (e / 2))"
have b:"b a ∈ B" "b a ∈ open_ball a (e / 2)" if a: "a ∈ A'" for a
proof -
have "b a ∈ B ∧ b a ∈ open_ball a (e / 2)"
unfolding b_def by(rule someI_ex) (insert that, auto simp: A'_def)
thus "b a ∈ B" "b a ∈ open_ball a (e / 2)" by auto
qed
show "∃A. m.eps_net e A"
unfolding m.eps_net_on_def
proof(safe intro!: exI[where x="b ` A'"])
fix x
assume "x ∈ B"
then obtain a where a: "a ∈ A'" "x ∈ open_ball a (e / 2)"
using A' by(auto simp: eps_net_on_def)
show "x ∈ (⋃a∈b ` A'. m.open_ball a e)"
proof
show "b a ∈ b ` A'"
using a by auto
next
have [simp]: "b a ∈ S" "x ∈ S" "b a ∈ B" "x ∈ B" "a ∈ S"
using b(1)[OF a(1)] assms ‹x ∈ B› a A' by (auto simp: eps_net_on_def)
note order.strict_trans1[OF dist_tr add_strict_mono[OF open_ballD[OF a(2),simplified dist_sym[of a]] open_ballD[OF b(2)[OF a(1)]]],simplified]
hence "submetric B dist x (b a) < e"
by(auto simp: submetric_def)
thus "x ∈ m.open_ball (b a) e"
by(auto simp: m.open_ball_def m.dist_sym)
qed
qed(insert h(2) A' b, auto simp: eps_net_on_def)
next
fix e :: real
assume "∀e>0. ∃A. m.eps_net e A" "e > 0"
then obtain A where A: "m.eps_net e A" by auto
thus "∃A. eps_net_on B e A"
using assms submetric_open_ball_subset[OF assms] by(auto intro!: exI[where x=A] simp: eps_net_on_def m.eps_net_def) blast
qed
qed
text ‹ Continuous functions ›
context
fixes S :: "'a set" and d
and S':: "'b set" and d'
assumes "metric_set S d" "metric_set S' d'"
begin
interpretation m1: metric_set S d by fact
interpretation m2: metric_set S' d' by fact
lemma metric_set_continuous_map_eq:
shows "continuous_map m1.mtopology m2.mtopology f
⟷ f ∈ S → S' ∧ (∀x∈S. ∀ε>0. ∃δ>0. ∀y∈S. d x y < δ ⟶ d' (f x) (f y) < ε)"
proof safe
show "⋀x. continuous_map m1.mtopology m2.mtopology f ⟹ x ∈ S ⟹ f x ∈ S'"
using m1.mtopology_topspace m2.mtopology_topspace by(auto dest: continuous_map_image_subset_topspace)
next
fix x ε
assume "continuous_map m1.mtopology m2.mtopology f"
"x ∈ S" "(0 :: real) < ε"
then have "openin m1.mtopology {z ∈ S. f z ∈ m2.open_ball (f x) ε}" "f x ∈ S'"
using openin_continuous_map_preimage[OF ‹continuous_map m1.mtopology m2.mtopology f›] m2.mtopology_open_ball_in[of "f x",OF _ ‹0 < ε›] continuous_map_image_subset_topspace[OF ‹continuous_map m1.mtopology m2.mtopology f›] m1.mtopology_topspace m2.mtopology_topspace
by auto
moreover have "x ∈ {z ∈ S. f z ∈ m2.open_ball (f x) ε}"
using ‹x ∈ S› ‹0 < ε› continuous_map_image_subset_topspace[OF ‹continuous_map m1.mtopology m2.mtopology f›] m1.mtopology_topspace m2.mtopology_topspace m2.dist_0[of "f x" "f x"]
by(auto simp: m2.open_ball_def)
ultimately obtain δ where
"δ>0" "m1.open_ball x δ ⊆ {z ∈ S. f z ∈ m2.open_ball (f x) ε}"
by (auto simp: m1.mtopology_openin_iff)
thus "∃δ>0. ∀y∈S. d x y < δ ⟶ d' (f x) (f y) < ε"
using ‹x ∈ S› ‹f x ∈ S'› by(auto intro!: exI[where x=δ] simp: m1.open_ball_def m2.open_ball_def)
next
assume "f ∈ S → S'"
and h:"∀x∈S. ∀ε>0. ∃δ>0. ∀y∈S. d x y < δ ⟶ d' (f x) (f y) < ε"
show "continuous_map m1.mtopology m2.mtopology f"
unfolding continuous_map
proof safe
show "⋀x. x ∈ topspace m1.mtopology ⟹ f x ∈ topspace m2.mtopology"
using ‹f ∈ S → S'› m1.mtopology_topspace m2.mtopology_topspace by auto
next
fix U
assume "openin m2.mtopology U"
show "openin m1.mtopology {x ∈ topspace m1.mtopology. f x ∈ U}"
unfolding m1.mtopology_openin_iff
proof safe
show "⋀x. x ∈ topspace m1.mtopology ⟹ f x ∈ U ⟹ x ∈ S"
using ‹f ∈ S → S'› m1.mtopology_topspace m2.mtopology_topspace by auto
next
fix x
assume "x ∈ topspace m1.mtopology" "f x ∈ U"
then obtain ε where he:
"ε > 0" "m2.open_ball (f x) ε ⊆ U"
using ‹openin m2.mtopology U› by(auto simp: m2.mtopology_openin_iff)
then obtain δ where hd:
"δ > 0" "⋀y. y ∈ S ⟹ d x y < δ ⟹ d' (f x) (f y) < ε"
using ‹x ∈ topspace m1.mtopology› m1.mtopology_topspace h by metis
thus "∃ε>0. m1.open_ball x ε ⊆ {x ∈ topspace m1.mtopology. f x ∈ U}"
using m1.open_ballD m1.open_ballD' m1.mtopology_topspace he(2) ‹f ∈ S → S'›
by(auto intro!: exI[where x=δ] simp: m2.open_ball_def) fastforce
qed
qed
qed
lemma metric_set_continuous_map_eq':
shows "continuous_map m1.mtopology m2.mtopology f
⟷ f ∈ S → S' ∧ (∀x z. m1.converge_to_inS x z ⟶ m2.converge_to_inS (λn. f (x n)) (f z))"
proof
show "continuous_map m1.mtopology m2.mtopology f ⟹ f ∈ S → S' ∧ (∀x z. m1.converge_to_inS x z ⟶ m2.converge_to_inS (λn. f (x n)) (f z))"
unfolding metric_set_continuous_map_eq
proof safe
fix x z
assume h:"f ∈ S → S'" "∀x∈S. ∀ε>0. ∃δ>0. ∀y∈S. d x y < δ ⟶ d' (f x) (f y) < ε" "m1.converge_to_inS x z"
hence h':"x ∈ m1.sequence" "z ∈ S" "⋀ε. ε > 0 ⟹ ∃N. ∀n≥N. d (x n) z < ε"
by(auto simp: m1.converge_to_inS_def2)
show "m2.converge_to_inS (λn. f (x n)) (f z)"
unfolding m2.converge_to_inS_def2
proof safe
show "f (x n) ∈ S'" "f z ∈ S'" for n
using h'(1,2) h(1) by auto
next
fix ε
assume he:"(0 :: real) < ε"
then obtain δ where hd:"δ > 0" "⋀y. y ∈ S ⟹ d z y < δ ⟹ d' (f z) (f y) < ε"
using h(2) h'(2) by metis
obtain N where hn: "⋀n. n ≥ N ⟹ d z (x n) < δ"
using h'(3)[OF hd(1),simplified m1.dist_sym[of _ z]] by auto
show "∃N. ∀n≥N. d' (f (x n)) (f z) < ε"
proof(safe intro!: exI[where x=N])
fix n
assume "n ≥ N"
then have "x n ∈ S" "d z (x n) < δ"
using hn[OF ‹n ≥ N›] h'(1) by auto
thus "d' (f (x n)) (f z) < ε"
by(auto intro!: hd(2) simp: m2.dist_sym[of _ "f z"])
qed
qed
qed
next
assume "f ∈ S → S' ∧ (∀x z. m1.converge_to_inS x z ⟶ m2.converge_to_inS (λn. f (x n)) (f z))"
hence h:"f ∈ S → S'" "⋀x z. m1.converge_to_inS x z ⟹ m2.converge_to_inS (λn. f (x n)) (f z)" by auto
show "continuous_map m1.mtopology m2.mtopology f"
unfolding continuous_map_closedin
proof safe
show "x ∈ topspace m1.mtopology ⟹ f x ∈ topspace m2.mtopology" for x
using m1.mtopology_topspace m2.mtopology_topspace h(1) by auto
next
fix C
assume hcl:"closedin m2.mtopology C"
show "closedin m1.mtopology {x ∈ topspace m1.mtopology. f x ∈ C}"
unfolding m1.mtopology_closedin_iff
proof safe
fix y s
assume hg:"y ∈ UNIV → {x ∈ topspace m1.mtopology. f x ∈ C}" " m1.converge_to_inS y s"
hence "(λn. f (y n)) ∈ UNIV → C"
by auto
thus "f s ∈ C" "s ∈ topspace m1.mtopology"
using h(2)[OF hg(2)] hcl[simplified m2.mtopology_closedin_iff] hg(2)[simplified m1.converge_to_inS_def] m1.mtopology_topspace
by auto
qed(simp add: m1.mtopology_topspace)
qed
qed
lemma continuous_map_limit_of:
assumes "continuous_map m1.mtopology m2.mtopology f" "m1.convergent_inS xn"
shows "m2.the_limit_of (λn. f (xn n)) = f (m1.the_limit_of xn)"
using assms m1.the_limit_if_converge m2.the_limit_of_eq
by(simp add: metric_set_continuous_map_eq')
text ‹ Uniform continuous functions. ›
definition uniform_continuous_map :: "('a ⇒ 'b) ⇒ bool" where
"uniform_continuous_map f ⟷ f ∈ S → S' ∧ (∀ε>0. ∃δ>0. ∀x∈S. ∀y∈S. d x y < δ ⟶ d' (f x) (f y) < ε)"
lemma uniform_continuous_map_const:
assumes "y ∈ S'"
shows "uniform_continuous_map (λx. y)"
using assms by(auto simp: uniform_continuous_map_def)
lemma continuous_if_uniform_continuous:
assumes "uniform_continuous_map f"
shows "continuous_map m1.mtopology m2.mtopology f"
unfolding metric_set_continuous_map_eq
proof safe
show "x ∈ S ⟹ f x ∈ S'" for x
using assms by(auto simp: uniform_continuous_map_def)
next
fix x ε
assume [simp]:"x ∈ S" and "(0 :: real) < ε"
then obtain δ where "δ > 0" "⋀x y. x ∈ S ⟹ y ∈ S ⟹ d x y < δ ⟹ d' (f x) (f y) < ε"
using assms by(auto simp: uniform_continuous_map_def)
thus "∃δ>0. ∀y∈S. d x y < δ ⟶ d' (f x) (f y) < ε"
by(auto intro!: exI[where x=δ])
qed
definition converges_uniformly :: "[nat ⇒ 'a ⇒ 'b, 'a ⇒ 'b] ⇒ bool" where
"converges_uniformly fn f ⟷ (∀n. fn n ∈ S → S') ∧ (f ∈ S → S') ∧ (∀e>0. ∃N. ∀n≥N. ∀x∈S. d' (fn n x) (f x) < e)"
lemma converges_uniformly_continuous:
assumes "⋀n. continuous_map m1.mtopology m2.mtopology (fn n)"
and "converges_uniformly fn f"
shows "continuous_map m1.mtopology m2.mtopology f"
unfolding metric_set_continuous_map_eq
proof safe
fix x e
assume h:"x ∈ S" "e > (0 :: real)"
then obtain N where N: "⋀z n. n ≥ N ⟹ z ∈ S ⟹ d' (fn n z) (f z) < e / 3"
using assms(2) by(simp only: converges_uniformly_def) (meson zero_less_divide_iff zero_less_numeral)
have f: "⋀n x. x ∈ S ⟹ fn n x ∈ S'" "⋀x. x ∈ S ⟹ f x ∈ S'"
using assms(2) by(auto simp: converges_uniformly_def)
from assms(1)[of N] h obtain δ where h': "δ > 0" "⋀y. y ∈ S ⟹ d x y < δ ⟹ d' (fn N x) (fn N y) < e / 3"
by (metis metric_set_continuous_map_eq zero_less_divide_iff zero_less_numeral)
show "∃δ>0. ∀y∈S. d x y < δ ⟶ d' (f x) (f y) < e"
proof(safe intro!: exI[where x=δ])
fix y
assume y:"y ∈ S" "d x y < δ"
have "d' (f x) (f y) ≤ d' (f x) (fn N x) + d' (fn N x) (fn N y) + d' (fn N y) (f y)"
using m2.dist_tr[of "f x" "fn N x" "f y"] m2.dist_tr[of "fn N x" "fn N y" "f y"] f[OF y(1)] f[OF h(1)]
by auto
also have "... < e"
using N[OF order_refl h(1),simplified m2.dist_sym] N[OF order_refl y(1)] h'(2)[OF y]
by auto
finally show "d' (f x) (f y) < e" .
qed(use h' in auto)
qed(use assms(2) converges_uniformly_def in auto)
text ‹ Lemma related @{term osc_on}.›
lemma osc_on_inA_0:
assumes "x ∈ A ∩ S" "continuous_map (subtopology m1.mtopology (A ∩ S)) m2.mtopology f"
shows "m2.osc_on A m1.mtopology f x = 0"
proof -
interpret subm1: metric_set "A ∩ S" "submetric (A ∩ S) d"
by(auto intro!: m1.submetric_metric_set)
have cont: "continuous_map subm1.mtopology m2.mtopology f"
using assms(2) by (simp add: m1.submetric_subtopology)
have "m2.osc_on A m1.mtopology f x < ennreal ε" if e:"ε > 0" for ε
unfolding m2.osc_on_less_iff
proof -
obtain ε' where "ε' > 0" "2*ε' < ε"
using e field_lbound_gt_zero[of "ε/2" "ε/2"] by auto
then obtain δ where hd:"δ>0" "⋀y. y ∈ A ⟹ y∈S ⟹ d x y < δ ⟹ d' (f x) (f y) < ε'"
using assms(1) cont[simplified Set_Based_Metric_Space.metric_set_continuous_map_eq[OF subm1.metric_set_axioms m2.metric_set_axioms]]
by(fastforce simp: submetric_def)
show "∃v. x ∈ v ∧ openin m1.mtopology v ∧ m2.diam (f ` (A ∩ v)) < ennreal ε"
proof(safe intro!: exI[where x="m1.open_ball x δ"] m1.open_ball_ina m1.mtopology_open_ball_in)
have "m2.diam (f ` (A ∩ m1.open_ball x δ)) ≤ ennreal (2*ε')"
unfolding m2.diam_def Sup_le_iff
proof safe
fix a1 a2
assume h:"a1 ∈ A" "a1 ∈ m1.open_ball x δ" "f a1 ∈ S'"
"a2 ∈ A" "a2 ∈ m1.open_ball x δ" "f a2 ∈ S'"
have "f x ∈ S'"
using cont assms(1) by(auto simp: Set_Based_Metric_Space.metric_set_continuous_map_eq[OF subm1.metric_set_axioms m2.metric_set_axioms])
have "d' (f a1) (f a2) < 2*ε'"
using hd(2)[OF ‹a1 ∈ A› m1.open_ballD'(1)[OF h(2)] m1.open_ballD[OF h(2)]] hd(2)[OF ‹a2 ∈ A› m1.open_ballD'(1)[OF h(5)] m1.open_ballD[OF h(5)]] m2.dist_tr[OF ‹f a1 ∈ S'› ‹f x ∈ S'› ‹f a2 ∈ S'›,simplified m2.dist_sym[of "f a1" "f x"]]
by auto
thus "ennreal (d' (f a1) (f a2)) ≤ ennreal (2*ε')"
by (simp add: ennreal_leI)
qed
also have "... < ennreal ε"
using ‹2*ε' < ε› ennreal_lessI e by presburger
finally show "m2.diam (f ` (A ∩ m1.open_ball x δ)) < ennreal ε" .
qed(use hd(1) IntD2[OF assms(1)] in auto)
qed
hence "m2.osc_on A m1.mtopology f x < ε" if "ε > 0" for ε
by (metis ennreal_enn2real ennreal_le_epsilon ennreal_less_zero_iff linorder_not_le order_le_less_trans that)
thus ?thesis
by fastforce
qed
end
context metric_set
begin
interpretation rnv: metric_set "UNIV :: ('b :: real_normed_vector) set" dist_typeclass
by simp
lemma dist_set_uniform_continuous:
"uniform_continuous_map S dist UNIV dist_typeclass (dist_set A)"
unfolding uniform_continuous_map_def[OF metric_set_axioms rnv.metric_set_axioms] dist_real_def
proof safe
fix ε :: real
assume "0 < ε"
then show "∃δ>0. ∀x∈S. ∀y∈S. dist x y < δ ⟶ ¦dist_set A x - dist_set A y¦ < ε"
using order.strict_trans1[OF dist_set_abs_le] by(auto intro!: exI[where x=ε])
qed simp
lemma dist_set_continuous: "continuous_map mtopology euclideanreal (dist_set A)"
unfolding euclidean_mtopology[symmetric]
by(auto intro!: continuous_if_uniform_continuous simp: dist_set_uniform_continuous metric_set_axioms)
lemma uniform_continuous_map_add:
fixes f :: "'a ⇒ 'b::real_normed_vector"
assumes "uniform_continuous_map S dist UNIV dist_typeclass f" "uniform_continuous_map S dist UNIV dist_typeclass g"
shows "uniform_continuous_map S dist UNIV dist_typeclass (λx. f x + g x)"
unfolding uniform_continuous_map_def[OF metric_set_axioms rnv.metric_set_axioms]
proof safe
fix e :: real
assume "e > 0"
from half_gt_zero[OF this] assms obtain d1 d2 where d: "d1 > 0" "d2 > 0"
"⋀x y. x ∈ S ⟹ y ∈ S ⟹ dist x y < d1 ⟹ dist_typeclass (f x) (f y) < e / 2" "⋀x y. x ∈ S ⟹ y ∈ S ⟹ dist x y < d2 ⟹ dist_typeclass (g x) (g y) < e / 2"
by(simp only: uniform_continuous_map_def[OF metric_set_axioms rnv.metric_set_axioms]) metis
show "∃δ>0. ∀x∈S. ∀y∈S. dist x y < δ ⟶ dist_typeclass (f x + g x) (f y + g y) < e"
using d by(fastforce intro!: exI[where x="min d1 d2"] order.strict_trans1[OF dist_triangle_add])
qed simp
lemma uniform_continuous_map_real_devide:
fixes f :: "'a ⇒ real"
assumes "uniform_continuous_map S dist UNIV dist_typeclass f" "uniform_continuous_map S dist UNIV dist_typeclass g"
and "⋀x. x ∈ S ⟹ g x ≠ 0" "⋀x. x ∈ S ⟹ ¦g x¦ ≥ a" "a > 0" "⋀x. x ∈ S ⟹ ¦g x¦ < Kg"
and "⋀x. x ∈ S ⟹ ¦f x¦ < Kf"
shows "uniform_continuous_map S dist UNIV dist_typeclass (λx. f x / g x)"
unfolding uniform_continuous_map_def[OF metric_set_axioms rnv.metric_set_axioms]
proof safe
fix e :: real
assume e[arith]:"e > 0"
consider "S = {}" | "S ≠ {}" by auto
then show "∃δ>0. ∀x∈S. ∀y∈S. dist x y < δ ⟶ dist_typeclass (f x / g x) (f y / g y) < e"
proof cases
case 1
then show ?thesis by (auto intro!: exI[where x=1])
next
case S:2
then have Kfg_pos[arith]: "Kg > 0" "Kf ≥ 0"
using assms(4-7) by auto fastforce+
define e' where "e' ≡ a^2 / (Kf + Kg) * e"
have e':"e' > 0"
using assms(5) by(auto simp: e'_def)
with assms obtain d1 d2 where d: "d1 > 0" "d2 > 0"
"⋀x y. x ∈ S ⟹ y ∈ S ⟹ dist x y < d1 ⟹ ¦f x - f y¦ < e'" "⋀x y. x ∈ S ⟹ y ∈ S ⟹ dist x y < d2 ⟹ ¦g x - g y¦ < e'"
by(auto simp: uniform_continuous_map_def[OF metric_set_axioms rnv.metric_set_axioms] dist_real_def) metis
show ?thesis
unfolding dist_real_def
proof(safe intro!: exI[where x="min d1 d2"])
fix x y
assume x:"x ∈ S" and y:"y ∈ S" and "dist x y < min d1 d2"
then have dist[arith]: "dist x y < d1" "dist x y < d2" by auto
note [arith] = assms(3,4,6,7)[OF x] assms(3,4,6,7)[OF y]
have "¦f x / g x - f y / g y¦ = ¦(f x * g y - f y * g x) / (g x * g y)¦"
by(simp add: diff_frac_eq)
also have "... = ¦(f x * g y - f x * g x + (f x * g x - f y * g x)) / (g x * g y)¦"
by simp
also have "... = ¦(f x - f y) * g x - f x * (g x - g y)¦ / (¦g x¦ * ¦g y¦)"
by(simp add: left_diff_distrib right_diff_distrib abs_mult)
also have "... ≤ (¦f x - f y¦ * ¦g x¦ + ¦f x¦ * ¦g x - g y¦) / (¦g x¦ * ¦g y¦)"
by(rule divide_right_mono) (use abs_triangle_ineq4 abs_mult in metis,auto)
also have "... < (e' * Kg + Kf * e') / (¦g x¦ * ¦g y¦)"
by(rule divide_strict_right_mono[OF add_less_le_mono]) (auto intro!: mult_mono' mult_strict_mono, use d(3,4)[OF x y] in auto)
also have "... ≤ (e' * Kg + Kf * e') / a^2"
by(auto intro!: divide_left_mono simp: power2_eq_square) (insert assms(5) e', auto simp: ‹a ≤ ¦g x¦› mult_mono')
also have "... = (Kf + Kg) / a^2 * e'"
by (simp add: distrib_left mult.commute)
also have "... = e"
using assms(5) by(auto simp: e'_def)
finally show " ¦f x / g x - f y / g y¦ < e" .
qed(use d in auto)
qed
qed simp
lemma the_limit_of_dist_converge:
assumes "converge_to_inS xn x"
shows "(λn. dist (xn n) y) ⇢ dist (the_limit_of xn) y"
proof -
have "continuous_map mtopology euclideanreal (λz. dist z y)"
using dist_set_continuous[of "{y}"] by simp
hence "(λn. dist (xn n) y) ⇢ dist x y"
using assms
by(auto simp: metric_set_continuous_map_eq'[OF metric_set_axioms rnv.metric_set_axioms,simplified euclidean_mtopology] converge_to_def_set)
thus ?thesis
by(simp add: the_limit_of_eq[OF assms])
qed
lemma the_limit_of_dist_converge':
assumes "converge_to_inS xn x" "ε > 0"
shows "∃N. ∀n≥N. ¦ dist (xn n) y - dist (the_limit_of xn) y ¦ < ε"
using the_limit_of_dist_converge[OF assms(1)] assms(2) by(simp add: LIMSEQ_iff)
lemma the_limit_of_dist:
assumes "converge_to_inS xn x"
shows "lim (λn. dist (xn n) y) = dist (the_limit_of xn) y"
using the_limit_of_dist_converge[OF assms] limI by blast
text ‹ Upper-semicontinuous functions.›
lemma upper_semicontinuous_map_def2:
fixes f :: "'a ⇒ ('b :: {complete_linorder,linorder_topology})"
shows "upper_semicontinuous_map mtopology f ⟷ (∀x y. converge_to_inS x y ⟶ limsup (λn. f (x n)) ≤ f y)"
proof
show "upper_semicontinuous_map mtopology f ⟹ ∀x y. converge_to_inS x y ⟶ limsup (λn. f (x n)) ≤ f y"
unfolding upper_semicontinuous_map_def
proof safe
fix x y
assume h:"∀a. openin mtopology {x ∈ topspace mtopology. f x < a}" "converge_to_inS x y"
show "limsup (λn. f (x n)) ≤ f y"
unfolding Limsup_le_iff eventually_sequentially
proof safe
fix c
assume "f y < c"
show "∃N. ∀n≥N. f (x n) < c"
proof(rule ccontr)
assume "∄N. ∀n≥N. f (x n) < c"
then have hc:"⋀N. ∃n≥N. f (x n) ≥ c"
using linorder_not_less by blast
define a :: "nat ⇒ nat" where "a ≡ rec_nat (SOME n. f (x n) ≥ c) (λn an. SOME m. m > an ∧ f (x m) ≥ c)"
have "strict_mono a"
proof(rule strict_monoI_Suc)
fix n
have [simp]:"a (Suc n) = (SOME m. m > a n ∧ f (x m) ≥ c)"
by(auto simp: a_def)
show "a n < a (Suc n)"
by simp (metis (mono_tags, lifting) Suc_le_lessD hc someI)
qed
have *:"f (x (a n)) ≥ c" for n
proof(cases n)
case 0
then show ?thesis
using hc[of 0] by(auto simp: a_def intro!: someI_ex)
next
case (Suc n')
then show ?thesis
by(simp add: a_def) (metis (mono_tags, lifting) Suc_le_lessD hc someI_ex)
qed
obtain N where "⋀n. n ≥ N ⟹ x (a n) ∈ {x ∈ S. f x < c}"
using converge_to_inS_subseq[OF ‹strict_mono a› h(2)] mtopology_openin_iff2[of "{x ∈ S. f x < c}"] h(2)[simplified converge_to_inS_def] mtopology_topspace ‹f y < c› h
by fastforce
from *[of N] this[of N] show False by auto
qed
qed
qed
next
assume h:"∀x y. converge_to_inS x y ⟶ limsup (λn. f (x n)) ≤ f y"
show "upper_semicontinuous_map mtopology f"
unfolding upper_semicontinuous_map_def mtopology_openin_iff2 mtopology_topspace
proof safe
fix a y s
assume "converge_to_inS y s" "s ∈ S" "f s < a"
then have "limsup (λn. f (y n)) ≤ f s"
using h by auto
with ‹f s < a› obtain N where "⋀n. n≥N ⟹ f (y n) < a"
by(auto simp: Limsup_le_iff eventually_sequentially)
thus "∃N. ∀n≥N. y n ∈ {x ∈ S. f x < a}"
using ‹converge_to_inS y s› by(auto intro!: exI[where x=N] simp: converge_to_inS_def)
qed
qed
lemma upper_semicontinuous_map_def2real:
fixes f :: "'a ⇒ real"
shows "upper_semicontinuous_map mtopology f ⟷ (∀x y. converge_to_inS x y ⟶ limsup (λn. f (x n)) ≤ f y)"
unfolding upper_semicontinuous_map_real_iff upper_semicontinuous_map_def2
by auto
lemma osc_upper_semicontinuous_map:
"upper_semicontinuous_map X (osc X f)"
proof -
have "{x ∈ topspace X. osc X f x < a} = ⋃ {V. openin X V ∧ diam (f ` V) < a}" for a
using openin_subset by(auto simp add: osc_less_iff)
thus ?thesis
by(auto simp: upper_semicontinuous_map_def)
qed
end
text ‹ Open maps.›
lemma metric_set_opem_map_from_dist:
assumes "metric_set S d" "metric_set S' d'" "f ∈ S → S'"
and "⋀x ε. x ∈ S ⟹ ε > 0 ⟹ ∃δ>0. ∀y∈S. d' (f x) (f y) < δ ⟶ d x y < ε"
shows "open_map (metric_set.mtopology S d) (subtopology (metric_set.mtopology S' d') (f ` S)) f"
proof -
interpret m1: metric_set S d by fact
interpret m2: metric_set S' d' by fact
interpret m2': metric_set "f ` S" "submetric (f ` S) d'"
using assms(3) by(auto intro!: m2.submetric_metric_set)
show ?thesis
proof(rule open_map_with_base[OF m1.mtopology_basis_ball])
fix A
assume "A ∈ {m1.open_ball a ε |a ε. a ∈ S ∧ 0 < ε}"
then obtain a ε where hae:
"a ∈ S" "0 < ε" "A = m1.open_ball a ε" by auto
show "openin (subtopology m2.mtopology (f ` S)) (f ` A)"
unfolding m2.submetric_subtopology[OF funcset_image[OF assms(3)]] m2'.mtopology_openin_iff
proof
show "f ` A ⊆ f ` S"
using m1.open_ball_subset_ofS[of a ε] by(auto simp: hae(3))
next
show "∀x∈f ` A. ∃ε>0. m2'.open_ball x ε ⊆ f ` A"
proof safe
fix x
assume "x ∈ A"
hence "x ∈ S"
using m1.open_ball_subset_ofS[of a ε] by(auto simp: hae(3))
moreover have "0 < ε - d a x"
using ‹x ∈ A› m1.open_ballD[of x a ε] by(auto simp: hae(3))
ultimately obtain δ where hd:"δ > 0" "⋀y. y∈S ⟹ d' (f x) (f y) < δ ⟹ d x y < ε - d a x"
using assms(4) by metis
show "∃ε>0. m2'.open_ball (f x) ε ⊆ f ` A"
proof(safe intro!: exI[where x=δ])
fix z
assume "z ∈ m2'.open_ball (f x) δ"
note hz = m2'.open_ballD'[OF this]
then obtain y where "y ∈ S" "z = f y" by auto
hence "d' (f x) (f y) < δ"
using m2'.open_ballD[OF ‹z ∈ m2'.open_ball (f x) δ›] ‹x ∈ A› m1.open_ball_subset_ofS[of a ε]
by(auto simp: submetric_def hae(3))
hence "d x y < ε - d a x"
by(auto intro!: hd(2)[OF ‹y ∈ S›])
hence "d a y < ε"
using m1.dist_tr[OF ‹a ∈ S› ‹x ∈ S› ‹y ∈ S›] by auto
thus "z ∈ f ` A"
by (simp add: ‹y ∈ S› ‹z = f y› hae(1) hae(3) m1.open_ball_def)
qed(use hd in auto)
qed
qed
qed
qed
subsubsection ‹ Complete Metric Spaces›
locale complete_metric_set = metric_set +
assumes convergence: "⋀f. Cauchy_inS f ⟹ convergent_inS f"
lemma complete_space_complete_metric_set:
"complete_metric_set (UNIV :: 'a :: complete_space set) dist"
proof -
interpret m: metric_set UNIV dist
by(rule metric_class_metric_set)
show ?thesis
by standard (simp add: Cahuchy_def_set[symmetric] convergent_def_set[symmetric] Cauchy_convergent_iff)
qed
lemma(in complete_metric_set) submetric_complete_iff:
assumes "M ⊆ S"
shows "complete_metric_set M (submetric M dist) ⟷ closedin mtopology M"
proof
assume "complete_metric_set M (submetric M dist)"
then interpret m: complete_metric_set M "submetric M dist" .
show "closedin mtopology M"
proof(rule ccontr)
assume "¬ closedin mtopology M"
then have "∃f∈m.sequence. ∃s. converge_to_inS f s ∧ s ∉ M"
using assms mtopology_closedin_iff by auto
then obtain f s where hfs:"f ∈ m.sequence" "converge_to_inS f s" "s ∉ M"
by auto
hence "convergent_inS f"
by(auto simp: convergent_inS_def converge_to_inS_def)
have "m.Cauchy_inS f"
using Cauchy_if_convergent_inS[OF ‹convergent_inS f›] hfs(1)
by(auto simp: m.Cauchy_inS_def Cauchy_inS_def) (fastforce simp: submetric_def)
then obtain s' where "s' ∈ M" "m.converge_to_inS f s'"
using m.convergence by(auto simp: m.convergent_inS_def m.converge_to_inS_def)
from converge_to_insub_converge_to_inS[OF assms this(2)] hfs(2)
have "s' = s"
by(rule converge_to_inS_unique)
thus False
using ‹s' ∈ M› ‹s ∉ M› by simp
qed
next
interpret m: metric_set M "submetric M dist"
by(rule submetric_metric_set[OF assms])
assume cls:"closedin mtopology M"
show "complete_metric_set M (submetric M dist)"
proof
fix f
assume "m.Cauchy_inS f"
then have "f ∈ m.sequence" by(simp add: m.Cauchy_inS_def)
have "Cauchy_inS f"
by(rule Cauchy_insub_Cauchy[OF assms ‹m.Cauchy_inS f›])
then obtain x where hx:"x ∈ S" "converge_to_inS f x"
using convergence by(auto simp: convergent_inS_def converge_to_inS_def)
hence "x ∈ M"
using cls[simplified mtopology_closedin_iff] ‹f ∈ m.sequence› assms
by auto
hence "m.converge_to_inS f x"
using convergent_insubmetric[OF assms ‹f ∈ m.sequence›] hx by auto
thus "m.convergent_inS f"
using ‹x ∈ M› by(auto simp: m.convergent_inS_def)
qed
qed
lemma(in complete_metric_set) embed_dist_complete:
assumes "f ∈ B → S" "inj_on f B" "closedin mtopology (f ` B)"
shows "complete_metric_set B (embed_dist_on B f)"
proof -
interpret m: metric_set B "embed_dist_on B f"
by(rule embed_dist_dist[OF assms(1,2)])
show ?thesis
proof
fix xn
assume "m.Cauchy_inS xn"
hence h:"xn ∈ m.sequence" "Cauchy_inS (λn. f (xn n))"
by(auto simp add: embed_dist_Cauchy_inS_iff[OF assms(1,2)])
with convergence obtain x where x: "converge_to_inS (λn. f (xn n)) x"
by(auto simp: convergent_inS_def)
have x': "x ∈ f ` B"
proof -
have "(λn. f (xn n)) ∈ UNIV → f ` B"
using assms(1) h(1) by auto
thus ?thesis
using assms(3) x by(auto simp: mtopology_closedin_iff)
qed
then obtain b where b: "b ∈ B" "f b = x" by auto
show "m.convergent_inS xn"
by(auto simp: m.convergent_inS_def embed_dist_converge_to_inS_iff[OF assms(1,2)] b x h intro!: exI[where x=b])
qed
qed
lemma(in metric_set) Cantor_intersection_theorem:
"complete_metric_set S dist ⟷ (∀Fn. (∀n. Fn n ≠ {}) ∧ (∀n. closedin mtopology (Fn n)) ∧ decseq Fn ∧ (∀ε > 0. ∃N. ∀n≥N. diam (Fn n) < ε) ⟶ (∃x∈S. ⋂ (range Fn) = {x}))"
proof safe
fix Fn
assume "complete_metric_set S dist"
interpret complete_metric_set S dist by fact
assume h: "∀n. Fn n ≠ {}" " ∀n. closedin mtopology (Fn n)" "decseq Fn" "∀ε > 0. ∃N. ∀n≥N. diam (Fn n) < ε"
then obtain xn where xn1: "⋀n. xn n ∈ Fn n"
by (meson all_not_in_conv)
hence xn2: "xn ∈ sequence"
using closedin_subset[of mtopology] h(2) by(auto simp: mtopology_topspace)
have "Cauchy_inS xn"
unfolding Cauchy_inS_def
proof safe
fix ε :: real
assume "0 < ε"
then obtain N where N:"⋀n. n≥N ⟹ diam (Fn n) < ennreal ε"
using h(4) ennreal_less_zero_iff by blast
show "∃N. ∀n≥N. ∀m≥N. dist (xn n) (xn m) < ε"
proof(safe intro!: exI[where x=N])
fix n m
assume "n ≥ N" "m ≥ N"
define nm where "nm = min m n"
have "nm ≥ N" "nm ≤ n" "nm ≤ m"
using ‹n ≥ N› ‹m ≥ N› by(auto simp: nm_def)
hence "xn n ∈ Fn nm" "xn m ∈ Fn nm"
using decseqD[OF h(3)] xn1[of n] xn1[of m] by auto
hence "ennreal (dist (xn n) (xn m)) ≤ diam (Fn nm)"
using xn2 by(auto intro!: diam_is_sup mtopology_topspace)
also have "... < ennreal ε"
by(rule N[OF ‹nm ≥ N›])
finally show "dist (xn n) (xn m) < ε"
by (simp add: dist_geq0 ennreal_less_iff)
qed
qed(use xn2 in auto)
then obtain x where x:"x ∈ S" "converge_to_inS xn x"
using convergence[of xn] by(auto simp: convergent_inS_def converge_to_inS_def)
show "∃x∈S. ⋂ (range Fn) = {x}"
proof(safe intro!: bexI[where x=x])
fix n
show "x ∈ Fn n"
proof(rule ccontr)
assume "x ∉ Fn n"
moreover have "openin mtopology (S - Fn n)"
using h(2) by (simp add: openin_diff)
ultimately obtain ε where e: "ε > 0" "open_ball x ε ⊆ S - Fn n"
using x(1) by(auto simp: mtopology_openin_iff)
then have "∃N. ∀n≥N. xn n ∈ open_ball x ε"
using mtopology_openin_iff2[of "open_ball x ε"] open_ball_ina[OF x(1) e(1)] x(2)
by(auto simp: openin_open_ball)
then obtain N where N:"⋀m. m ≥ N ⟹ xn m ∈ open_ball x ε"
by auto
hence "xn m ∈ S - Fn m" if "m ≥ N" "m ≥ n" for m
using e(2) decseqD[OF h(3) that(2)] using that(1) by blast
from xn1[of "max N n"] this[of "max N n"]
show False by auto
qed
next
fix y
assume "y ∈ ⋂ (range Fn)"
then have hy:"∀n. y ∈ Fn n" by auto
have "y ∈ S"
using closedin_subset[of mtopology] h(2) hy mtopology_topspace by auto
have "converge_to_inS xn y"
unfolding converge_to_inS_def2
proof safe
fix ε :: real
assume "0 < ε"
then obtain N where N:"⋀n. n ≥ N ⟹ diam (Fn n) < ennreal ε"
using ennreal_less_zero_iff h(4) by presburger
show "∃N. ∀n≥N. dist (xn n) y < ε"
proof(safe intro!: exI[where x=N])
fix n
assume "n ≥ N"
then have "ennreal (dist (xn n) y) < ennreal ε"
using ‹y ∈ S› hy xn1[of n] xn2
by(auto intro!: order.strict_trans1[OF diam_is_sup[of "xn n" "Fn n" y] N[of n]])
thus "dist (xn n) y < ε"
by (simp add: dist_geq0 ennreal_less_iff)
qed
qed(use xn2 ‹y ∈ S› in auto)
with converge_to_inS_unique[OF x(2)]
show "y = x" by simp
qed(use x in auto)
next
assume h:"∀Fn. (∀n. Fn n ≠ {}) ∧ (∀n. closedin mtopology (Fn n)) ∧ decseq Fn ∧ (∀ε>0. ∃N. ∀n≥N. diam (Fn n) < ε) ⟶ (∃x∈S. ⋂ (range Fn) = {x})"
show "complete_metric_set S dist"
proof
fix xn
assume cauchy:"Cauchy_inS xn"
hence xn: "xn ∈ sequence"
by (simp add: Cauchy_inS_dest1)
define Fn where "Fn ≡ (λn. mtopology closure_of {xn m|m. m ≥ n})"
have Fn0': "{xn m|m. m ≥ n} ⊆ Fn n" for n
using xn by(auto intro!: closure_of_subset simp: Fn_def mtopology_topspace)
have Fn0: "⋀n. Fn n ⊆ S"
using xn by(auto simp: Fn_def in_closure_of metric_set.mtopology_topspace metric_set_axioms)
have Fn1: "Fn n ≠ {}" for n
using xn closure_of_eq_empty[of "{xn m|m. m ≥ n}" mtopology,simplified mtopology_topspace]
by(auto simp: Fn_def)
have Fn2:"⋀n. closedin mtopology (Fn n)"
by(simp add: Fn_def)
have Fn3: "decseq Fn"
by standard (auto simp: Fn_def intro!: closure_of_mono)
have Fn4:"∀ε>0. ∃N. ∀n≥N. diam (Fn n) < ε"
proof safe
fix ε :: ennreal
assume "0 < ε"
define e where "e ≡ min 1 ε"
have he: "e ≤ ε" "enn2real e > 0" "ennreal (enn2real e) = e"
using ‹0 < ε› by(auto simp: e_def enn2real_positive_iff min_less_iff_disj)
then obtain e' where e':"e' > 0" "e' < enn2real e"
using field_lbound_gt_zero by auto
then obtain N where N:"⋀n m. n ≥ N ⟹ m ≥ N ⟹ dist (xn n) (xn m) ≤ e'"
using cauchy by(fastforce simp: Cauchy_inS_def)
show "∃N. ∀n≥N. diam (Fn n) < ε"
proof(safe intro!: exI[where x=N])
fix n
assume "N ≤ n"
then have "diam (Fn n) ≤ ennreal e'"
by(auto intro!: diam_le N simp: Fn_def diam_eq_closure)
also have "... < e"
using e'(2) ennreal_lessI he(2) he(3) by fastforce
finally show "diam (Fn n) < ε"
using he(1) by auto
qed
qed
obtain x where x:"x∈S" "⋂ (range Fn) = {x}"
using h Fn1 Fn2 Fn3 Fn4 by metis
show "convergent_inS xn"
unfolding convergent_inS_def converge_to_inS_def2
proof(safe intro!: exI[where x=x])
fix ε :: real
assume he:"0 < ε"
then have "0 < ennreal ε" by simp
then obtain N where N: "⋀n. n ≥ N ⟹ diam (Fn n) < ennreal ε"
using Fn4 by metis
show "∃N. ∀n≥N. dist (xn n) x < ε"
proof(safe intro!: exI[where x=N])
fix n
assume "N ≤ n"
then have "xn n ∈ Fn N" "x ∈ Fn N"
using x(2) Fn0'[of N] by auto
hence "ennreal (dist (xn n) x) ≤ diam (Fn N)"
using Fn0 by(auto intro!: diam_is_sup)
also have "... < ennreal ε"
by(auto intro!: N)
finally show "dist (xn n) x < ε"
by (simp add: dist_geq0 ennreal_less_iff)
qed
qed(use xn x in auto)
qed
qed
lemma(in complete_metric_set) closed_decseq_Inter':
assumes "⋀n. Fn n ≠ {}" "⋀n. closedin mtopology (Fn n)" "decseq Fn"
and "⋀ε. ε > 0 ⟹ ∃N. ∀n≥N. diam (Fn n) < ε"
shows "∃x∈S. ⋂ (range Fn) = {x}"
using assms Cantor_intersection_theorem by(simp add: complete_metric_set_axioms)
lemma(in complete_metric_set) closed_decseq_Inter:
assumes "⋀n. Fn n ≠ {}" "⋀n. closedin mtopology (Fn n)" "decseq Fn"
and "⋀ε. ε > 0 ⟹ ∃N. ∀n≥N. diam (Fn n) < ennreal ε"
shows "∃x∈S. ⋂ (range Fn) = {x}"
proof -
have "∃N. ∀n≥N. diam (Fn n) < ε" if "ε > 0" for ε
proof -
consider "ε < ∞" | "ε = ∞"
using top.not_eq_extremum by fastforce
then show ?thesis
proof cases
case 1
with that have 2:"ennreal (enn2real ε) = ε"
by simp
have "0 < enn2real ε"
using 1 that by(simp add: enn2real_positive_iff)
from assms(4)[OF this] show ?thesis
by(simp add: 2)
next
case 2
then show ?thesis
by (metis assms(4) ennreal_less_top gt_ex infinity_ennreal_def order_less_imp_not_less top.not_eq_extremum)
qed
qed
thus ?thesis
using closed_decseq_Inter'[OF assms(1-3)] by simp
qed
subsubsection ‹ Separable Metric Spaces ›
locale separable_metric_set = metric_set +
assumes separable: "∃U. countable U ∧ dense_set U"
lemma(in metric_set) separable_if_countable:
assumes "countable S"
shows "separable_metric_set S dist"
apply standard
using assms by(auto intro!: exI[where x=S] simp: dense_set_S)
lemma(in metric_set) separable_iff_topological_separable:
"separable_metric_set S dist ⟷ separable mtopology"
by(simp add: separable_metric_set_def separable_metric_set_axioms_def separable_def metric_set_axioms)
lemma(in separable_metric_set) topological_separable_if_separable:
"separable mtopology"
using separable_iff_topological_separable
by (simp add: separable_metric_set_axioms)
lemma separable_metric_setI:
assumes "metric_set S d" "separable (metric_set.mtopology S d)"
shows "separable_metric_set S d"
by (simp add: assms(1) assms(2) metric_set.separable_iff_topological_separable)
text ‹ For a metric space $X$, $X$ is separable iff $X$ is second countable.›
lemma(in metric_set) generated_by_countable_balls:
assumes "countable U" and "dense_set U"
shows "mtopology = topology_generated_by {open_ball y (1 / real n) | y n. y ∈ U}"
proof -
have hu: "U ⊆ S" "⋀x ε. x ∈ S ⟹ ε > 0 ⟹ open_ball x ε ∩ U ≠ {}"
using assms by(auto simp: dense_set_def)
show ?thesis
unfolding mtopology_def2
proof(rule topology_generated_by_eq)
fix K
assume "K ∈ {open_ball y (1 / real n) |y n. y ∈ U}"
then obtain y n where hyn:
"y ∈ U" "y ∈ S" "K = open_ball y (1 / real n)"
using hu(1) by auto
consider "n = 0" | "n > 0" by auto
then show "openin (topology_generated_by {open_ball a ε |a ε. a ∈ S ∧ 0 < ε}) K"
proof cases
case 1
then have "K = {}"
using hyn dist_geq0[of y] not_less by(auto simp: open_ball_def)
thus ?thesis
by auto
next
case 2
then have "1 / real n > 0" by auto
thus ?thesis
using hyn mtopology_open_ball_in[simplified mtopology_def2] by auto
qed
next
have h0:"⋀x ε. x ∈ S ⟹ ε > 0 ⟹ ∃y∈U. ∃n. x ∈ open_ball y (1 / real n) ∧ open_ball y (1 / real n) ⊆ open_ball x ε"
proof -
fix x ε
assume h: "x ∈ S" "(0 :: real) < ε"
then obtain N where hn: "1 / ε < real N"
using reals_Archimedean2 by blast
have hn0: "0 < real N"
by(rule ccontr) (use hn h in fastforce)
hence hn':"1 / real N < ε"
using h hn by (metis divide_less_eq mult.commute)
have "open_ball x (1 / (2 * real N)) ∩ U ≠ {}"
using dense_set_def[of U] assms(2) h(1) hn0 by fastforce
then obtain y where hy:
"y∈U" "y ∈ S" "y ∈ open_ball x (1 / (real (2 * N)))"
using hu by auto
show "∃y∈U. ∃n. x ∈ open_ball y (1 / real n) ∧ open_ball y (1 / real n) ⊆ open_ball x ε"
proof(intro bexI[where x=y] exI[where x="2 * N"] conjI)
show "x ∈ open_ball y (1 / real (2 * N))"
using hy(3) by(simp add: open_ball_inverse[of x y])
next
show "open_ball y (1 / real (2 * N)) ⊆ open_ball x ε"
proof
fix y'
assume hy':"y' ∈ open_ball y (1 / real (2 * N))"
have "dist x y' < ε" (is "?lhs < ?rhs")
proof -
have "?lhs ≤ dist x y + dist y y'"
using hy(2) open_ballD'(1)[OF hy'] h(1) by(auto intro!: dist_tr)
also have "... < 1 / real (2 * N) + 1 / real (2 * N)"
apply(rule strict_ordered_ab_semigroup_add_class.add_strict_mono)
using hy(3) hy(2) open_ballD'(1)[OF hy'] h(1) hy' by(simp_all add: open_ball_def dist_sym[of x y])
finally show ?thesis
using hn' by auto
qed
thus "y' ∈ open_ball x ε"
using open_ballD'(1)[OF hy'] h(1) by(simp add: open_ball_def)
qed
qed fact
qed
fix K
assume hk: "K ∈ {open_ball a ε |a ε. a ∈ S ∧ 0 < ε}"
then obtain x εx where hxe:
"x ∈ S" "0 < εx" "K = open_ball x εx" by auto
have gh:"K = (⋃{open_ball y (1 / real n) | y n. y ∈ U ∧ open_ball y (1 / real n) ⊆ K})"
proof
show "K ⊆ (⋃ {open_ball y (1 / real n) |y n. y ∈ U ∧ open_ball y (1 / real n) ⊆ K})"
proof
fix k
assume hkink:"k ∈ K"
then have hkinS:"k ∈ S"
using open_ballD'(1)[of k] by(simp add: hxe)
obtain εk where hek:
"εk > 0" "open_ball k εk ⊆ K"
using mtopology_open_ball_in'[of k x] hkink
by(auto simp: hxe)
obtain y n where hyey:
"y ∈ U" "k ∈ open_ball y (1 / real n)" "open_ball y (1 / real n) ⊆ open_ball k εk"
using h0[OF hkinS hek(1)] by auto
show "k ∈ ⋃ {open_ball y (1 / real n) |y n. y ∈ U ∧ open_ball y (1 / real n) ⊆ K}"
using hek(2) hyey by blast
qed
qed auto
show "openin (topology_generated_by {open_ball y (1 / real n) |y n. y ∈ U}) K"
unfolding openin_topology_generated_by_iff
apply(rule generate_topology_on.UN[of "{open_ball y (1 / real n) |y n. y ∈ U ∧ open_ball y (1 / real n) ⊆ K}", simplified gh[symmetric]])
apply(rule generate_topology_on.Basis) by auto
qed
qed
lemma(in separable_metric_set) second_countable':
"∃𝒪. countable 𝒪 ∧ mtopology_basis 𝒪"
proof -
obtain U where hu:
"countable U" "dense_set U"
using separable by auto
show ?thesis
proof(rule countable_base_from_countable_subbase[where 𝒪="{open_ball y (1 / real n) | y n. y ∈ U}",simplified second_countable_def])
have "{open_ball y (1 / real n) |y n. y ∈ U} = (λ(y,n). open_ball y (1 / real n)) ` (U × UNIV)"
by auto
also have "countable ..."
using hu by auto
finally show "countable {open_ball y (1 / real n) |y n. y ∈ U}" .
qed (simp add: generated_by_countable_balls[OF hu] subbase_of_def)
qed
lemma(in separable_metric_set) second_countable: "second_countable mtopology"
by(simp add: second_countable_def second_countable')
lemma(in metric_set) separable_if_second_countable:
assumes "countable 𝒪" and "mtopology_basis 𝒪"
shows "separable_metric_set S dist"
proof
have 1:"mtopology = topology_generated_by {U ∈ 𝒪. U ≠ {}}"
by(simp add: topology_generated_by_without_empty[symmetric] base_is_subbase[OF assms(2),simplified subbase_of_def])
have "∀U ∈ {U ∈𝒪. U ≠ {} }. ∃x. x ∈ U"
by auto
then have "∃x. ∀U ∈ { U ∈ 𝒪. U ≠ {} }. x U ∈ U"
by(rule bchoice)
then obtain x where hx:
"∀U ∈ { U ∈ 𝒪. U ≠ {} }. x U ∈ U"
by auto
show "∃U. countable U ∧ dense_set U"
proof(intro exI[where x="{ x U | U. U ∈ 𝒪 ∧ U ≠ {}}"] conjI)
have "{x U |U. U ∈ 𝒪 ∧ U ≠ {}} = (λU. x U) ` { U ∈ 𝒪. U ≠ {} }"
by auto
also have "countable ..."
using assms(1) by auto
finally show "countable {x U |U. U ∈ 𝒪 ∧ U ≠ {}}" .
next
show "dense_set {x U |U. U ∈ 𝒪 ∧ U ≠ {}}"
unfolding dense_set_def
proof
have "⋀U. U ∈ 𝒪 ⟹ U ⊆ topspace mtopology"
using assms(2)[simplified base_of_def2']
by(auto intro!: openin_subset)
then show "{x U |U. U ∈ 𝒪 ∧ U ≠ {}} ⊆ S"
using hx by(auto simp add: mtopology_topspace)
next
show "∀xa∈S. ∀ε>0. open_ball xa ε ∩ {x U |U. U ∈ 𝒪 ∧ U ≠ {}} ≠ {}"
proof safe
fix s ε
assume h:"s ∈ S" "(0::real) < ε" "open_ball s ε ∩ {x U |U. U ∈ 𝒪 ∧ U ≠ {}} = {}"
then have "openin mtopology (open_ball s ε)"
by(auto intro!: mtopology_open_ball_in)
moreover have "open_ball s ε ≠ {}"
using h open_ball_ina by blast
ultimately obtain U' where
"U'∈𝒪" "U' ≠ {}" "U' ⊆ open_ball s ε"
using assms(2)[simplified base_of_def] by fastforce
then have "x U' ∈ open_ball s ε ∩ {x U |U. U ∈ 𝒪 ∧ U ≠ {}}"
using hx by blast
with h show False
by auto
qed
qed
qed
qed
lemma metric_generates_same_topology_separable_if:
assumes "metric_set S d" "metric_set S d'"
and "metric_set.mtopology S d = metric_set.mtopology S d'"
and "separable_metric_set S d"
shows "separable_metric_set S d'"
proof -
interpret m1: separable_metric_set S d by fact
interpret m2: metric_set S d' by fact
obtain 𝒪 where "countable 𝒪" "m1.mtopology_basis 𝒪"
using m1.second_countable' by auto
thus ?thesis
by(auto intro!: m2.separable_if_second_countable simp: assms(3)[symmetric])
qed
lemma metric_generates_same_topology_separable:
assumes "metric_set S d" "metric_set S d'"
and "metric_set.mtopology S d = metric_set.mtopology S d'"
shows "separable_metric_set S d ⟷ separable_metric_set S d'"
using metric_generates_same_topology_separable_if[OF assms] metric_generates_same_topology_separable_if[OF assms(2,1) assms(3)[symmetric]]
by auto
lemma(in metric_set) separable_if_totally_bounded:
assumes totally_boundedS
shows "separable_metric_set S dist"
unfolding separable_iff_topological_separable
proof -
have "∃A. finite A ∧ A ⊆ S ∧ S = ⋃ ((λa. open_ball a (1 / real (Suc n))) ` A)" for n
using totally_boundedSD[OF assms,of "1 / Suc n"] by fastforce
then obtain A where A:"⋀n. finite (A n)" "⋀n. A n ⊆ S" "⋀n. S = ⋃ ((λa. open_ball a (1 / real (Suc n))) ` (A n))"
by metis
define K where "K ≡ ⋃ (range A)"
have 1: "countable K"
using A(1) by(auto intro!: countable_UN[of _ id,simplified] simp: K_def countable_finite)
show "separable mtopology"
unfolding dense_set_def2 separable_def
proof(safe intro!: exI[where x=K] 1)
fix x and ε :: real
assume h: "x ∈ S" "0 < ε"
then obtain n where n:"1 / real (Suc n) ≤ ε"
by (meson nat_approx_posE order.strict_iff_not)
then obtain y where y: "y ∈ A n" "x ∈ open_ball y (1 / real (Suc n))"
using h(1) A(3)[of n] by auto
then show "∃y∈K. dist x y < ε"
using open_ballD[OF y(2)] n by(auto intro!: bexI[where x=y] simp: dist_sym[of y x] K_def)
qed(use K_def A(2) in auto)
qed
lemma second_countable_metric_class_separable_set:
"separable_metric_set (UNIV :: 'a ::{metric_space,second_countable_topology} set) dist"
proof -
interpret m: metric_set UNIV dist
by(rule metric_class_metric_set)
obtain B :: "'a set set" where "countable B ∧ topological_basis B"
using second_countable_topology_class.ex_countable_basis by auto
then show ?thesis
by(auto intro!: m.separable_if_second_countable[where 𝒪=B] simp: topological_basis_set)
qed
lemma second_countable_euclidean[simp]:
"second_countable (euclidean :: 'a :: {metric_space,second_countable_topology} topology)"
by (metis euclidean_mtopology second_countable_metric_class_separable_set separable_metric_set.second_countable)
lemma separable_euclidean[simp]:
"separable (euclidean :: 'a :: {metric_space,second_countable_topology} topology)"
by(auto intro!: separable_if_second_countable)
lemma(in separable_metric_set) submetric_separable:
assumes "S' ⊆ S"
shows "separable_metric_set S' (submetric S' dist)"
proof -
interpret m: metric_set S' "submetric S' dist"
by(rule submetric_metric_set[OF assms])
obtain 𝒪 where ho:"countable 𝒪" "mtopology_basis 𝒪"
using second_countable' by auto
show ?thesis
proof(rule m.separable_if_second_countable[where 𝒪="{S' ∩ U | U. U∈𝒪}"])
show "countable {S' ∩ U |U. U ∈ 𝒪}"
using countable_image[where f="(∩) S'",OF ho(1)]
by (simp add: Setcompr_eq_image)
next
show "m.mtopology_basis {S' ∩ U |U. U ∈ 𝒪}"
by(auto simp: submetric_subtopology[OF assms,symmetric] intro!: subtopology_base_of ho(2))
qed
qed
lemma(in separable_metric_set) Lindelof_diam:
assumes "0 < e"
shows "∃U. countable U ∧ ⋃ U = S ∧ (∀u∈U. diam u < ennreal e)"
proof -
have "(⋀u. u ∈ {open_ball x (e / 3) |x. x ∈ S} ⟹ openin mtopology u)"
by(auto simp: openin_open_ball)
moreover have "⋃ {open_ball x (e / 3) |x. x ∈ S} = S"
using open_ball_ina open_ball_subset_ofS assms by auto
ultimately have "∃U'. countable U' ∧ U' ⊆ {open_ball x (e / 3) |x. x ∈ S} ∧ ⋃ U' = S"
by(rule Lindelof_of[OF second_countable,simplified mtopology_topspace]) auto
then obtain U' where U': "countable U'" "U' ⊆ {open_ball x (e / 3) |x. x ∈ S}" "⋃ U' = S"
by auto
show ?thesis
proof(safe intro!: exI[where x=U'])
fix u
assume "u ∈ U'"
then obtain x where u:"u = open_ball x (e / 3)"
using U' by auto
have "diam u ≤ ennreal (2 * (e / 3))"
by(simp only: u diam_ball_leq)
also have "... < ennreal e"
by(auto intro!: ennreal_lessI assms)
finally show "diam u < ennreal e" .
qed(use U' in auto)
qed
subsubsection ‹ Polish Metric Spaces ›
locale polish_metric_set = complete_metric_set + separable_metric_set
lemma polish_class_polish_set[simp]:
"polish_metric_set (UNIV :: 'a :: polish_space set) dist"
using second_countable_metric_class_separable_set complete_space_complete_metric_set
by(simp add: polish_metric_set_def)
lemma(in polish_metric_set) submetric_polish:
assumes "M ⊆ S" and "closedin mtopology M"
shows "polish_metric_set M (submetric M dist)"
using submetric_separable[OF assms(1)] submetric_complete_iff[OF assms(1)]
by(simp add: polish_metric_set_def assms(2))
lemma polish_metric_setI:
assumes "complete_metric_set S d" "separable (metric_set.mtopology S d)"
shows "polish_metric_set S d"
using assms by(auto intro!: separable_metric_setI simp: polish_metric_set_def complete_metric_set_def)
subsubsection ‹ Compact Metric Spaces›
locale compact_metric_set = metric_set +
assumes mtopology_compact:"compact_space mtopology"
begin
context
fixes S' :: "'b set" and dist'
assumes S'_dist: "metric_set S' dist'"
begin
interpretation m': metric_set S' dist' by fact
lemma continuous_map_is_uniform:
assumes "continuous_map mtopology m'.mtopology f"
shows "uniform_continuous_map S dist S' dist' f"
unfolding uniform_continuous_map_def[OF metric_set_axioms m'.metric_set_axioms]
proof safe
show goal1:"⋀x. x ∈ S ⟹ f x ∈ S'"
using assms by(auto simp: continuous_map_def mtopology_topspace m'.mtopology_topspace)
fix e :: real
assume e:"0 < e"
{ fix x
assume x:"x ∈ S"
then have "∃δ>0. ∀y∈S. dist x y < δ ⟶ dist' (f x) (f y) < e / 2"
using assms(1)[simplified metric_set_continuous_map_eq[OF metric_set_axioms m'.metric_set_axioms]] half_gt_zero[OF e]
by metis
}
then obtain δ where delta:"⋀x. x ∈ S ⟹ δ x > 0" "⋀x y. x ∈ S ⟹ y ∈ S ⟹ dist x y < δ x ⟹ dist' (f x) (f y) < e / 2"
by metis
show "∃δ>0. ∀x∈S. ∀y∈S. dist x y < δ ⟶ dist' (f x) (f y) < e"
proof(cases "S = {}")
case True
then show ?thesis
by (auto intro!: exI[where x=1])
next
case nem:False
have "∃ℱ. finite ℱ ∧ ℱ ⊆ {open_ball x (δ x / 2)|x. x ∈ S} ∧ S ⊆ ⋃ ℱ"
using open_ball_ina[OF _ half_gt_zero[OF delta(1)]] mtopology_compact
by(auto intro!: compactinD simp: compact_space_def mtopology_topspace openin_open_ball)
then obtain F where F: "finite F" "F ⊆ {open_ball x (δ x / 2)|x. x ∈ S}" "S ⊆ ⋃ F"
by auto
have F_nem:"F ≠ {}"
using nem F by auto
have "a ∈ F ⟹ (∃x∈S. a = open_ball x (δ x / 2))" for a
using F(2) by auto
then obtain xa where xa:"⋀a. a ∈ F ⟹ xa a ∈ S" "⋀a. a ∈ F ⟹ a = open_ball (xa a) (δ (xa a) / 2)"
by metis
define δ' where "δ' ≡ (MIN a∈F. δ (xa a) / 2)"
have fin:"finite ((λa. δ (xa a)/ 2) ` F)"
using F by auto
have nemd: "((λa. δ (xa a)/ 2) ` F) ≠ {}"
using F_nem by auto
have d_pos: "δ' > 0"
by(auto simp: δ'_def linorder_class.Min_gr_iff[OF fin nemd] intro!: delta(1) xa)
show ?thesis
proof(safe intro!: exI[where x=δ'])
fix x y
assume h:"x ∈ S" "y ∈ S" "dist x y < δ'"
then obtain a where a:"x ∈ a" "a ∈ F"
using F(3) by auto
have "dist (xa a) y ≤ dist (xa a) x + dist x y"
by(auto intro!: dist_tr xa a simp: h)
also have "... < δ' + δ (xa a) / 2"
using h xa(2)[OF a(2)] a(1) open_ballD[of x "xa a"] by fastforce
also have "... ≤ δ (xa a) / 2 + δ (xa a) / 2"
proof -
have "δ' ≤ δ (xa a) / 2"
by(simp only: δ'_def,rule Min.coboundedI[OF fin]) (use a in auto)
thus ?thesis by simp
qed
finally have 2:"dist (xa a) y < δ (xa a)" by simp
have "dist' (f x) (f y) ≤ dist' (f x) (f (xa a)) + dist' (f (xa a)) (f y)"
by(auto intro!: m'.dist_tr goal1 h xa a)
also have "... < e"
proof -
have [simp]:"dist (xa a) x < δ (xa a)"
using a(1) xa[OF a(2)] delta(1) open_ballD by fastforce
have "dist' (f x) (f (xa a)) < e / 2"
by(simp only: m'.dist_sym[where x="f x"],rule delta(2)) (auto intro!: xa a h)
moreover have "dist' (f (xa a)) (f y) < e / 2"
by(rule delta(2)[OF _ _ 2]) (auto intro!: h xa a)
ultimately show ?thesis by simp
qed
finally show "dist' (f x) (f y) < e" .
qed(rule d_pos)
qed
qed
end
lemma totally_bounded: totally_boundedS
unfolding totally_boundedS_def
proof safe
fix ε :: real
assume "0 < ε"
define 𝒰 where "𝒰 ≡ (λa. open_ball a ε) ` S"
have 1: "⋀U. U ∈ 𝒰 ⟹ openin mtopology U"
by(auto simp: 𝒰_def openin_open_ball)
have 2:"⋃ 𝒰 = S"
using open_ball_ina[OF _ ‹0 < ε›] open_ball_subset_ofS
by(auto simp: 𝒰_def)
obtain ℱ where "ℱ ⊆ 𝒰" "finite ℱ" "⋃ ℱ = S"
using 1 2 compact_space[of mtopology,simplified mtopology_compact mtopology_topspace] by metis
then obtain A where "A ⊆ S" "finite A" "⋃ ((λa. open_ball a ε) ` A) = S"
by(simp add: 𝒰_def) (metis finite_subset_image)
thus "∃A. eps_net ε A"
by(auto intro!: exI[where x=A] simp: eps_net_def ‹0 < ε›)
qed
lemma sequentially_compact: sequentially_compact
unfolding sequentially_compact_def
proof safe
fix xn
assume "xn ∈ sequence"
then have xn:"⋀n. xn n ∈ S" by auto
have "¬ (∀x∈S. ∃e>0. finite {n. xn n ∈ open_ball x e})"
proof
assume contr:"∀x∈S. ∃e>0. finite {n. xn n ∈ open_ball x e}"
then obtain e where e: "⋀x. x ∈ S ⟹ e x > 0" "⋀x. x ∈ S ⟹ finite {n. xn n ∈ open_ball x (e x)}"
by metis
define U where "U ≡ {open_ball x (e x)|x. x ∈ S}"
have "⋀u. u ∈ U ⟹ openin mtopology u" "topspace mtopology ⊆ ⋃U"
by(auto simp: U_def openin_open_ball mtopology_topspace open_ball_ina[OF _ e(1)])
then obtain F where F: "finite F" "F ⊆ U" "S ⊆ ⋃ F"
using mtopology_compact compactinD by (metis compact_space_def mtopology_topspace)
then have "finite (⋃f∈F. {n. xn n ∈ f})"
using e(2) by(auto simp: U_def)
moreover have "UNIV = (⋃f∈F. {n. xn n ∈ f})"
using F(3) xn by auto
ultimately show False by simp
qed
then obtain x where x:"x ∈ S" "⋀e. e > 0 ⟹ infinite {n. xn n ∈ open_ball x e}"
by metis
have inf:"infinite {n. n > m ∧ xn n ∈ open_ball x e}" if "e > 0" for e m
proof
assume "finite {n. m < n ∧ xn n ∈ open_ball x e}"
then have "finite ({..m} ∪ {n. m < n ∧ xn n ∈ open_ball x e})"
by auto
moreover have "{n. xn n ∈ open_ball x e} ⊆ {..m} ∪ {n. m < n ∧ xn n ∈ open_ball x e}"
by auto
ultimately show False
using x(2)[OF that] finite_subset by blast
qed
define a where "a ≡ rec_nat (SOME n. xn n ∈ open_ball x 1) (λn an. SOME m. m > an ∧ xn m ∈ open_ball x (1 / Suc n))"
have an: "xn (a n) ∈ open_ball x (1 / n)" if "n > 0" for n
proof(cases n)
case 0
with that show ?thesis by simp
next
case (Suc n)
have [simp]:"a (Suc n) = (SOME m. m > a n ∧ xn m ∈ open_ball x (1 / Suc n))"
by(auto simp: a_def)
obtain m where m:"a n < m" "xn m ∈ open_ball x (1 / (Suc n))"
using inf[of "1 / (real (Suc n))" "a n"] not_finite_existsD by auto
have "a (Suc n) > a n ∧ xn (a (Suc n)) ∈ open_ball x (1 / (Suc n))"
by(simp,rule someI2[of _ m]) (use m in auto)
then show ?thesis
by(simp only: Suc)
qed
have as:"strict_mono a"
unfolding strict_mono_Suc_iff
proof safe
fix n
have [simp]:"a (Suc n) = (SOME m. m > a n ∧ xn m ∈ open_ball x (1 / Suc n))"
by(auto simp: a_def)
obtain m where m:"a n < m" "xn m ∈ open_ball x (1 / (Suc n))"
using inf[of "1 / (real (Suc n))" "a n"] not_finite_existsD by auto
have "a (Suc n) > a n ∧ xn (a (Suc n)) ∈ open_ball x (1 / (Suc n))"
by(simp,rule someI2[of _ m]) (use m in auto)
thus "a n < a (Suc n)" by simp
qed
show "∃a. strict_mono a ∧ convergent_inS (xn ∘ a)"
unfolding convergent_inS_def converge_to_inS_def2'
proof(safe intro!: exI[where x=a] exI[where x=x])
fix e :: real
assume "0 < e"
then obtain N ::nat where N: "N > 0" "1 / N < e"
by (meson nat_approx_posE zero_less_Suc)
show "∃N. ∀n≥N. (xn ∘ a) n ∈ open_ball x e"
proof(safe intro!: exI[where x=N])
fix n
assume n:"n ≥ N"
show "(xn ∘ a) n ∈ open_ball x e"
using order.trans[OF open_ball_le[of "1 / n"] open_ball_le[of "1 / N" e]] N n an[of n] inverse_of_nat_le
by auto
qed
qed(auto simp: simp: as x xn)
qed
lemma polish: "polish_metric_set S dist"
using separable_if_totally_bounded[OF totally_bounded]
by(simp add: polish_metric_set_def complete_metric_set_def complete_metric_set_axioms_def separable_metric_set_def)
(meson Cauchy_inS_def converge_if_Cauchy_and_subconverge convergent_inS_def sequentially_compact sequentially_compact_def)
sublocale polish_metric_set
by(rule polish)
end
lemma(in metric_set) ex_lebesgue_number:
assumes "S ≠ {}" sequentially_compact "⋀u. u ∈ U ⟹ openin mtopology u" "S ⊆ ⋃ U"
shows "∃d>0. ∀a⊆S. diam a < ennreal d ⟶ (∃u∈U. a ⊆ u)"
proof(rule ccontr)
assume "¬ (∃d>0. ∀a⊆S. diam a < ennreal d ⟶ (∃u∈U. a ⊆ u))"
then have "⋀n. ∃a⊆S. diam a < ennreal (1 / Suc n) ∧ (∀x∈U. ¬ a ⊆ x)" by auto
then obtain An where an: "⋀n. An n ⊆ S" "⋀n. diam (An n) < ennreal (1 / Suc n)" "⋀n u. u ∈ U ⟹ ¬ (An n) ⊆ u"
by metis
have "An n ≠ {}" for n
proof
assume "An n = {}"
then have "U = {} ∨ (∀u∈U. u = {})"
using an(3)[of _ n] by auto
thus False
using assms(1,4) by blast
qed
then obtain xn where xn:"⋀n. xn n ∈ An n"
by (meson ex_in_conv)
then have xn':"⋀n. xn n ∈ S" using an by auto
then obtain a x where ax:"strict_mono a" "converge_to_inS (xn ∘ a) x"
using assms(2) by(fastforce simp: sequentially_compact_def convergent_inS_def)
then have x: "x ∈ S" by(auto simp: converge_to_inS_def)
then obtain u where u:"x ∈ u" "u ∈ U"
using assms(4) by auto
obtain e where e:"e > 0" "open_ball x e ⊆ u"
using assms(3)[OF u(2)] u(1) mtopology_openin_iff by fastforce
obtain n ::nat where n: "1 / Suc n < e / 2"
using e(1) half_gt_zero nat_approx_posE by blast
obtain n' where n':"⋀n. n ≥ n' ⟹ xn (a n) ∈ open_ball x (e / 2)"
using e(1) ax(2) by(auto simp: converge_to_inS_def2') (meson half_gt_zero)
define n0 where "n0 ≡ max (a (Suc n)) (a n')"
have n0:"1 / Suc n0 < e / 2" "xn n0 ∈ open_ball x (e / 2)"
proof -
have "Suc n0 ≥ Suc n"
using seq_suble[OF ax(1),of "Suc n"] by (simp add: n0_def)
hence "1 / Suc n0 ≤ 1 / Suc n"
using inverse_of_nat_le by blast
thus "1 / Suc n0 < e / 2"
using n by auto
show "xn n0 ∈ open_ball x (e / 2)"
by (cases "a (Suc n) ≤ a n'") (auto intro!: n' simp: n0_def ax(1) strict_mono_less_eq)
qed
have "An n0 ⊆ open_ball x e"
unfolding open_ball_def
proof safe
fix y
assume y:"y ∈ An n0"
have "dist x y ≤ dist x (xn n0) + dist (xn n0) y"
using y xn' an by(auto intro!: dist_tr simp: x)
also have "... < e / 2 + dist (xn n0) y"
using open_ballD[OF n0(2)] by auto
also have "... ≤ e / 2 + 1 / Suc n0"
using xn[of n0] xn' y an by(auto intro!: diam_is_sup'[OF _ _ order.strict_implies_order[OF an(2)[of n0]],simplified])
also have "... < e"
using n0(1) by auto
finally show "y ∈ (if x ∈ S then {xa ∈ S. dist x xa < e} else {})"
using an(1) x y by auto
qed
hence "An n0 ⊆ u"
using e by auto
with an(3)[OF u(2)] show False by auto
qed
lemma(in metric_set) sequentially_compact_iff1:
"sequentially_compact ⟷ totally_boundedS ∧ complete_metric_set S dist"
proof safe
assume h:sequentially_compact
then show totally_boundedS
using Cauchy_if_convergent_inS by(fastforce simp: totally_boundedS_iff sequentially_compact_def)
show "complete_metric_set S dist"
proof
fix xn
assume 1:"Cauchy_inS xn"
with h obtain a x where 2:"strict_mono a" "converge_to_inS (xn ∘ a) x"
by(fastforce dest: Cauchy_inS_dest1 simp: sequentially_compact_def convergent_inS_def)
thus "convergent_inS xn"
by(auto simp: convergent_inS_def converge_if_Cauchy_and_subconverge[OF 2 1] intro!: exI[where x=x])
qed
next
assume h:"totally_boundedS" "complete_metric_set S dist"
show sequentially_compact
unfolding sequentially_compact_def
proof safe
fix xn
assume "xn ∈ sequence"
then obtain a where a:"strict_mono a" "Cauchy_inS (xn ∘ a)"
using h by(auto simp: totally_boundedS_iff)
thus "∃a. strict_mono a ∧ convergent_inS (xn ∘ a)"
using h by(auto intro!: exI[where x=a] simp: complete_metric_set_def complete_metric_set_axioms_def)
qed
qed
lemma(in metric_set) sequentially_compact_compact:
assumes sequentially_compact
shows "compact_metric_set S dist"
proof
show "compact_space mtopology"
proof(cases "S = {}")
case True
have [simp]:"topspace mtopology = {}"
by(simp add: mtopology_topspace,fact)
show ?thesis
by(auto simp: compact_space intro!: exI[where x="{}"])
next
case 1:False
{
fix U
assume h:"⋀u. u ∈ U ⟹ openin mtopology u" "S ⊆ ⋃ U"
obtain d where d:"d > 0" "⋀a. a ⊆ S ⟹ diam a < ennreal d ⟹ ∃u∈U. a ⊆ u"
using ex_lebesgue_number[OF 1 assms h] by metis
obtain B where B:"finite B" "B ⊆ S" "S = (⋃a∈B. open_ball a (d / 3))"
using totally_boundedSD[of "d / 3"] d(1) assms
by(auto simp: sequentially_compact_iff1)
have "∃u∈U. open_ball b (d / 3) ⊆ u" if "b ∈ B" for b
using open_ballD' d(1) by(auto intro!: d(2) order.strict_trans1[OF diam_ball_leq[of b "d / 3"]] simp: ennreal_less_iff)
then obtain u where u:"⋀b. b ∈ B ⟹ u b ∈ U" "⋀b. b ∈ B ⟹ open_ball b (d / 3) ⊆ u b"
by metis
have "∃F. finite F ∧ F ⊆ U ∧ S ⊆ (⋃ F)"
using B u by(fastforce intro!: exI[where x="u ` B"])
}
thus ?thesis
by (simp add: compact_space_alt mtopology_topspace)
qed
qed
corollary(in metric_set) compact_iff_sequentially_compact:
"compact_space mtopology ⟷ sequentially_compact"
using compact_metric_set.sequentially_compact sequentially_compact_compact compact_metric_set_axioms_def compact_metric_set_def metric_set_axioms
by blast
corollary(in metric_set) compact_iff2:
"compact_space mtopology ⟷ totally_boundedS ∧ complete_metric_set S dist"
by(simp add: compact_iff_sequentially_compact sequentially_compact_iff1)
corollary(in complete_metric_set) compactin_closed_iff:
assumes "closedin mtopology C"
shows "compactin mtopology C ⟷ totally_bounded_on C"
proof -
from assms have C:"C ⊆ S"
using mtopology_closedin_iff by blast
then interpret C: complete_metric_set C "submetric C dist"
by(auto simp: submetric_complete_iff assms)
show ?thesis
by(simp add: compactin_subspace submetric_subtopology[OF C] totally_bounded_on_submetric[OF C] mtopology_topspace C C.compact_iff2 C.complete_metric_set_axioms)
qed
subsubsection ‹ Completion ›
context metric_set
begin
abbreviation "Cauchys ≡ Collect Cauchy_inS"
definition Cauchy_r :: "((nat ⇒ 'a) × (nat ⇒ 'a)) set" where
"Cauchy_r ≡ {(xn,yn)|xn yn. Cauchy_inS xn ∧ Cauchy_inS yn ∧ (λn. dist (xn n) (yn n)) ⇢ 0}"
lemma Cauchy_r_equiv[simp]: "equiv Cauchys Cauchy_r"
proof(rule equivI)
show "refl_on Cauchys Cauchy_r"
by(auto simp: refl_on_def Cauchy_r_def)
next
show "sym Cauchy_r"
using dist_sym by(auto simp: sym_def Cauchy_r_def)
next
show "trans Cauchy_r"
proof(rule transI)
show "⋀x y z. (x, y) ∈ Cauchy_r ⟹ (y, z) ∈ Cauchy_r ⟹ (x, z) ∈ Cauchy_r"
unfolding Cauchy_r_def
proof safe
fix xn yn zn
assume h:"Cauchy_inS xn" "Cauchy_inS yn" "Cauchy_inS zn"
"(λn. dist (xn n) (yn n)) ⇢ 0" "(λn. dist (yn n) (zn n)) ⇢ 0"
then show "∃xn' yn'. (xn, zn) = (xn', yn') ∧ Cauchy_inS xn' ∧ Cauchy_inS yn' ∧ (λn. dist (xn' n) (yn' n)) ⇢ 0"
by(auto intro!: tendsto_0_le[OF tendsto_add_zero[OF h(4,5)],of _ 1] dist_tr eventuallyI simp: dist_geq0 Cauchy_inS_dest1)
qed
qed
qed
abbreviation S_completion :: "(nat ⇒ 'a) set set" ("S⇧*") where
"S_completion ≡ Cauchys // Cauchy_r"
lemma S_c_represent:
assumes "X ∈ S⇧*"
obtains xn where "xn ∈ X" "Cauchy_inS xn"
using equiv_Eps_in[OF _ assms] equiv_Eps_preserves[OF _ assms] by auto
lemma Cauchy_inS_ignore_initial_eq:
assumes "Cauchy_inS xn"
shows "(xn, (λn. xn (n + k))) ∈ Cauchy_r"
by(auto simp: Cauchy_r_def Cauchy_inS_ignore_initial[OF assms] assms,insert assms)
(auto simp: LIMSEQ_def dist_real_def dist_geq0 Cauchy_inS_def,metis add.commute trans_le_add2)
corollary Cauchy_inS_r: "a ∈ S ⟹ (λn. a, λn. a) ∈ Cauchy_r"
by(auto intro!: Cauchy_inS_ignore_initial_eq Cauchy_inS_const)
abbreviation dist_completion' :: "[nat ⇒ 'a, nat ⇒ 'a] ⇒ real" where
"dist_completion' xn yn ≡ lim (λn. dist (xn n) (yn n))"
lemma dist_of_completion_congruent2: "dist_completion' respects2 Cauchy_r"
proof(safe intro!: congruent2_commuteI[OF Cauchy_r_equiv])
fix xn yn zn
assume h:"(xn,yn) ∈ Cauchy_r" "Cauchy_inS zn"
then have h':"Cauchy_inS xn" "Cauchy_inS yn" "(λn. dist (xn n) (yn n)) ⇢ 0"
by(auto simp: Cauchy_r_def)
have 1:"(λn. dist (zn n) (xn n)) ⇢ lim (λn. dist (zn n) (xn n))"
using Cauchy_inS_dist_convergent[OF h(2) h'(1)] by(simp add: convergent_LIMSEQ_iff)
have 2:"(λn. dist (zn n) (yn n)) ⇢ lim (λn. dist (zn n) (xn n))"
using h(2) h'(1,2) dist_tr_abs[of "zn _" "xn _" "yn _",simplified abs_diff_le_iff]
by(auto intro!: real_tendsto_sandwich[OF _ _ tendsto_diff[OF 1 h'(3),simplified] tendsto_add[OF 1 h'(3),simplified]] eventuallyI dist_tr dest: Cauchy_inS_dest1) (simp add: Cauchy_inS_dest1 add.commute diff_le_eq)
show "dist_completion' zn xn = dist_completion' zn yn"
using 1 2 by(auto dest: limI)
qed(auto simp: dist_sym)
definition dist_completion :: "[(nat ⇒ 'a) set, (nat ⇒ 'a) set] ⇒ real" ("dist⇧*") where
"dist⇧* X Y ≡ (if X ∈ S⇧* ∧ Y ∈ S⇧* then dist_completion' (SOME xn. xn ∈ X) (SOME yn. yn ∈ Y) else 0)"
lemma dist_c_def:
assumes "xn ∈ X" "yn ∈ Y" "X ∈ S⇧*" "Y ∈ S⇧*"
shows "dist⇧* X Y = dist_completion' xn yn"
by(auto simp: assms dist_completion_def,rule someI2[of "λx. x ∈ X",OF assms(1)],rule someI2[of "λx. x ∈ Y",OF assms(2)])
(auto simp: congruent2D[OF dist_of_completion_congruent2 quotient_eq_iff[OF _ assms(3,3,1),simplified] quotient_eq_iff[OF _ assms(4,4,2),simplified]])
lemma completion_metric_set: "metric_set S⇧* dist⇧*"
proof
fix X Y
consider "X ∈ S⇧*" "Y ∈ S⇧*" | "X ∉ S⇧*" | "Y ∉ S⇧*" by blast
then show "0 ≤ dist⇧* X Y"
proof cases
case 1
then obtain xn yn where h: "xn ∈ X" "yn ∈ Y" "Cauchy_inS xn" "Cauchy_inS yn"
by (meson S_c_represent)
with 1 show ?thesis
by(auto simp: dist_c_def intro!: Lim_bounded2[OF Cauchy_inS_dist_convergent[OF h(3,4),simplified convergent_LIMSEQ_iff]] dist_geq0)
qed(auto simp: dist_completion_def)
next
fix X Y
show "dist⇧* X Y = dist⇧* Y X"
by(auto simp: dist_completion_def dist_sym)
next
fix X Y
assume h:"X ∈ S⇧*" "Y ∈ S⇧*"
then obtain xn yn where h': "xn ∈ X" "yn ∈ Y" "Cauchy_inS xn" "Cauchy_inS yn"
by (meson S_c_represent)
show "X = Y ⟷ dist⇧* X Y = 0"
proof
assume "X = Y"
then show "dist⇧* X Y = 0"
using h' h by(auto simp: dist_c_def)
next
assume "dist⇧* X Y = 0"
then have "(xn, yn) ∈ Cauchy_r"
using h h' convergent_LIMSEQ_iff[THEN iffD1,OF Cauchy_inS_dist_convergent[OF h'(3,4)]]
by(auto simp: dist_c_def Cauchy_r_def)
thus "X = Y"
by(simp add: quotient_eq_iff[OF _ h h'(1,2)])
qed
next
fix X Y Z
assume h:"X ∈ S⇧*" "Y ∈ S⇧*" "Z ∈ S⇧*"
then obtain xn yn zn where h': "xn ∈ X" "yn ∈ Y" "zn ∈ Z" "Cauchy_inS xn" "Cauchy_inS yn" "Cauchy_inS zn"
by (meson S_c_represent)
have "dist⇧* X Z = dist_completion' xn zn"
using h h' by(simp add: dist_c_def)
also have "... ≤ lim (λn. dist (xn n) (yn n) + dist (yn n) (zn n))"
using h' by(auto intro!: lim_mono[OF _ convergent_LIMSEQ_iff[THEN iffD1,OF Cauchy_inS_dist_convergent[OF h'(4,6)]] convergent_LIMSEQ_iff[THEN iffD1,OF convergent_add[OF Cauchy_inS_dist_convergent[OF h'(4,5)] Cauchy_inS_dist_convergent[OF h'(5,6)]]]] dist_tr dest: Cauchy_inS_dest1)
also have "... = dist_completion' xn yn + dist_completion' yn zn"
using tendsto_add[OF convergent_LIMSEQ_iff[THEN iffD1,OF Cauchy_inS_dist_convergent[OF h'(4,5)]] convergent_LIMSEQ_iff[THEN iffD1,OF Cauchy_inS_dist_convergent[OF h'(5,6)]]]
by(simp add: limI)
also have "... = dist⇧* X Y + dist⇧* Y Z"
using h h' by(simp add: dist_c_def)
finally show "dist⇧* X Z ≤ dist⇧* X Y + dist⇧* Y Z" .
qed(simp add: dist_completion_def)
interpretation c:metric_set "S⇧*" "dist⇧*"
by(rule completion_metric_set)
definition into_S_c :: "'a ⇒ (nat ⇒ 'a) set" where
"into_S_c a ≡ Cauchy_r `` {(λn. a)}"
lemma into_S_c_in:
assumes "a ∈ S"
shows "(λn. a) ∈ into_S_c a"
using Cauchy_inS_const[OF assms] Cauchy_inS_r[OF assms]
by(auto simp: into_S_c_def)
lemma into_S_c_into:
assumes "a ∈ S"
shows "into_S_c a ∈ S⇧*"
by(auto simp: into_S_c_def intro!: quotientI Cauchy_if_convergent_inS convergent_inS_const assms)
lemma into_S_inj: "inj_on into_S_c S"
proof
fix x y
assume "x ∈ S" "y ∈ S" "into_S_c x = into_S_c y"
with eq_equiv_class_iff[THEN iffD1,OF Cauchy_r_equiv _ _ this(3)[simplified into_S_c_def]]
have "(λn. x, λn. y) ∈ Cauchy_r"
by(auto simp: Cauchy_if_convergent_inS convergent_inS_const)
thus "x = y"
using dist_0[OF ‹x ∈ S› ‹y ∈ S›]
by(auto simp: Cauchy_r_def LIMSEQ_const_iff)
qed
lemma dist_into_S_c:
assumes "x ∈ S" "y ∈ S"
shows "dist⇧* (into_S_c x) (into_S_c y) = dist x y"
using into_S_c_in[OF assms(1)] into_S_c_in[OF assms(2)] into_S_c_into[OF assms(1)] into_S_c_into[OF assms(2)]
by(simp add: dist_c_def)
lemma S_c_isometry:
"c.ed into_S_c S = dist"
by standard+ (auto simp: c.embed_dist_on_def dist_into_S_c dist_notin dist_notin')
corollary mtopology_embedding_S_c_map:
"homeomorphic_map mtopology (subtopology c.mtopology (into_S_c ` S)) into_S_c"
using into_S_c_into by(auto intro!: c.embed_dist_topology_homeomorphic_map[OF _ into_S_inj,simplified S_c_isometry])
corollary mtopology_embedding_S_c:
"mtopology homeomorphic_space subtopology c.mtopology (into_S_c ` S)"
using mtopology_embedding_S_c_map homeomorphic_space by blast
lemma into_S_c_image_dense: "c.dense_set (into_S_c ` S)"
unfolding c.dense_set_def2'
proof safe
fix X
assume X:"X ∈ S⇧*"
from S_c_represent[OF this] obtain xn where xn:"xn ∈ X" "Cauchy_inS xn"
by auto
show "∃f∈UNIV → into_S_c ` S. c.converge_to_inS f X"
proof(safe intro!: bexI[where x="λn. into_S_c (xn n)"])
show "c.converge_to_inS (λn. into_S_c (xn n)) X"
unfolding c.converge_to_inS_def2
proof safe
fix e :: real
assume e:"e > 0"
then obtain N where N:"⋀n m. n ≥ N ⟹ m ≥ N ⟹ dist (xn n) (xn m) < e / 2"
using xn(2) by (meson Cauchy_inS_def half_gt_zero)
show "∃N. ∀n≥N. dist⇧* (into_S_c (xn n)) X < e"
proof(safe intro!: exI[where x=N])
fix n
assume n:"N ≤ n"
have "dist⇧* (into_S_c (xn n)) X = dist_completion' (λna. xn n) xn"
by(rule dist_c_def[OF into_S_c_in[OF Cauchy_inS_dest1[OF xn(2),of n]] xn(1) into_S_c_into[OF Cauchy_inS_dest1[OF xn(2),of n]] X])
also have "... ≤ e / 2"
by(rule Lim_bounded[OF Cauchy_inS_dist_convergent[OF Cauchy_inS_const[OF Cauchy_inS_dest1[OF xn(2),of n]] xn(2),simplified convergent_LIMSEQ_iff],of N "e/2"],auto dest: N[OF n])
also have "... < e"
using e by auto
finally show "dist⇧* (into_S_c (xn n)) X < e" .
qed
qed(auto simp: Cauchy_inS_dest1[OF xn(2)] into_S_c_into X)
qed(auto simp: Cauchy_inS_dest1[OF xn(2)] into_S_c_into)
qed (use into_S_c_into in auto)
lemma completion_complete:"complete_metric_set S⇧* dist⇧*"
proof
fix Xn
assume h:"c.Cauchy_inS Xn"
have "⋀n. ∃xn∈S. dist⇧* (Xn n) (into_S_c xn) < 1 / (Suc n)"
using into_S_c_image_dense c.Cauchy_inS_dest1[OF h]
by(auto simp: c.dense_set_def2)
then obtain xn where xn: "⋀n. xn n ∈ S" "⋀n. dist⇧* (Xn n) (into_S_c (xn n)) < 1 / (Suc n)"
by metis
have xnC:"Cauchy_inS xn"
unfolding Cauchy_inS_def
proof safe
fix e :: real
assume e:"0 < e"
then obtain N1 where N1: "1 / Suc N1 < e / 3"
by (meson nat_approx_posE zero_less_divide_iff zero_less_numeral)
obtain N2 where N2: "⋀n m. n ≥ N2 ⟹ m ≥ N2 ⟹ dist⇧* (Xn n) (Xn m) < e / 3"
using e h by(simp only: c.Cauchy_inS_def) (meson zero_less_divide_iff zero_less_numeral)
show "∃N. ∀n≥N. ∀m≥N. dist (xn n) (xn m) < e"
proof(safe intro!: exI[where x="max N1 N2"])
fix n m
assume "max N1 N2 ≤ n" "max N1 N2 ≤ m"
hence n: "N1 ≤ n" "N2 ≤ n"
and m: "N1 ≤ m" "N2 ≤ m" by auto
have "dist (xn n) (xn m) = c.ed into_S_c S (xn n) (xn m)"
by(simp add: S_c_isometry)
also have "... = dist⇧* (into_S_c (xn n)) (into_S_c (xn m))"
using xn by(simp add: c.embed_dist_on_def)
also have "... ≤ dist⇧* (into_S_c (xn n)) (Xn n) + dist⇧* (Xn n) (Xn m) + dist⇧* (Xn m) (into_S_c (xn m))"
using c.dist_tr[OF into_S_c_into[OF xn(1)[of n]] c.Cauchy_inS_dest1[OF h,of m] into_S_c_into[OF xn(1)[of m]]] c.dist_tr[OF into_S_c_into[OF xn(1)[of n]] c.Cauchy_inS_dest1[OF h,of n] c.Cauchy_inS_dest1[OF h,of m]]
by simp
also have "... < 1 / Suc n + e / 3 + 1 / Suc m"
using N2[OF n(2) m(2)] xn(2)[of m] xn(2)[of n,simplified c.dist_sym[of "Xn n"]] by auto
also have "... < e"
proof -
have "1 / Suc n ≤ 1 / Suc N1" "1 / Suc m ≤ 1 / Suc N1"
using n m inverse_of_nat_le by blast+
thus ?thesis
using N1 by linarith
qed
finally show "dist (xn n) (xn m) < e" .
qed
qed(simp add: xn)
show "c.convergent_inS Xn"
unfolding c.convergent_inS_def c.converge_to_inS_def2
proof(safe intro!: exI[where x="Cauchy_r `` {xn}"] quotientI xnC)
fix e :: real
assume e:"0 < e"
then obtain N1 where N1: "1 / Suc N1 < e / 2"
by (meson nat_approx_posE zero_less_divide_iff zero_less_numeral)
hence 1:"dist⇧* (Xn n) (into_S_c (xn n)) < e / 2" if "n ≥ N1" for n
proof -
have "1 / Suc n ≤ 1 / Suc N1"
using that inverse_of_nat_le by blast
thus ?thesis
using xn(2)[of n] N1 by linarith
qed
then obtain N2 where N2:"⋀n m. n ≥ N2 ⟹ m ≥ N2 ⟹ dist (xn n) (xn m) < e / 3"
using xnC e by (meson Cauchy_inS_def zero_less_divide_iff zero_less_numeral)
have 2:"dist⇧* (into_S_c (xn n)) (Cauchy_r `` {xn}) < e / 2" if "n ≥ N2" for n
proof -
have "dist⇧* (into_S_c (xn n)) (Cauchy_r `` {xn}) = dist_completion' (λm. xn n) xn"
using dist_c_def[OF into_S_c_in[OF Cauchy_inS_dest1[OF xnC,of n]] equiv_class_self[OF Cauchy_r_equiv,of xn] into_S_c_into[OF Cauchy_inS_dest1[OF xnC,of n]]] xnC
by (simp add: quotientI)
also have "... ≤ e / 3"
by(rule Lim_bounded[OF Cauchy_inS_dist_convergent[OF Cauchy_inS_const[OF Cauchy_inS_dest1[OF xnC,of n]] xnC,simplified convergent_LIMSEQ_iff],of N2 "e/3"], auto dest: N2[OF that])
also have "... < e / 2" using e by simp
finally show "dist⇧* (into_S_c (xn n)) (Cauchy_r `` {xn}) < e / 2" .
qed
show "∃N. ∀n≥N. dist⇧* (Xn n) (Cauchy_r `` {xn}) < e"
proof(safe intro!: exI[where x="max N1 N2"])
fix n
assume "max N1 N2 ≤ n"
then have n:"n ≥ N1" "n ≥ N2" by auto
show "dist⇧* (Xn n) (Cauchy_r `` {xn}) < e"
using c.dist_tr[OF c.Cauchy_inS_dest1[OF h,of n] into_S_c_into[OF Cauchy_inS_dest1[OF xnC],of n] quotientI[of xn]] xnC 1[OF n(1)] 2[OF n(2)]
by auto
qed
qed(use c.Cauchy_inS_dest1[OF h] in auto)
qed
lemma dense_set_c_dense:
assumes "dense_set U"
shows "c.dense_set (into_S_c ` U)"
unfolding c.dense_set_def2
proof safe
fix X and e :: real
assume h:"X ∈ S⇧*" "0 < e"
then obtain xn where xn:"xn ∈ X" "Cauchy_inS xn"
by(auto dest: S_c_represent)
obtain y where y:"y ∈ S" "dist⇧* X (into_S_c y) < e / 2"
using h into_S_c_image_dense half_gt_zero[OF h(2)] by(simp only: c.dense_set_def2) blast
obtain z where z:"z ∈ U" "dist y z < e / 2"
using half_gt_zero[OF h(2)] y(1) assms by(simp only: dense_set_def2) blast
show "∃y∈into_S_c ` U. dist⇧* X y < e"
proof(rule bexI[OF _ imageI[OF z(1)]])
have "dist⇧* X (into_S_c z) ≤ dist⇧* X (into_S_c y) + dist⇧* (into_S_c y) (into_S_c z)"
using z(1) assms by(auto intro!: c.dist_tr h into_S_c_into y simp: dense_set_def)
also have "... = dist⇧* X (into_S_c y) + dist y z"
using z(1) assms y(1) dist_into_S_c[of y z] by(auto simp: dense_set_def)
also have "... < e"
using y(2) z(2) by simp
finally show "dist⇧* X (into_S_c z) < e" .
qed
qed(insert assms, auto simp: dense_set_def intro!: into_S_c_into)
end
lemma(in separable_metric_set) completion_polish: "polish_metric_set S⇧* dist⇧*"
proof -
interpret c:complete_metric_set "S⇧*" "dist⇧*"
by(rule completion_complete)
show ?thesis
proof
obtain U where U: "countable U" "dense_set U"
using separable by blast
show "∃U. countable U ∧ c.dense_set U"
using U by(auto intro!: exI[where x="into_S_c ` U"] dense_set_c_dense)
qed
qed
subsection ‹Discrete Distance›
definition discrete_dist :: "'a set ⇒ 'a ⇒ 'a ⇒ real" where
"discrete_dist S ≡ (λa b. if a ∈ S ∧ b ∈ S ∧ a ≠ b then 1 else 0)"
lemma
assumes "a ∈ S" and "b ∈ S"
shows discrete_dist_iff_1: "discrete_dist S a b = 1 ⟷ a ≠ b"
and discrete_dist_iff_0: "discrete_dist S a b = 0 ⟷ a = b"
using assms by(auto simp: discrete_dist_def)
lemma discrete_dist_metric:
"metric_set S (discrete_dist S)"
by(auto simp: discrete_dist_def metric_set_def)
lemma
shows discrete_dist_ball_ge1: "x ∈ S ⟹ 1 < ε ⟹ metric_set.open_ball S (discrete_dist S) x ε = S"
and discrete_dist_ball_leq1: "x ∈ S ⟹ 0 < ε ⟹ ε ≤ 1 ⟹ metric_set.open_ball S (discrete_dist S) x ε = {x}"
apply(auto simp: metric_set.open_ball_def[OF discrete_dist_metric],simp_all add: discrete_dist_def)
using less_le_not_le by fastforce
lemma discrete_dist_complete_metric:
"complete_metric_set S (discrete_dist S)"
proof -
interpret m: metric_set S "discrete_dist S"
by(rule discrete_dist_metric)
show ?thesis
proof
fix f
assume h:"m.Cauchy_inS f"
then have "⋀ε. ε>0 ⟹ ∃x∈S. ∃N. ∀n≥N. f n ∈ m.open_ball x ε"
by(auto simp: m.Cauchy_inS_def2')
from this[of 1] obtain x N where hxn:
"x ∈ S" "∀n≥N. f n ∈ m.open_ball x 1"
by auto
hence "⋀n. n ≥ N ⟹ f n = x"
using discrete_dist_ball_leq1[of x S 1] by auto
thus "m.convergent_inS f"
unfolding m.convergent_inS_def using h hxn(1)
by(auto intro!: bexI[where x=x] exI[where x=N] simp:m.converge_to_inS_def2' m.Cauchy_inS_def)
qed
qed
lemma discrete_dist_dense_set:
"metric_set.dense_set S (discrete_dist S) U ⟷ S = U"
proof -
interpret m: metric_set S "discrete_dist S"
by(rule discrete_dist_metric)
show ?thesis
proof
assume h:"m.dense_set U"
show "S = U"
proof safe
fix x
assume hx:"x ∈ S"
then have "⋀ε. ε>0 ⟹ m.open_ball x ε ∩ U ≠ {}"
using h by(simp add: m.dense_set_def)
hence "m.open_ball x 1 ∩ U ≠ {}" by auto
thus "x ∈ U"
using discrete_dist_ball_leq1[OF hx,of 1]
by auto
next
show "⋀x. x ∈ U ⟹ x ∈ S"
using h by(auto simp: m.dense_set_def)
qed
next
show "S = U ⟹ m.dense_set U "
using m.dense_set_S by auto
qed
qed
lemma discrete_dist_separable_iff:
"separable_metric_set S (discrete_dist S) ⟷ countable S"
proof -
interpret m: metric_set S "discrete_dist S"
by(rule discrete_dist_metric)
show ?thesis
proof
assume "separable_metric_set S (discrete_dist S)"
then obtain U where "countable U" "m.dense_set U"
by(auto simp: separable_metric_set_def separable_metric_set_axioms_def)
thus "countable S"
using discrete_dist_dense_set[of S] by auto
next
assume "countable S"
then show "separable_metric_set S (discrete_dist S)"
by(auto simp: separable_metric_set_def separable_metric_set_axioms_def intro!:exI[where x=S] m.dense_set_S discrete_dist_metric)
qed
qed
lemma discrete_dist_polish_iff: "polish_metric_set S (discrete_dist S) ⟷ countable S"
using discrete_dist_separable_iff[of S] discrete_dist_complete_metric[of S]
by(auto simp: polish_metric_set_def)
lemma discrete_dist_topology_x:
assumes "x ∈ S"
shows "openin (metric_set.mtopology S (discrete_dist S)) {x}"
proof -
interpret m: metric_set S "discrete_dist S"
by(rule discrete_dist_metric)
show ?thesis
by(auto simp: m.mtopology_open_ball_in[OF assms,of 1, simplified discrete_dist_ball_leq1[OF assms]])
qed
lemma discrete_dist_topology:
"openin (metric_set.mtopology S (discrete_dist S)) U ⟷ U ⊆ S"
proof -
interpret m: metric_set S "discrete_dist S"
by(rule discrete_dist_metric)
show ?thesis
proof
show "openin m.mtopology U ⟹ U ⊆ S"
using m.mtopology_topspace
by(auto simp: topspace_def)
next
assume "U ⊆ S"
then have "⋀x. x ∈ U ⟹ openin m.mtopology {x}"
by(auto simp: discrete_dist_topology_x)
hence "openin m.mtopology (⋃{{x} | x. x ∈ U})"
by auto
moreover have "⋃{{x} | x. x ∈ U} = U" by blast
ultimately show "openin m.mtopology U"
by simp
qed
qed
lemma discrete_dist_topology':
"metric_set.mtopology S (discrete_dist S) = discrete_topology S"
by (simp add: discrete_dist_topology topology_eq)
text ‹ Empty space. ›
lemma empty_metric_compact: "compact_metric_set {} (λx y. 0)"
proof -
interpret metric_set "{}" "λx y. 0"
by(auto simp: metric_set_def)
show ?thesis
by standard (use Hausdorff_space_finite_topspace[OF mtopology_Hausdorff,simplified mtopology_topspace] in blast)
qed
corollary
shows empty_metric_polish: "polish_metric_set {} (λx y. 0)"
and empty_metric_complete: "complete_metric_set {} (λx y. 0)"
and empty_metric_separable: "separable_metric_set {} (λx y. 0)"
and empty_metric: "metric_set {} (λx y. 0)"
proof -
interpret compact_metric_set "{}" "λx y. 0"
by(rule empty_metric_compact)
show "polish_metric_set {} (λx y. 0)" "complete_metric_set {} (λx y. 0)"
"separable_metric_set {} (λx y. 0)" "metric_set {} (λx y. 0)"
using polish_metric_set_axioms complete_metric_set_axioms separable_metric_set_axioms metric_set_axioms
by blast+
qed
lemma empty_metric_unique:
assumes "metric_set {} d"
shows "d = (λx y. 0)"
apply standard+
using assms by(auto simp: metric_set_def)
lemma empty_metric_mtopology:
"metric_set.mtopology {} (λx y. 0) = discrete_topology {}"
proof -
have 1:"(λU. U = {} ∧ (∀x∈U. ∃ε>0. metric_set.open_ball {} (λx y. 0) x ε ⊆ U)) = (λU. U = {})"
by standard auto
thus ?thesis
using metric_set.mtopology_def[of "{}" "λx y. 0"]
by(simp add: metric_set_def discrete_topology_def 1)
qed
text ‹ Singleton space ›
lemma singleton_metric_compact:
"compact_metric_set {a} (λx y. 0)"
proof -
interpret metric_set "{a}" "λx y. 0"
by(auto simp: metric_set_def)
show ?thesis
by standard (use Hausdorff_space_finite_topspace[OF mtopology_Hausdorff,simplified mtopology_topspace] in blast)
qed
corollary
shows singleton_metric_polish: "polish_metric_set {a} (λx y. 0)"
and singleton_metric_complete: "complete_metric_set {a} (λx y. 0)"
and singleton_metric_separable: "separable_metric_set {a} (λx y. 0)"
and singleton_metric: "metric_set {a} (λx y. 0)"
proof -
interpret compact_metric_set "{a}" "λx y. 0"
by(rule singleton_metric_compact)
show "polish_metric_set {a} (λx y. 0)" "complete_metric_set {a} (λx y. 0)"
"separable_metric_set {a} (λx y. 0)" "metric_set {a} (λx y. 0)"
using polish_metric_set_axioms complete_metric_set_axioms separable_metric_set_axioms metric_set_axioms
by blast+
qed
lemma singleton_metric_unique:
assumes "metric_set {a} d"
shows "d = (λx y. 0)"
by standard+ (insert assms,auto simp: metric_set_def, metis)
lemma singleton_metric_mtopology:
"metric_set.mtopology {a} (λx y. 0) = discrete_topology {a}"
proof -
have "(λU. U ⊆ {a} ∧ (∀x∈U. ∃ε>0. metric_set.open_ball {a} (λx y. 0) x ε ⊆ U)) = (λU. U ⊆ {a})"
proof
fix U
have "(U ⊆ {a} ∧ (∀x∈U. ∃ε>0. metric_set.open_ball {a} (λx y. 0) x ε ⊆ U))" if "U ⊆ {a}"
proof safe
fix x
assume "x ∈ U"
then have "x = a" using that by auto
thus "∃ε>0. metric_set.open_ball {a} (λx y. 0) x ε ⊆ U"
by(auto intro!: exI[where x=1]) (metis ‹x ∈ U› complete_metric_set_def empty_iff metric_set.open_ballD'(1) polish_metric_set_def singleton_metric_polish subset_singletonD that)
qed(use that in auto)
thus "(U ⊆ {a} ∧ (∀x∈U. ∃ε>0. metric_set.open_ball {a} (λx y. 0) x ε ⊆ U)) = (U ⊆ {a})"
by auto
qed
thus ?thesis
using metric_set.mtopology_def[of "{a}" "λx y. 0"]
by(simp add: metric_set_def discrete_topology_def )
qed
subsection ‹Binary Product Metric Spaces›
text ‹ We define the $L^{1}$-distance. $L^{1}$-distance and $L^{2}$ distance (Euclid distance)
generate the same topological space.›
definition binary_distance :: "['a set, 'a ⇒ 'a ⇒ real, 'b set, 'b ⇒ 'b ⇒ real] ⇒ 'a × 'b ⇒ 'a × 'b ⇒ real" where
"binary_distance S d S' d' ≡ (λ(x,x') (y,y'). if (x,x') ∈ S × S' ∧ (y,y') ∈ S × S' then d x y + d' x' y' else 0)"
context
fixes S S' d d'
assumes "metric_set S d" "metric_set S' d'"
begin
interpretation m1: metric_set S d by fact
interpretation m2: metric_set S' d' by fact
lemma binary_metric_set:
"metric_set (S × S') (binary_distance S d S' d')"
proof
fix x y z
assume "x ∈ S × S'" "y ∈ S × S'" "z ∈ S × S'"
then show "binary_distance S d S' d' x z ≤ binary_distance S d S' d' x y + binary_distance S d S' d' y z"
using m1.dist_tr[of "fst x" "fst y" "fst z"] m2.dist_tr[of "snd x" "snd y" "snd z"]
by(fastforce simp: binary_distance_def split_beta')
next
show "⋀x y. 0 ≤ binary_distance S d S' d' x y"
"⋀x y. x ∉ S × S' ⟹ binary_distance S d S' d' x y = 0"
using m1.dist_geq0 m2.dist_geq0 m1.dist_notin m2.dist_notin by(auto simp: binary_distance_def split_beta')
next
fix x y
assume "x ∈ S × S'" "y ∈ S × S'"
then show "(x = y) = (binary_distance S d S' d' x y = 0)"
using m1.dist_0[of "fst x" "fst y"] m2.dist_0[of "snd x" "snd y"] m1.dist_geq0[of "fst x" "fst y"] m2.dist_geq0[of "snd x" "snd y"]
by(auto simp: binary_distance_def split_beta)
next
show "⋀x y. binary_distance S d S' d' x y = binary_distance S d S' d' y x"
using m1.dist_sym m2.dist_sym by(auto simp: binary_distance_def split_beta')
qed
interpretation m: metric_set "S × S'" "binary_distance S d S' d'"
by (rule binary_metric_set)
lemma binary_distance_geq:
assumes "x ∈ S" "y ∈ S" "x' ∈ S'" "y' ∈ S'"
shows "d x y ≤ binary_distance S d S' d' (x,x') (y,y')"
"d' x' y' ≤ binary_distance S d S' d' (x,x') (y,y')"
using m1.dist_geq0 m2.dist_geq0 assms by(auto simp: binary_distance_def)
lemma binary_distance_ball:
assumes "(x,x') ∈ m.open_ball (a,a') ε"
shows "x ∈ m1.open_ball a ε"
and "x' ∈ m2.open_ball a' ε"
proof -
have 1:"x ∈ S" "x' ∈ S'" "ε > 0" "a ∈ S" "a' ∈ S'"
using m.open_ballD'[OF assms(1)] by auto
thus "x ∈ metric_set.open_ball S d a ε"
and "x' ∈ metric_set.open_ball S' d' a' ε"
using m.open_ballD[OF assms(1)] binary_distance_geq[OF 1(4,1,5,2)] 1
by(auto simp: m1.open_ball_def m2.open_ball_def)
qed
lemma binary_distance_ball':
assumes "z ∈ m.open_ball a ε"
shows "fst z ∈ m1.open_ball (fst a) ε"
and "snd z ∈ m2.open_ball (snd a) ε"
using binary_distance_ball[of "fst z" "snd z" "fst a" "snd a" ε] assms by auto
lemma binary_distance_ball1':
assumes "a ∈ S" "ε > 0" "a'∈ S'" "ε' > 0"
shows "∃ε''>0. m.open_ball (a,a') ε'' ⊆ m1.open_ball a ε × m2.open_ball a' ε'"
proof(rule exI[where x="min ε ε'"])
show "0 < min ε ε' ∧ m.open_ball (a, a') (min ε ε') ⊆ m1.open_ball a ε × m2.open_ball a' ε'"
proof
show "0 < min ε ε'"
using assms by auto
next
show "m.open_ball (a, a') (min ε ε') ⊆ m1.open_ball a ε × m2.open_ball a' ε'"
proof safe
fix x x'
assume h:"(x,x') ∈ m.open_ball (a, a') (min ε ε')"
then have hx:"x ∈ S" "x' ∈ S'"
using m.open_ballD'(1)[of "(x,x')" "(a, a')" "min ε ε'"] by auto
hence "d a x + d' a' x' < min ε ε'"
using h assms by(auto simp: m.open_ball_def,auto simp: binary_distance_def)
thus "x ∈ m1.open_ball a ε" "x' ∈ m2.open_ball a' ε'"
using m1.dist_geq0[of a x] m2.dist_geq0[of a' x'] assms hx
by(auto simp: m1.open_ball_def m2.open_ball_def)
qed
qed
qed
lemma binary_distance_ball1:
assumes "b ∈ m1.open_ball a ε" "b' ∈ m2.open_ball a' ε'"
shows "∃ε''>0. m.open_ball (b,b') ε'' ⊆ m1.open_ball a ε × m2.open_ball a' ε'"
proof -
obtain εa εa' where he:
"εa > 0" "εa' > 0" "m1.open_ball b εa ⊆ m1.open_ball a ε" "m2.open_ball b' εa' ⊆ m2.open_ball a' ε'"
using m1.mtopology_open_ball_in'[OF assms(1)] m2.mtopology_open_ball_in'[OF assms(2)] by auto
thus ?thesis
using binary_distance_ball1'[OF m1.open_ballD'(1)[OF assms(1)] he(1) m2.open_ballD'(1)[OF assms(2)] he(2)]
by blast
qed
lemma binary_distance_ball2':
assumes "a ∈ S" "ε'' > 0" "a'∈ S'"
shows "∃ε>0. ∃ε'>0. m1.open_ball a ε × m2.open_ball a' ε' ⊆ m.open_ball (a,a') ε''"
proof(safe intro!: exI[where x="ε''/2"])
fix x x'
assume "x ∈ m1.open_ball a (ε'' / 2)" "x' ∈ m2.open_ball a' (ε'' / 2)"
then have "x ∈ S" "x' ∈ S'" "d a x < ε'' / 2" "d' a' x' < ε'' / 2"
using assms by(auto simp: m1.open_ball_def m2.open_ball_def)
thus "(x,x') ∈ m.open_ball (a, a') ε''"
using assms by(auto simp: m.open_ball_def,auto simp: binary_distance_def)
qed (use assms in auto)
lemma binary_distance_ball2:
assumes "(b,b') ∈ m.open_ball (a,a') ε''"
shows "∃ε>0. ∃ε'>0. m1.open_ball b ε × m2.open_ball b' ε' ⊆ m.open_ball (a,a') ε''"
proof -
obtain ε''' where "ε''' > 0" "m.open_ball (b,b') ε''' ⊆ m.open_ball (a,a') ε''"
using m.mtopology_open_ball_in'[OF assms(1)] by blast
thus ?thesis
using binary_distance_ball2'[of b ε''' b'] m.open_ballD'[OF assms(1),simplified]
by blast
qed
lemma binary_distance_mtopology:
"m.mtopology = prod_topology m1.mtopology m2.mtopology"
proof -
have "m.mtopology = topology_generated_by { m1.open_ball a ε × m2.open_ball a' ε' | a a' ε ε'. a ∈ S ∧ a' ∈ S' ∧ ε > 0 ∧ ε' > 0}"
unfolding m.mtopology_def2
proof(rule topology_generated_by_eq)
fix U
assume "U ∈ {m1.open_ball a ε × m2.open_ball a' ε' |a a' ε ε'. a ∈ S ∧ a' ∈ S' ∧ 0 < ε ∧ 0 < ε'}"
then obtain a ε a' ε' where hae:
"U = m1.open_ball a ε × m2.open_ball a' ε'" "a ∈ S" "a' ∈ S'" "0 < ε" "0 < ε'"
by auto
show "openin (topology_generated_by {m.open_ball a ε |a ε. a ∈ S × S' ∧ 0 < ε}) U"
unfolding m.mtopology_def2[symmetric] m.mtopology_openin_iff hae(1)
using binary_distance_ball1[of _ a ε _ a' ε'] m1.open_ball_subset_ofS m2.open_ball_subset_ofS
by fastforce
next
fix U
assume "U ∈ {m.open_ball a ε |a ε. a ∈ S × S' ∧ 0 < ε}"
then obtain a a' ε where hae:
"U = m.open_ball (a,a') ε" "a ∈ S" "a' ∈ S'" "0 < ε"
by auto
show "openin (topology_generated_by {m1.open_ball a ε × m2.open_ball a' ε' |a a' ε ε'. a ∈ S ∧ a' ∈ S' ∧ 0 < ε ∧ 0 < ε'}) U"
unfolding openin_subopen[of _ " m.open_ball (a,a') ε"] hae(1)
proof
fix x
assume h:"x ∈ m.open_ball (a, a') ε"
with binary_distance_ball2[of "fst x" "snd x" a a' ε]
obtain ε' ε'' where he:
"ε' > 0" "ε'' > 0" "m1.open_ball (fst x) ε' × m2.open_ball (snd x) ε'' ⊆ m.open_ball (a, a') ε"
by auto
show "∃T. openin (topology_generated_by {m1.open_ball a ε × m2.open_ball a' ε' |a a' ε ε'. a ∈ S ∧ a' ∈ S' ∧ 0 < ε ∧ 0 < ε'}) T ∧ x ∈ T ∧ T ⊆ m.open_ball (a, a') ε"
unfolding openin_topology_generated_by_iff
using he m1.open_ball_ina[of "fst x",OF _ he(1)] m.open_ballD'(1,2)[OF h] m2.open_ball_ina[of "snd x",OF _ he(2)]
by(fastforce intro!: generate_topology_on.Basis exI[where x="m1.open_ball (fst x) ε' × m2.open_ball (snd x) ε''"] exI[where x="fst x"] exI[where x="snd x"])
qed
qed
also have "... = prod_topology m1.mtopology m2.mtopology"
proof -
have "{m1.open_ball a ε × m2.open_ball a' ε' |a a' ε ε'. a ∈ S ∧ a' ∈ S' ∧ 0 < ε ∧ 0 < ε'} = {U × V |U V. U ∈ {m1.open_ball a ε |a ε. a ∈ S ∧ 0 < ε} ∧ V ∈ {m2.open_ball a ε |a ε. a ∈ S' ∧ 0 < ε}}"
by blast
thus ?thesis
unfolding m1.mtopology_def2 m2.mtopology_def2
by(simp only: prod_topology_generated_by[symmetric])
qed
finally show ?thesis .
qed
lemma binary_distance_converge_to_inS_iff:
"m.converge_to_inS zn (x,y) ⟷ m1.converge_to_inS (λn. fst (zn n)) x ∧ m2.converge_to_inS (λn. snd (zn n)) y"
proof safe
assume "m.converge_to_inS zn (x, y)"
then have h:"zn ∈ UNIV → S × S'" "x ∈ S" "y ∈ S'" "⋀e. e>0 ⟹ ∃N. ∀n≥N. zn n ∈ m.open_ball (x, y) e"
by(auto simp: m.converge_to_inS_def2')
show "m1.converge_to_inS (λn. fst (zn n)) x"
"m2.converge_to_inS (λn. snd (zn n)) y"
unfolding m1.converge_to_inS_def2' m2.converge_to_inS_def2'
proof safe
fix e :: real
assume "e > 0"
then obtain N where "⋀n. n ≥ N ⟹ zn n ∈ m.open_ball (x, y) e"
using h(4) by auto
thus "∃N. ∀n≥N. fst (zn n) ∈ m1.open_ball x e"
"∃N. ∀n≥N. snd (zn n) ∈ m2.open_ball y e"
using binary_distance_ball'[of "zn _" "(x,y)"]
by(auto intro!: exI[where x=N])
qed(insert h(1-3),simp_all add: Pi_iff mem_Times_iff)
next
assume h:"m1.converge_to_inS (λn. fst (zn n)) x" "m2.converge_to_inS (λn. snd (zn n)) y"
show "m.converge_to_inS zn (x, y)"
unfolding m.converge_to_inS_def2'
proof safe
show goal1:"x ∈ S" "y ∈ S'" "zn n ∈ S × S'" for n
using h by(auto simp: m1.converge_to_inS_def m2.converge_to_inS_def Pi_iff mem_Times_iff)
fix e :: real
assume "e > 0"
from binary_distance_ball2'[OF goal1(1) this goal1(2)]
obtain e1 e2 where e12:"e1 > 0" "e2 > 0" "m1.open_ball x e1 × m2.open_ball y e2 ⊆ m.open_ball (x, y) e " by auto
then obtain N1 N2 where N12: "⋀n. n ≥ N1 ⟹ fst (zn n) ∈ m1.open_ball x e1" "⋀n. n ≥ N2 ⟹ snd (zn n) ∈ m2.open_ball y e2"
using h by(auto simp: m1.converge_to_inS_def2' m2.converge_to_inS_def2') metis
with e12 have "⋀n. n ≥ max N1 N2 ⟹ zn n ∈ m1.open_ball x e1 × m2.open_ball y e2"
by (simp add: mem_Times_iff)
with e12(3) show "∃N. ∀n≥N. zn n ∈ m.open_ball (x, y) e"
by(auto intro!: exI[where x="max N1 N2"])
qed
qed
lemma binary_distance_converge_to_inS_iff':
"m.converge_to_inS zn z ⟷ m1.converge_to_inS (λn. fst (zn n)) (fst z) ∧ m2.converge_to_inS (λn. snd (zn n)) (snd z)"
using binary_distance_converge_to_inS_iff[of _ "fst z" "snd z"] by simp
corollary binary_distance_convergent_inS_iff:
"m.convergent_inS zn ⟷ m1.convergent_inS (λn. fst (zn n)) ∧ m2.convergent_inS (λn. snd (zn n))"
by(auto simp: m.convergent_inS_def m1.convergent_inS_def m2.convergent_inS_def binary_distance_converge_to_inS_iff)
lemma binary_distance_Cauchy_inS_iff:
"m.Cauchy_inS zn ⟷ m1.Cauchy_inS (λn. fst (zn n)) ∧ m2.Cauchy_inS (λn. snd (zn n))"
proof safe
assume h:"m.Cauchy_inS zn"
show "m1.Cauchy_inS (λn. fst (zn n))" "m2.Cauchy_inS (λn. snd (zn n))"
unfolding m1.Cauchy_inS_def2' m2.Cauchy_inS_def2'
proof safe
fix e :: real
assume "e > 0"
then obtain x y N where "x ∈ S" "y ∈ S'" "⋀n. n ≥ N ⟹ zn n ∈ m.open_ball (x,y) e"
using h by(auto simp: m.Cauchy_inS_def2') metis
thus "∃x∈S. ∃N. ∀n≥N. fst (zn n) ∈ m1.open_ball x e"
"∃y∈S'. ∃N. ∀n≥N. snd (zn n) ∈ m2.open_ball y e"
using binary_distance_ball'[of "zn _" "(x,y)"]
by(auto intro!: exI[where x=x] exI[where x=y] exI[where x=N]) blast
qed(insert h, simp_all add: m.Cauchy_inS_def Pi_iff mem_Times_iff)
next
assume h: "m1.Cauchy_inS (λn. fst (zn n))" "m2.Cauchy_inS (λn. snd (zn n))"
show "m.Cauchy_inS zn"
unfolding m.Cauchy_inS_def
proof safe
show 1:"zn n ∈ S × S'" for n
using h(1,2) m1.Cauchy_inS_dest1 m2.Cauchy_inS_dest1 mem_Times_iff by blast
fix e :: real
assume "e > 0"
then obtain N1 N2 where N:"⋀n m. n ≥ N1 ⟹ m ≥ N1 ⟹ d (fst (zn n)) (fst (zn m)) < e / 2" "⋀n m. n ≥ N2 ⟹ m ≥ N2 ⟹ d' (snd (zn n)) (snd (zn m)) < e / 2"
by (metis h(1) h(2) less_divide_eq_numeral1(1) m1.Cauchy_inS_def m2.Cauchy_inS_def mult_zero_left)
show "∃N. ∀n≥N. ∀m≥N. binary_distance S d S' d' (zn n) (zn m) < e"
proof(safe intro!: exI[where x="max N1 N2"])
fix n m
assume "max N1 N2 ≤ n" "max N1 N2 ≤ m"
then have le:"N1 ≤ n" "N1 ≤ m" "N2 ≤ n" "N2 ≤ m" by auto
show "binary_distance S d S' d' (zn n) (zn m) < e"
using N(1)[OF le(1,2)] N(2)[OF le(3,4)] ‹e > 0›
by(auto simp: binary_distance_def split_beta')
qed
qed
qed
end
lemma binary_distance_separable:
assumes "separable_metric_set S d" "separable_metric_set S' d'"
shows "separable_metric_set (S × S') (binary_distance S d S' d')"
proof -
interpret m1:separable_metric_set S d by fact
interpret m2:separable_metric_set S' d' by fact
interpret m : metric_set "S × S'" "binary_distance S d S' d'"
by(auto intro!: binary_metric_set m1.metric_set_axioms m2.metric_set_axioms)
show ?thesis
using m.separable_iff_topological_separable separable_prod[OF m1.topological_separable_if_separable m2.topological_separable_if_separable] binary_distance_mtopology[OF m1.metric_set_axioms m2.metric_set_axioms]
by auto
qed
lemma binary_distance_complete:
assumes "complete_metric_set S d" "complete_metric_set S' d'"
shows "complete_metric_set (S × S') (binary_distance S d S' d')"
proof -
interpret m1:complete_metric_set S d by fact
interpret m2:complete_metric_set S' d' by fact
interpret m : metric_set "S × S'" "binary_distance S d S' d'"
by(auto intro!: binary_metric_set m1.metric_set_axioms m2.metric_set_axioms)
show ?thesis
by standard (simp add: binary_distance_Cauchy_inS_iff[OF m1.metric_set_axioms m2.metric_set_axioms] binary_distance_convergent_inS_iff[OF m1.metric_set_axioms m2.metric_set_axioms] m1.convergence m2.convergence)
qed
lemma binary_distance_polish:
assumes "polish_metric_set S d" and "polish_metric_set S' d'"
shows "polish_metric_set (S×S') (binary_distance S d S' d')"
using assms by(simp add: polish_metric_set_def binary_distance_separable binary_distance_complete)
subsection ‹Sum Metric Spaces›
locale sum_metric =
fixes I :: "'i set"
and Si :: "'i ⇒ 'a set"
and di :: "'i ⇒ 'a ⇒ 'a ⇒ real"
assumes disj_fam: "disjoint_family_on Si I"
and d_nonneg: "⋀i x y. 0 ≤ di i x y"
and d_bounded: "⋀i x y. di i x y < 1"
and sd_metric: "⋀i. i ∈ I ⟹ metric_set (Si i) (di i)"
begin
abbreviation "S ≡ ⋃i∈I. Si i"
lemma Si_inj_on:
assumes "i ∈ I" "j ∈ I" "a ∈ Si i" "a ∈ Si j"
shows "i = j"
using disj_fam assms by(auto simp: disjoint_family_on_def)
definition sum_dist :: "['a, 'a] ⇒ real" where
"sum_dist x y ≡ (if x ∈ S ∧ y ∈ S then (if ∃i∈I. x ∈ Si i ∧ y ∈ Si i then di (THE i. i ∈ I ∧ x ∈ Si i ∧ y ∈ Si i) x y else 1) else 0)"
lemma sum_dist_simps:
shows "⋀i. ⟦i ∈ I; x ∈ Si i; y ∈ Si i⟧ ⟹ sum_dist x y = di i x y"
and "⋀i j. ⟦i ∈ I; j ∈ I; i ≠ j; x ∈ Si i; y ∈ Si j⟧ ⟹ sum_dist x y = 1"
and "⋀i. ⟦i ∈ I; y ∈ S; x ∈ Si i; y ∉ Si i⟧ ⟹ sum_dist x y = 1"
and "⋀i. ⟦i ∈ I; x ∈ S; y ∈ Si i; x ∉ Si i⟧ ⟹ sum_dist x y = 1"
and "x ∉ S ⟹ sum_dist x y = 0"
proof -
{ fix i
assume h:"i ∈ I" "x ∈ Si i" "y ∈ Si i"
then have "sum_dist x y = di (THE i. i ∈ I ∧ x ∈ Si i ∧ y ∈ Si i) x y"
by(auto simp: sum_dist_def)
also have "... = di i x y"
proof -
have "(THE i. i ∈ I ∧ x ∈ Si i ∧ y ∈ Si i) = i"
using disj_fam h by(auto intro!: the1_equality simp: disjoint_family_on_def)
thus ?thesis by simp
qed
finally show "sum_dist x y = di i x y" . }
show "⋀i j. ⟦i ∈ I; j ∈ I; i ≠ j; x ∈ Si i; y ∈ Si j⟧ ⟹ sum_dist x y = 1"
"⋀i. ⟦i ∈ I; y ∈ S; x ∈ Si i; y ∉ Si i⟧ ⟹ sum_dist x y = 1" "⋀i. ⟦i ∈ I; x ∈ S; y ∈ Si i; x ∉ Si i⟧ ⟹ sum_dist x y = 1"
"x ∉ S ⟹ sum_dist x y = 0"
using disj_fam by(auto simp: sum_dist_def disjoint_family_on_def dest:Si_inj_on)
qed
lemma sum_dist_if_less1:
assumes "i ∈ I" "x ∈ Si i" "y ∈ S" "sum_dist x y < 1"
shows "y ∈ Si i"
using assms sum_dist_simps(3) by fastforce
lemma inS_cases:
assumes "x ∈ S" "y ∈ S"
and "⋀i. ⟦i ∈ I; x ∈ Si i; y ∈ Si i⟧ ⟹ P x y"
and "⋀i j. ⟦i ∈ I; j ∈ I; i ≠ j; x ∈ Si i; y ∈ Si j; x ≠ y⟧ ⟹ P x y"
shows "P x y" using assms by auto
sublocale metric_set S sum_dist
proof
fix x y
assume "x ∈ S" "y ∈ S"
then show "x = y ⟷ sum_dist x y = 0"
by(rule inS_cases, insert sd_metric) (auto simp: sum_dist_simps metric_set_def)
next
{ fix i x y
assume h: "i ∈ I" "x ∈ Si i" "y ∈ Si i"
then have "sum_dist x y = di i x y"
"sum_dist y x = di i x y"
using sd_metric by(auto simp: sum_dist_simps metric_set_def) }
thus "⋀x y. sum_dist x y = sum_dist y x"
by (metis (no_types, lifting) sum_dist_def)
next
show 1:"⋀x y. 0 ≤ sum_dist x y"
using d_nonneg by(simp add: sum_dist_def)
fix x y z
assume h: "x ∈ S" "y ∈ S" "z ∈ S"
show "sum_dist x z ≤ sum_dist x y + sum_dist y z" (is "?lhs ≤ ?rhs")
proof(rule inS_cases[OF h(1,3)])
fix i
assume h':"i ∈ I" "x ∈ Si i" "z ∈ Si i"
consider "y ∈ Si i" | "y ∉ Si i" by auto
thus "?lhs ≤ ?rhs"
proof cases
case 1
with h' sd_metric [OF h'(1)]show ?thesis
by(simp add: sum_dist_simps metric_set_def)
next
case 2
with h' h(2) d_bounded[of i x z] 1[of y z]
show ?thesis
by(auto simp: sum_dist_simps)
qed
next
fix i j
assume h': "i ∈ I" "j ∈ I" "i ≠ j" "x ∈ Si i" "z ∈ Si j"
consider "y ∉ Si i" | "y ∉ Si j"
using h' h(2) disj_fam by(auto simp: disjoint_family_on_def)
thus "?lhs ≤ ?rhs"
by (cases, insert 1[of x y] 1[of y z] h' h(2)) (auto simp: sum_dist_simps)
qed
qed(simp add: sum_dist_simps)
lemma sum_dist_le1: "sum_dist x y ≤ 1"
using d_bounded[of _ x y] by(auto simp: sum_dist_def less_eq_real_def)
lemma sum_dist_ball_eq_ball:
assumes "i ∈ I" "e ≤ 1" "x ∈ Si i"
shows "metric_set.open_ball (Si i) (di i) x e = open_ball x e"
proof -
interpret m: metric_set "Si i" "di i"
by(simp add: assms sd_metric)
show ?thesis
using assms sum_dist_simps(1)[OF assms(1) assms(3)] sum_dist_if_less1[OF assms(1,3)]
by(auto simp: m.open_ball_def open_ball_def) fastforce+
qed
lemma ball_le_sum_dist_ball:
assumes "i ∈ I"
shows "metric_set.open_ball (Si i) (di i) x e ⊆ open_ball x e"
proof -
interpret m: metric_set "Si i" "di i"
by(simp add: assms sd_metric)
show ?thesis
proof safe
fix y
assume y: "y ∈ m.open_ball x e"
show "y ∈ open_ball x e"
using m.open_ballD[OF y] m.open_ballD'[OF y] assms
by(auto simp: open_ball_def sum_dist_simps)
qed
qed
lemma openin_sum_mtopology_iff:
"openin mtopology U ⟷ U ⊆ S ∧ (∀i∈I. openin (metric_set.mtopology (Si i) (di i)) (U ∩ Si i))"
proof safe
fix i
assume h:"openin mtopology U" "i ∈ I"
then interpret m: metric_set "Si i" "di i"
using sd_metric by simp
show "openin m.mtopology (U ∩ Si i)"
unfolding m.mtopology_openin_iff
proof safe
fix x
assume x:"x ∈ U" "x ∈ Si i"
with h obtain e where e: "e > 0" "open_ball x e ⊆ U"
by(auto simp: mtopology_openin_iff)
show "∃ε>0. m.open_ball x ε ⊆ U ∩ Si i"
proof(safe intro!: exI[where x=e])
fix y
assume "y ∈ m.open_ball x e"
from m.open_ballD[OF this] x(2) m.open_ballD'(1)[OF this] h(2)
have "y ∈ open_ball x e"
by(auto simp: open_ball_def sum_dist_simps)
with e show "y ∈ U" by auto
qed(use e m.open_ball_subset_ofS in auto)
qed
next
show "⋀x. openin mtopology U ⟹ x ∈ U ⟹ x ∈ S"
by(auto simp: mtopology_openin_iff)
next
assume h: "U ⊆ S" "∀i∈I. openin (metric_set.mtopology (Si i) (di i)) (U ∩ Si i)"
show "openin mtopology U"
unfolding mtopology_openin_iff
proof safe
fix x
assume x: "x ∈ U"
then obtain i where i: "i ∈ I" "x ∈ Si i"
using h(1) by auto
then interpret m: metric_set "Si i" "di i"
using sd_metric by simp
obtain e where e: "e > 0" "m.open_ball x e ⊆ U ∩ Si i"
using i h(2) by (meson IntI m.mtopology_openin_iff x)
show "∃ε>0. open_ball x ε ⊆ U"
proof(safe intro!: exI[where x="min e 1"])
fix y
assume y:"y ∈ open_ball x (min e 1)"
then show "y ∈ U"
using sum_dist_ball_eq_ball[OF i(1) _ i(2),of "min e 1"] e m.open_ball_le[of "min e 1" e x]
by auto
qed(simp add: e)
qed(use h(1) in auto)
qed
corollary openin_sum_mtopology_Si:
assumes "i ∈ I"
shows "openin mtopology (Si i)"
unfolding openin_sum_mtopology_iff
proof safe
fix j
assume j:"j ∈ I"
then interpret m: metric_set "Si j" "di j"
by(simp add: sd_metric)
show "openin m.mtopology (Si i ∩ Si j)"
by (cases "i = j", insert assms disj_fam j) (auto simp: disjoint_family_on_def)
qed(use assms in auto)
lemma converge_to_inSi_converge_to_inS:
assumes "i ∈ I" "metric_set.converge_to_inS (Si i) (di i) xn x"
shows "converge_to_inS xn x"
proof -
interpret m: metric_set "Si i" "di i"
by(simp add: assms sd_metric)
{
fix e :: real
assume "e > 0"
then obtain N where "⋀n. n ≥ N ⟹ xn n ∈ m.open_ball x e"
using assms(2) by(auto simp: m.converge_to_inS_def2') metis
hence "∃N. ∀n≥N. xn n ∈ open_ball x e"
using ball_le_sum_dist_ball[OF assms(1),of x e]
by(auto intro!: exI[where x=N]) }
thus ?thesis
using assms by(auto simp: m.converge_to_inS_def2' converge_to_inS_def2')
qed
corollary convergent_inSi_convergent_inS:
assumes "i ∈ I" "metric_set.convergent_inS (Si i) (di i) xn"
shows "convergent_inS xn"
using converge_to_inSi_converge_to_inS[OF assms(1)] assms(1) assms(2) convergent_inS_def metric_set.the_limit_if_converge sd_metric
by blast
lemma converge_to_inS_converge_to_inSi_off_set:
assumes "converge_to_inS xn x"
shows "∃n. ∃j∈I. metric_set.converge_to_inS (Si j) (di j) (λi. xn (i + n)) x"
proof -
obtain i where i: "i ∈ I" "x ∈ Si i"
using assms by(auto simp: converge_to_inS_def)
then interpret m: metric_set "Si i" "di i"
by(simp add: sd_metric)
obtain N where N: "⋀n. n ≥ N ⟹ sum_dist (xn n) x < 1"
using assms by(fastforce simp: converge_to_inS_def2)
hence N': "n ≥ N ⟹ xn n ∈ Si i" for n
using assms by(auto intro!: sum_dist_if_less1[OF i,of "xn n"] simp: dist_sym[of _ x] converge_to_inS_def)
show ?thesis
proof(safe intro!: exI[where x=N] bexI[OF _ i(1)])
show "m.converge_to_inS (λi. xn (i + N)) x"
unfolding m.converge_to_inS_def2
proof(safe intro!: N' i(2))
fix e :: real
assume "0 < e"
then obtain M where M: "⋀n. n ≥ M ⟹ sum_dist (xn n) x < e"
using assms by(fastforce simp: converge_to_inS_def2)
hence "n ≥ max N M ⟹ di i (xn n) x < e" for n
using sum_dist_simps(1)[OF i(1) N'[of n] i(2),symmetric] by auto
thus "∃M. ∀n≥M. di i (xn (n + N)) x < e"
by(auto intro!: exI[where x=M])
qed simp
qed
qed
corollary convergent_inS_convergent_inSi_off_set:
assumes "convergent_inS xn"
shows "∃n. ∃j∈I. metric_set.convergent_inS (Si j) (di j) (λi. xn (i + n))"
using converge_to_inS_converge_to_inSi_off_set
by (meson assms metric_set.convergent_inS_def metric_set_axioms sd_metric)
lemma Cauchy_inSi_Cauchy_inS:
assumes "i ∈ I" "metric_set.Cauchy_inS (Si i) (di i)xn"
shows "Cauchy_inS xn"
proof -
interpret m: metric_set "Si i" "di i"
by(simp add: assms sd_metric)
have [simp]:"sum_dist (xn n) (xn m) = di i (xn n) (xn m)" for n m
using assms sum_dist_simps(1)[OF assms(1)]
by(auto simp: m.Cauchy_inS_def Cauchy_inS_def)
show ?thesis
using assms by(auto simp: m.Cauchy_inS_def Cauchy_inS_def)
qed
lemma Cauchy_inS_Cauchy_inSi:
assumes "Cauchy_inS xn"
shows "∃n. ∃j∈I. metric_set.Cauchy_inS (Si j) (di j) (λi. xn (i + n))"
proof -
obtain x i N where xiN: "i ∈ I" "x ∈ Si i" "⋀n. n ≥ N ⟹ xn n ∈ open_ball x 1"
using assms by(auto simp: Cauchy_inS_def2') (metis UNION_empty_conv(2) d_bounded d_nonneg dist_0 empty_subsetI less_eq_real_def open_ball_le_0 subsetI subset_antisym sum_dist_le1)
then interpret m: metric_set "Si i" "di i"
by(simp add: sd_metric)
have xn: "n ≥ N ⟹ xn n ∈ Si i" for n
using xiN(3)[of n] by(auto simp: sum_dist_ball_eq_ball[OF xiN(1) order_refl xiN(2),symmetric] dest: m.open_ballD')
show ?thesis
proof(safe intro!: exI[where x=N] bexI[OF _ xiN(1)])
show "m.Cauchy_inS (λi. xn (i + N))"
unfolding m.Cauchy_inS_def
proof safe
fix e :: real
assume "0 < e"
then obtain M where M: "⋀n m. n ≥ M ⟹ m ≥ M ⟹ sum_dist (xn n) (xn m) < e"
using assms by(auto simp: Cauchy_inS_def) metis
have [simp]: "n ≥ N ⟹ m ≥ N ⟹ di i (xn n) (xn m) = sum_dist (xn n) (xn m)" for n m
using xn sum_dist_simps(1)[OF xiN(1) xn[of n] xn[of m]] by simp
show "∃N'. ∀n≥N'. ∀m≥N'. di i (xn (n + N)) (xn (m + N)) < e"
using M by(auto intro!: exI[where x="max N M"])
qed(use xn in auto)
qed
qed
end
lemma sum_metricI:
fixes Si
assumes "disjoint_family_on Si I"
and "⋀i x y. i ∉ I ⟹ 0 ≤ di i x y"
and "⋀i x y. di i x y < 1"
and "⋀i. i ∈ I ⟹ metric_set (Si i) (di i)"
shows "sum_metric I Si di"
using assms by(auto simp: sum_metric_def) (meson metric_set.dist_geq0)
locale sum_separable_metric = sum_metric +
assumes I: "countable I"
and sd_separable_metric: "⋀i. i ∈ I ⟹ separable_metric_set (Si i) (di i)"
begin
sublocale separable_metric_set S sum_dist
proof
obtain Ui where Ui: "⋀i. i ∈ I ⟹ countable (Ui i)" "⋀i. i ∈ I ⟹ metric_set.dense_set (Si i) (di i) (Ui i)"
using sd_separable_metric by(auto simp: separable_metric_set_def separable_metric_set_axioms_def) metis
define U where "U ≡ ⋃i∈I. Ui i"
show "∃U. countable U ∧ dense_set U"
proof(safe intro!: exI[where x=U])
show "countable U"
using Ui(1) I by(auto simp: U_def)
next
show "dense_set U"
unfolding dense_set_def U_def
proof safe
fix i x
assume "i ∈ I" "x ∈ Ui i"
then show "x ∈ S"
using sd_separable_metric Ui by(auto intro!: bexI[where x=i] simp: separable_metric_set_def metric_set.dense_set_def)
next
fix i x e
assume h:"i ∈ I" "x ∈ Si i" "(0 :: real) < e" "open_ball x e ∩ ⋃ (Ui ` I) = {}"
then interpret sd: separable_metric_set "Si i" "di i"
by(simp add: sd_separable_metric)
have "sd.open_ball x e ∩ Ui i ≠ {}"
using Ui(2)[OF h(1)] h(1-3) by(auto simp: U_def sd.dense_set_def)
hence "sd.open_ball x e ∩ ⋃ (Ui ` I) ≠ {}"
using h(1) by blast
thus False
using ball_le_sum_dist_ball[OF ‹i ∈ I›,of x e] h(4) by blast
qed
qed
qed
end
locale sum_complete_metric = sum_metric +
assumes sd_complete_metric: "⋀i. i ∈ I ⟹ complete_metric_set (Si i) (di i)"
begin
sublocale complete_metric_set S sum_dist
proof
fix xn
assume 1:"Cauchy_inS xn"
from Cauchy_inS_Cauchy_inSi[OF this] obtain n j where h: "j ∈ I" "metric_set.Cauchy_inS (Si j) (di j) (λi. xn (i + n))"
by auto
then have "metric_set.convergent_inS (Si j) (di j) (λi. xn (i + n))"
by (simp add: complete_metric_set.convergence sd_complete_metric)
from convergent_inS_offset[OF convergent_inSi_convergent_inS[OF h(1) this]] 1
show "convergent_inS xn"
by(simp add: Cauchy_inS_def)
qed
end
locale sum_polish_metric = sum_complete_metric + sum_separable_metric
begin
sublocale polish_metric_set S sum_dist
by (simp add: complete_metric_set_axioms polish_metric_set_def separable_metric_set_axioms)
end
lemma sum_polish_metricI:
fixes Si
assumes "countable I"
and "disjoint_family_on Si I"
and "⋀i x y. i ∉ I ⟹ 0 ≤ di i x y"
and "⋀i x y. di i x y < 1"
and "⋀i. i ∈ I ⟹ polish_metric_set (Si i) (di i)"
shows "sum_polish_metric I Si di"
using assms by(auto simp: sum_polish_metric_def sum_complete_metric_def sum_separable_metric_def sum_complete_metric_axioms_def sum_separable_metric_axioms_def polish_metric_set_def complete_metric_set_def sum_metricI)
end