Theory Abstract_Metric_Spaces
section ‹Abstract Metric Spaces›
theory Abstract_Metric_Spaces
imports Elementary_Metric_Spaces Abstract_Limits Abstract_Topological_Spaces
begin
locale Metric_space =
fixes M :: "'a set" and d :: "'a ⇒ 'a ⇒ real"
assumes nonneg [simp]: "⋀x y. 0 ≤ d x y"
assumes commute: "⋀x y. d x y = d y x"
assumes zero [simp]: "⋀x y. ⟦x ∈ M; y ∈ M⟧ ⟹ d x y = 0 ⟷ x=y"
assumes triangle: "⋀x y z. ⟦x ∈ M; y ∈ M; z ∈ M⟧ ⟹ d x z ≤ d x y + d y z"
text ‹Link with the type class version›
interpretation Met_TC: Metric_space UNIV dist
by (simp add: dist_commute dist_triangle Metric_space.intro)
context Metric_space
begin
lemma subspace: "M' ⊆ M ⟹ Metric_space M' d"
by (simp add: commute in_mono Metric_space.intro triangle)
lemma abs_mdist [simp] : "¦d x y¦ = d x y"
by simp
lemma mdist_pos_less: "⟦x ≠ y; x ∈ M; y ∈ M⟧ ⟹ 0 < d x y"
by (metis less_eq_real_def nonneg zero)
lemma mdist_zero [simp]: "x ∈ M ⟹ d x x = 0"
by simp
lemma mdist_pos_eq [simp]: "⟦x ∈ M; y ∈ M⟧ ⟹ 0 < d x y ⟷ x ≠ y"
using mdist_pos_less zero by fastforce
lemma triangle': "⟦x ∈ M; y ∈ M; z ∈ M⟧ ⟹ d x z ≤ d x y + d z y"
by (simp add: commute triangle)
lemma triangle'': "⟦x ∈ M; y ∈ M; z ∈ M⟧ ⟹ d x z ≤ d y x + d y z"
by (simp add: commute triangle)
lemma mdist_reverse_triangle: "⟦x ∈ M; y ∈ M; z ∈ M⟧ ⟹ ¦d x y - d y z¦ ≤ d x z"
by (smt (verit) commute triangle)
text‹ Open and closed balls ›
definition mball where "mball x r ≡ {y. x ∈ M ∧ y ∈ M ∧ d x y < r}"
definition mcball where "mcball x r ≡ {y. x ∈ M ∧ y ∈ M ∧ d x y ≤ r}"
lemma in_mball [simp]: "y ∈ mball x r ⟷ x ∈ M ∧ y ∈ M ∧ d x y < r"
by (simp add: mball_def)
lemma centre_in_mball_iff [iff]: "x ∈ mball x r ⟷ x ∈ M ∧ 0 < r"
using in_mball mdist_zero by force
lemma mball_subset_mspace: "mball x r ⊆ M"
by auto
lemma mball_eq_empty: "mball x r = {} ⟷ (x ∉ M) ∨ r ≤ 0"
by (smt (verit, best) Collect_empty_eq centre_in_mball_iff mball_def nonneg)
lemma mball_subset: "⟦d x y + a ≤ b; y ∈ M⟧ ⟹ mball x a ⊆ mball y b"
by (smt (verit) commute in_mball subsetI triangle)
lemma disjoint_mball: "r + r' ≤ d x x' ⟹ disjnt (mball x r) (mball x' r')"
by (smt (verit) commute disjnt_iff in_mball triangle)
lemma mball_subset_concentric: "r ≤ s ⟹ mball x r ⊆ mball x s"
by auto
lemma in_mcball [simp]: "y ∈ mcball x r ⟷ x ∈ M ∧ y ∈ M ∧ d x y ≤ r"
by (simp add: mcball_def)
lemma centre_in_mcball_iff [iff]: "x ∈ mcball x r ⟷ x ∈ M ∧ 0 ≤ r"
using mdist_zero by force
lemma mcball_eq_empty: "mcball x r = {} ⟷ (x ∉ M) ∨ r < 0"
by (smt (verit, best) Collect_empty_eq centre_in_mcball_iff empty_iff mcball_def nonneg)
lemma mcball_subset_mspace: "mcball x r ⊆ M"
by auto
lemma mball_subset_mcball: "mball x r ⊆ mcball x r"
by auto
lemma mcball_subset: "⟦d x y + a ≤ b; y ∈ M⟧ ⟹ mcball x a ⊆ mcball y b"
by (smt (verit) in_mcball mdist_reverse_triangle subsetI)
lemma mcball_subset_concentric: "r ≤ s ⟹ mcball x r ⊆ mcball x s"
by force
lemma mcball_subset_mball: "⟦d x y + a < b; y ∈ M⟧ ⟹ mcball x a ⊆ mball y b"
by (smt (verit) commute in_mball in_mcball subsetI triangle)
lemma mcball_subset_mball_concentric: "a < b ⟹ mcball x a ⊆ mball x b"
by force
end
subsection ‹Metric topology ›
context Metric_space
begin
definition mopen where
"mopen U ≡ U ⊆ M ∧ (∀x. x ∈ U ⟶ (∃r>0. mball x r ⊆ U))"
definition mtopology :: "'a topology" where
"mtopology ≡ topology mopen"
lemma is_topology_metric_topology [iff]: "istopology mopen"
proof -
have "⋀S T. ⟦mopen S; mopen T⟧ ⟹ mopen (S ∩ T)"
by (smt (verit, del_insts) Int_iff in_mball mopen_def subset_eq)
moreover have "⋀𝒦. (∀K∈𝒦. mopen K) ⟶ mopen (⋃𝒦)"
using mopen_def by fastforce
ultimately show ?thesis
by (simp add: istopology_def)
qed
lemma openin_mtopology: "openin mtopology U ⟷ U ⊆ M ∧ (∀x. x ∈ U ⟶ (∃r>0. mball x r ⊆ U))"
by (simp add: mopen_def mtopology_def)
lemma topspace_mtopology [simp]: "topspace mtopology = M"
by (meson order.refl mball_subset_mspace openin_mtopology openin_subset openin_topspace subset_antisym zero_less_one)
lemma subtopology_mspace [simp]: "subtopology mtopology M = mtopology"
by (metis subtopology_topspace topspace_mtopology)
lemma open_in_mspace [iff]: "openin mtopology M"
by (metis openin_topspace topspace_mtopology)
lemma closedin_mspace [iff]: "closedin mtopology M"
by (metis closedin_topspace topspace_mtopology)
lemma openin_mball [iff]: "openin mtopology (mball x r)"
proof -
have "⋀y. ⟦x ∈ M; d x y < r⟧ ⟹ ∃s>0. mball y s ⊆ mball x r"
by (metis add_diff_cancel_left' add_diff_eq commute less_add_same_cancel1 mball_subset order_refl)
then show ?thesis
by (auto simp: openin_mtopology)
qed
lemma mtopology_base:
"mtopology = topology(arbitrary union_of (λU. ∃x ∈ M. ∃r>0. U = mball x r))"
proof -
have "⋀S. ∃x r. x ∈ M ∧ 0 < r ∧ S = mball x r ⟹ openin mtopology S"
using openin_mball by blast
moreover have "⋀U x. ⟦openin mtopology U; x ∈ U⟧ ⟹ ∃B. (∃x r. x ∈ M ∧ 0 < r ∧ B = mball x r) ∧ x ∈ B ∧ B ⊆ U"
by (metis centre_in_mball_iff in_mono openin_mtopology)
ultimately show ?thesis
by (smt (verit) topology_base_unique)
qed
lemma closedin_metric:
"closedin mtopology C ⟷ C ⊆ M ∧ (∀x. x ∈ M - C ⟶ (∃r>0. disjnt C (mball x r)))" (is "?lhs = ?rhs")
proof
show "?lhs ⟹ ?rhs"
unfolding closedin_def openin_mtopology
by (metis Diff_disjoint disjnt_def disjnt_subset2 topspace_mtopology)
show "?rhs ⟹ ?lhs"
unfolding closedin_def openin_mtopology disjnt_def
by (metis Diff_subset Diff_triv Int_Diff Int_commute inf.absorb_iff2 mball_subset_mspace topspace_mtopology)
qed
lemma closedin_mcball [iff]: "closedin mtopology (mcball x r)"
proof -
have "∃ra>0. disjnt (mcball x r) (mball y ra)" if "x ∉ M" for y
by (metis disjnt_empty1 gt_ex mcball_eq_empty that)
moreover have "disjnt (mcball x r) (mball y (d x y - r))" if "y ∈ M" "d x y > r" for y
using that disjnt_iff in_mball in_mcball mdist_reverse_triangle by force
ultimately show ?thesis
using closedin_metric mcball_subset_mspace by fastforce
qed
lemma mball_iff_mcball: "(∃r>0. mball x r ⊆ U) = (∃r>0. mcball x r ⊆ U)"
by (meson dense mball_subset_mcball mcball_subset_mball_concentric order_trans)
lemma openin_mtopology_mcball:
"openin mtopology U ⟷ U ⊆ M ∧ (∀x. x ∈ U ⟶ (∃r. 0 < r ∧ mcball x r ⊆ U))"
by (simp add: mball_iff_mcball openin_mtopology)
lemma metric_derived_set_of:
"mtopology derived_set_of S = {x ∈ M. ∀r>0. ∃y∈S. y≠x ∧ y ∈ mball x r}" (is "?lhs=?rhs")
proof
show "?lhs ⊆ ?rhs"
unfolding openin_mtopology derived_set_of_def
by clarsimp (metis in_mball openin_mball openin_mtopology zero)
show "?rhs ⊆ ?lhs"
unfolding openin_mtopology derived_set_of_def
by clarify (metis subsetD topspace_mtopology)
qed
lemma metric_closure_of:
"mtopology closure_of S = {x ∈ M. ∀r>0. ∃y ∈ S. y ∈ mball x r}"
proof -
have "⋀x r. ⟦0 < r; x ∈ mtopology closure_of S⟧ ⟹ ∃y∈S. y ∈ mball x r"
by (metis centre_in_mball_iff in_closure_of openin_mball topspace_mtopology)
moreover have "⋀x T. ⟦x ∈ M; ∀r>0. ∃y∈S. y ∈ mball x r⟧ ⟹ x ∈ mtopology closure_of S"
by (smt (verit) in_closure_of in_mball openin_mtopology subsetD topspace_mtopology)
ultimately show ?thesis
by (auto simp: in_closure_of)
qed
lemma metric_closure_of_alt:
"mtopology closure_of S = {x ∈ M. ∀r>0. ∃y ∈ S. y ∈ mcball x r}"
proof -
have "⋀x r. ⟦∀r>0. x ∈ M ∧ (∃y∈S. y ∈ mcball x r); 0 < r⟧ ⟹ ∃y∈S. y ∈ M ∧ d x y < r"
by (meson dense in_mcball le_less_trans)
then show ?thesis
by (fastforce simp: metric_closure_of in_closure_of)
qed
lemma metric_interior_of:
"mtopology interior_of S = {x ∈ M. ∃ε>0. mball x ε ⊆ S}" (is "?lhs=?rhs")
proof
show "?lhs ⊆ ?rhs"
using interior_of_maximal_eq openin_mtopology by fastforce
show "?rhs ⊆ ?lhs"
using interior_of_def openin_mball by fastforce
qed
lemma metric_interior_of_alt:
"mtopology interior_of S = {x ∈ M. ∃ε>0. mcball x ε ⊆ S}"
by (fastforce simp: mball_iff_mcball metric_interior_of)
lemma in_interior_of_mball:
"x ∈ mtopology interior_of S ⟷ x ∈ M ∧ (∃ε>0. mball x ε ⊆ S)"
using metric_interior_of by force
lemma in_interior_of_mcball:
"x ∈ mtopology interior_of S ⟷ x ∈ M ∧ (∃ε>0. mcball x ε ⊆ S)"
using metric_interior_of_alt by force
lemma Hausdorff_space_mtopology: "Hausdorff_space mtopology"
unfolding Hausdorff_space_def
proof clarify
fix x y
assume x: "x ∈ topspace mtopology" and y: "y ∈ topspace mtopology" and "x ≠ y"
then have gt0: "d x y / 2 > 0"
by auto
have "disjnt (mball x (d x y / 2)) (mball y (d x y / 2))"
by (simp add: disjoint_mball)
then show "∃U V. openin mtopology U ∧ openin mtopology V ∧ x ∈ U ∧ y ∈ V ∧ disjnt U V"
by (metis centre_in_mball_iff gt0 openin_mball topspace_mtopology x y)
qed
subsection‹Bounded sets›
definition mbounded where "mbounded S ⟷ (∃x B. S ⊆ mcball x B)"
lemma mbounded_pos: "mbounded S ⟷ (∃x B. 0 < B ∧ S ⊆ mcball x B)"
proof -
have "∃x' r'. 0 < r' ∧ S ⊆ mcball x' r'" if "S ⊆ mcball x r" for x r
by (metis gt_ex less_eq_real_def linorder_not_le mcball_subset_concentric order_trans that)
then show ?thesis
by (auto simp: mbounded_def)
qed
lemma mbounded_alt:
"mbounded S ⟷ S ⊆ M ∧ (∃B. ∀x ∈ S. ∀y ∈ S. d x y ≤ B)"
proof -
have "⋀x B. S ⊆ mcball x B ⟹ ∀x∈S. ∀y∈S. d x y ≤ 2 * B"
by (smt (verit, best) commute in_mcball subsetD triangle)
then show ?thesis
apply (auto simp: mbounded_def subset_iff)
apply blast+
done
qed
lemma mbounded_alt_pos:
"mbounded S ⟷ S ⊆ M ∧ (∃B>0. ∀x ∈ S. ∀y ∈ S. d x y ≤ B)"
by (smt (verit, del_insts) gt_ex mbounded_alt)
lemma mbounded_subset: "⟦mbounded T; S ⊆ T⟧ ⟹ mbounded S"
by (meson mbounded_def order_trans)
lemma mbounded_subset_mspace: "mbounded S ⟹ S ⊆ M"
by (simp add: mbounded_alt)
lemma mbounded:
"mbounded S ⟷ S = {} ∨ (∀x ∈ S. x ∈ M) ∧ (∃y B. y ∈ M ∧ (∀x ∈ S. d y x ≤ B))"
by (meson all_not_in_conv in_mcball mbounded_def subset_iff)
lemma mbounded_empty [iff]: "mbounded {}"
by (simp add: mbounded)
lemma mbounded_mcball: "mbounded (mcball x r)"
using mbounded_def by auto
lemma mbounded_mball [iff]: "mbounded (mball x r)"
by (meson mball_subset_mcball mbounded_def)
lemma mbounded_insert: "mbounded (insert a S) ⟷ a ∈ M ∧ mbounded S"
proof -
have "⋀y B. ⟦y ∈ M; ∀x∈S. d y x ≤ B⟧
⟹ ∃y. y ∈ M ∧ (∃B ≥ d y a. ∀x∈S. d y x ≤ B)"
by (metis order.trans nle_le)
then show ?thesis
by (auto simp: mbounded)
qed
lemma mbounded_Int: "mbounded S ⟹ mbounded (S ∩ T)"
by (meson inf_le1 mbounded_subset)
lemma mbounded_Un: "mbounded (S ∪ T) ⟷ mbounded S ∧ mbounded T" (is "?lhs=?rhs")
proof
assume R: ?rhs
show ?lhs
proof (cases "S={} ∨ T={}")
case True then show ?thesis
using R by auto
next
case False
obtain x y B C where "S ⊆ mcball x B" "T ⊆ mcball y C" "B > 0" "C > 0" "x ∈ M" "y ∈ M"
using R mbounded_pos
by (metis False mcball_eq_empty subset_empty)
then have "S ∪ T ⊆ mcball x (B + C + d x y)"
by (smt (verit) commute dual_order.trans le_supI mcball_subset mdist_pos_eq)
then show ?thesis
using mbounded_def by blast
qed
next
show "?lhs ⟹ ?rhs"
using mbounded_def by auto
qed
lemma mbounded_Union:
"⟦finite ℱ; ⋀X. X ∈ ℱ ⟹ mbounded X⟧ ⟹ mbounded (⋃ℱ)"
by (induction ℱ rule: finite_induct) (auto simp: mbounded_Un)
lemma mbounded_closure_of:
"mbounded S ⟹ mbounded (mtopology closure_of S)"
by (meson closedin_mcball closure_of_minimal mbounded_def)
lemma mbounded_closure_of_eq:
"S ⊆ M ⟹ (mbounded (mtopology closure_of S) ⟷ mbounded S)"
by (metis closure_of_subset mbounded_closure_of mbounded_subset topspace_mtopology)
lemma maxdist_thm:
assumes "mbounded S"
and "x ∈ S"
and "y ∈ S"
shows "d x y = (SUP z∈S. ¦d x z - d z y¦)"
proof -
have "¦d x z - d z y¦ ≤ d x y" if "z ∈ S" for z
by (metis all_not_in_conv assms mbounded mdist_reverse_triangle that)
moreover have "d x y ≤ r"
if "⋀z. z ∈ S ⟹ ¦d x z - d z y¦ ≤ r" for r :: real
using that assms mbounded_subset_mspace mdist_zero by fastforce
ultimately show ?thesis
by (intro cSup_eq [symmetric]) auto
qed
lemma metric_eq_thm: "⟦S ⊆ M; x ∈ S; y ∈ S⟧ ⟹ (x = y) = (∀z∈S. d x z = d y z)"
by (metis commute subset_iff zero)
lemma compactin_imp_mbounded:
assumes "compactin mtopology S"
shows "mbounded S"
proof -
have "S ⊆ M"
and com: "⋀𝒰. ⟦∀U∈𝒰. openin mtopology U; S ⊆ ⋃𝒰⟧ ⟹ ∃ℱ. finite ℱ ∧ ℱ ⊆ 𝒰 ∧ S ⊆ ⋃ℱ"
using assms by (auto simp: compactin_def mbounded_def)
show ?thesis
proof (cases "S = {}")
case False
with ‹S ⊆ M› obtain a where "a ∈ S" "a ∈ M"
by blast
with ‹S ⊆ M› gt_ex have "S ⊆ ⋃(range (mball a))"
by force
then obtain ℱ where "finite ℱ" "ℱ ⊆ range (mball a)" "S ⊆ ⋃ℱ"
by (metis (no_types, opaque_lifting) com imageE openin_mball)
then show ?thesis
using mbounded_Union mbounded_subset by fastforce
qed auto
qed
end
lemma mcball_eq_cball [simp]: "Met_TC.mcball = cball"
by force
lemma mball_eq_ball [simp]: "Met_TC.mball = ball"
by force
lemma mopen_eq_open [simp]: "Met_TC.mopen = open"
by (force simp: open_contains_ball Met_TC.mopen_def)
lemma limitin_iff_tendsto [iff]: "limitin Met_TC.mtopology σ x F = tendsto σ x F"
by (simp add: Met_TC.mtopology_def)
lemma mtopology_is_euclidean [simp]: "Met_TC.mtopology = euclidean"
by (simp add: Met_TC.mtopology_def)
lemma mbounded_iff_bounded [iff]: "Met_TC.mbounded A ⟷ bounded A"
by (metis Met_TC.mbounded UNIV_I all_not_in_conv bounded_def)
subsection‹Subspace of a metric space›
locale Submetric = Metric_space +
fixes A
assumes subset: "A ⊆ M"
sublocale Submetric ⊆ sub: Metric_space A d
by (simp add: subset subspace)
context Submetric
begin
lemma mball_submetric_eq: "sub.mball a r = (if a ∈ A then A ∩ mball a r else {})"
and mcball_submetric_eq: "sub.mcball a r = (if a ∈ A then A ∩ mcball a r else {})"
using subset by force+
lemma mtopology_submetric: "sub.mtopology = subtopology mtopology A"
unfolding topology_eq
proof (intro allI iffI)
fix S
assume "openin sub.mtopology S"
then have "∃T. openin (subtopology mtopology A) T ∧ x ∈ T ∧ T ⊆ S" if "x ∈ S" for x
by (metis mball_submetric_eq openin_mball openin_subtopology_Int2 sub.centre_in_mball_iff sub.openin_mtopology subsetD that)
then show "openin (subtopology mtopology A) S"
by (meson openin_subopen)
next
fix S
assume "openin (subtopology mtopology A) S"
then obtain T where "openin mtopology T" "S = T ∩ A"
by (meson openin_subtopology)
then have "mopen T"
by (simp add: mopen_def openin_mtopology)
then have "sub.mopen (T ∩ A)"
unfolding sub.mopen_def mopen_def
by (metis inf.coboundedI2 mball_submetric_eq Int_iff ‹S = T ∩ A› inf.bounded_iff subsetI)
then show "openin sub.mtopology S"
using ‹S = T ∩ A› sub.mopen_def sub.openin_mtopology by force
qed
lemma mbounded_submetric: "sub.mbounded T ⟷ mbounded T ∧ T ⊆ A"
by (meson mbounded_alt sub.mbounded_alt subset subset_trans)
end
lemma (in Metric_space) submetric_empty [iff]: "Submetric M d {}"
proof qed auto
subsection ‹Abstract type of metric spaces›
typedef 'a metric = "{(M::'a set,d). Metric_space M d}"
morphisms "dest_metric" "metric"
proof -
have "Metric_space {} (λx y. 0)"
by (auto simp: Metric_space_def)
then show ?thesis
by blast
qed
definition mspace where "mspace m ≡ fst (dest_metric m)"
definition mdist where "mdist m ≡ snd (dest_metric m)"
lemma Metric_space_mspace_mdist [iff]: "Metric_space (mspace m) (mdist m)"
by (metis Product_Type.Collect_case_prodD dest_metric mdist_def mspace_def)
lemma mdist_nonneg [simp]: "⋀x y. 0 ≤ mdist m x y"
by (metis Metric_space_def Metric_space_mspace_mdist)
lemma mdist_commute: "⋀x y. mdist m x y = mdist m y x"
by (metis Metric_space_def Metric_space_mspace_mdist)
lemma mdist_zero [simp]: "⋀x y. ⟦x ∈ mspace m; y ∈ mspace m⟧ ⟹ mdist m x y = 0 ⟷ x=y"
by (meson Metric_space.zero Metric_space_mspace_mdist)
lemma mdist_triangle: "⋀x y z. ⟦x ∈ mspace m; y ∈ mspace m; z ∈ mspace m⟧ ⟹ mdist m x z ≤ mdist m x y + mdist m y z"
by (meson Metric_space.triangle Metric_space_mspace_mdist)
lemma (in Metric_space) mspace_metric[simp]:
"mspace (metric (M,d)) = M"
by (simp add: metric_inverse mspace_def subspace)
lemma (in Metric_space) mdist_metric[simp]:
"mdist (metric (M,d)) = d"
by (simp add: mdist_def metric_inverse subspace)
lemma metric_collapse [simp]: "metric (mspace m, mdist m) = m"
by (simp add: dest_metric_inverse mdist_def mspace_def)
definition mtopology_of :: "'a metric ⇒ 'a topology"
where "mtopology_of ≡ λm. Metric_space.mtopology (mspace m) (mdist m)"
lemma topspace_mtopology_of [simp]: "topspace (mtopology_of m) = mspace m"
by (simp add: Metric_space.topspace_mtopology Metric_space_mspace_mdist mtopology_of_def)
lemma (in Metric_space) mtopology_of [simp]:
"mtopology_of (metric (M,d)) = mtopology"
by (simp add: mtopology_of_def)
definition "mball_of ≡ λm. Metric_space.mball (mspace m) (mdist m)"
lemma in_mball_of [simp]: "y ∈ mball_of m x r ⟷ x ∈ mspace m ∧ y ∈ mspace m ∧ mdist m x y < r"
by (simp add: Metric_space.in_mball mball_of_def)
lemma (in Metric_space) mball_of [simp]:
"mball_of (metric (M,d)) = mball"
by (simp add: mball_of_def)
definition "mcball_of ≡ λm. Metric_space.mcball (mspace m) (mdist m)"
lemma in_mcball_of [simp]: "y ∈ mcball_of m x r ⟷ x ∈ mspace m ∧ y ∈ mspace m ∧ mdist m x y ≤ r"
by (simp add: Metric_space.in_mcball mcball_of_def)
lemma (in Metric_space) mcball_of [simp]:
"mcball_of (metric (M,d)) = mcball"
by (simp add: mcball_of_def)
definition "euclidean_metric ≡ metric (UNIV,dist)"
lemma mspace_euclidean_metric [simp]: "mspace euclidean_metric = UNIV"
by (simp add: euclidean_metric_def)
lemma mdist_euclidean_metric [simp]: "mdist euclidean_metric = dist"
by (simp add: euclidean_metric_def)
lemma mtopology_of_euclidean [simp]: "mtopology_of euclidean_metric = euclidean"
by (simp add: Met_TC.mtopology_def mtopology_of_def)
text ‹Allows reference to the current metric space within the locale as a value›
definition (in Metric_space) "Self ≡ metric (M,d)"
lemma (in Metric_space) mspace_Self [simp]: "mspace Self = M"
by (simp add: Self_def)
lemma (in Metric_space) mdist_Self [simp]: "mdist Self = d"
by (simp add: Self_def)
text‹ Subspace of a metric space›
definition submetric where
"submetric ≡ λm S. metric (S ∩ mspace m, mdist m)"
lemma mspace_submetric [simp]: "mspace (submetric m S) = S ∩ mspace m"
unfolding submetric_def
by (meson Metric_space.subspace inf_le2 Metric_space_mspace_mdist Metric_space.mspace_metric)
lemma mdist_submetric [simp]: "mdist (submetric m S) = mdist m"
unfolding submetric_def
by (meson Metric_space.subspace inf_le2 Metric_space.mdist_metric Metric_space_mspace_mdist)
lemma submetric_UNIV [simp]: "submetric m UNIV = m"
by (simp add: submetric_def dest_metric_inverse mdist_def mspace_def)
lemma submetric_submetric [simp]:
"submetric (submetric m S) T = submetric m (S ∩ T)"
by (metis submetric_def Int_assoc inf_commute mdist_submetric mspace_submetric)
lemma submetric_mspace [simp]:
"submetric m (mspace m) = m"
by (simp add: submetric_def dest_metric_inverse mdist_def mspace_def)
lemma submetric_restrict:
"submetric m S = submetric m (mspace m ∩ S)"
by (metis submetric_mspace submetric_submetric)
lemma mtopology_of_submetric: "mtopology_of (submetric m A) = subtopology (mtopology_of m) A"
proof -
interpret Submetric "mspace m" "mdist m" "A ∩ mspace m"
using Metric_space_mspace_mdist Submetric.intro Submetric_axioms.intro inf_le2 by blast
have "sub.mtopology = subtopology (mtopology_of m) A"
by (metis inf_commute mtopology_of_def mtopology_submetric subtopology_mspace subtopology_subtopology)
then show ?thesis
by (simp add: submetric_def)
qed
subsection‹The discrete metric›
locale discrete_metric =
fixes M :: "'a set"
definition (in discrete_metric) dd :: "'a ⇒ 'a ⇒ real"
where "dd ≡ λx y::'a. if x=y then 0 else 1"
lemma metric_M_dd: "Metric_space M discrete_metric.dd"
by (simp add: discrete_metric.dd_def Metric_space.intro)
sublocale discrete_metric ⊆ disc: Metric_space M dd
by (simp add: metric_M_dd)
lemma (in discrete_metric) mopen_singleton:
assumes "x ∈ M" shows "disc.mopen {x}"
proof -
have "disc.mball x (1/2) ⊆ {x}"
by (smt (verit) dd_def disc.in_mball less_divide_eq_1_pos singleton_iff subsetI)
with assms show ?thesis
using disc.mopen_def half_gt_zero_iff zero_less_one by blast
qed
lemma (in discrete_metric) mtopology_discrete_metric:
"disc.mtopology = discrete_topology M"
proof -
have "⋀x. x ∈ M ⟹ openin disc.mtopology {x}"
by (simp add: disc.mtopology_def mopen_singleton)
then show ?thesis
by (metis disc.topspace_mtopology discrete_topology_unique)
qed
lemma (in discrete_metric) discrete_ultrametric:
"dd x z ≤ max (dd x y) (dd y z)"
by (simp add: dd_def)
lemma (in discrete_metric) dd_le1: "dd x y ≤ 1"
by (simp add: dd_def)
lemma (in discrete_metric) mbounded_discrete_metric: "disc.mbounded S ⟷ S ⊆ M"
by (meson dd_le1 disc.mbounded_alt)
subsection‹Metrizable spaces›
definition metrizable_space where
"metrizable_space X ≡ ∃M d. Metric_space M d ∧ X = Metric_space.mtopology M d"
lemma (in Metric_space) metrizable_space_mtopology: "metrizable_space mtopology"
using local.Metric_space_axioms metrizable_space_def by blast
lemma (in Metric_space) first_countable_mtopology: "first_countable mtopology"
proof (clarsimp simp add: first_countable_def)
fix x
assume "x ∈ M"
define ℬ where "ℬ ≡ mball x ` {r ∈ ℚ. 0 < r}"
show "∃ℬ. countable ℬ ∧ (∀V∈ℬ. openin mtopology V) ∧ (∀U. openin mtopology U ∧ x ∈ U ⟶ (∃V∈ℬ. x ∈ V ∧ V ⊆ U))"
proof (intro exI conjI ballI)
show "countable ℬ"
by (simp add: ℬ_def countable_rat)
show "∀U. openin mtopology U ∧ x ∈ U ⟶ (∃V∈ℬ. x ∈ V ∧ V ⊆ U)"
proof clarify
fix U
assume "openin mtopology U" and "x ∈ U"
then obtain r where "r>0" and r: "mball x r ⊆ U"
by (meson openin_mtopology)
then obtain q where "q ∈ Rats" "0 < q" "q < r"
using Rats_dense_in_real by blast
then show "∃V∈ℬ. x ∈ V ∧ V ⊆ U"
unfolding ℬ_def using ‹x ∈ M› r by fastforce
qed
qed (auto simp: ℬ_def)
qed
lemma metrizable_imp_first_countable:
"metrizable_space X ⟹ first_countable X"
by (force simp add: metrizable_space_def Metric_space.first_countable_mtopology)
lemma openin_mtopology_eq_open [simp]: "openin Met_TC.mtopology = open"
by (simp add: Met_TC.mtopology_def)
lemma closedin_mtopology_eq_closed [simp]: "closedin Met_TC.mtopology = closed"
proof -
have "(euclidean::'a topology) = Met_TC.mtopology"
by (simp add: Met_TC.mtopology_def)
then show ?thesis
using closed_closedin by fastforce
qed
lemma compactin_mtopology_eq_compact [simp]: "compactin Met_TC.mtopology = compact"
by (simp add: compactin_def compact_eq_Heine_Borel fun_eq_iff) meson
lemma metrizable_space_discrete_topology [simp]:
"metrizable_space(discrete_topology U)"
by (metis discrete_metric.mtopology_discrete_metric metric_M_dd metrizable_space_def)
lemma empty_metrizable_space: "metrizable_space trivial_topology"
by simp
lemma metrizable_space_subtopology:
assumes "metrizable_space X"
shows "metrizable_space(subtopology X S)"
proof -
obtain M d where "Metric_space M d" and X: "X = Metric_space.mtopology M d"
using assms metrizable_space_def by blast
then interpret Submetric M d "M ∩ S"
by (simp add: Submetric.intro Submetric_axioms_def)
show ?thesis
unfolding metrizable_space_def
by (metis X mtopology_submetric sub.Metric_space_axioms subtopology_restrict topspace_mtopology)
qed
lemma homeomorphic_metrizable_space_aux:
assumes "X homeomorphic_space Y" "metrizable_space X"
shows "metrizable_space Y"
proof -
obtain M d where "Metric_space M d" and X: "X = Metric_space.mtopology M d"
using assms by (auto simp: metrizable_space_def)
then interpret m: Metric_space M d
by simp
obtain f g where hmf: "homeomorphic_map X Y f" and hmg: "homeomorphic_map Y X g"
and fg: "(∀x ∈ M. g(f x) = x) ∧ (∀y ∈ topspace Y. f(g y) = y)"
using assms X homeomorphic_maps_map homeomorphic_space_def by fastforce
define d' where "d' x y ≡ d (g x) (g y)" for x y
interpret m': Metric_space "topspace Y" "d'"
unfolding d'_def
proof
show "(d (g x) (g y) = 0) = (x = y)" if "x ∈ topspace Y" "y ∈ topspace Y" for x y
by (metis fg X hmg homeomorphic_imp_surjective_map imageI m.topspace_mtopology m.zero that)
show "d (g x) (g z) ≤ d (g x) (g y) + d (g y) (g z)"
if "x ∈ topspace Y" and "y ∈ topspace Y" and "z ∈ topspace Y" for x y z
by (metis X that hmg homeomorphic_eq_everything_map imageI m.topspace_mtopology m.triangle)
qed (auto simp: m.nonneg m.commute)
have "Y = Metric_space.mtopology (topspace Y) d'"
unfolding topology_eq
proof (intro allI)
fix S
have "openin m'.mtopology S" if S: "S ⊆ topspace Y" and "openin X (g ` S)"
unfolding m'.openin_mtopology
proof (intro conjI that strip)
fix y
assume "y ∈ S"
then obtain r where "r>0" and r: "m.mball (g y) r ⊆ g ` S"
using X ‹openin X (g ` S)› m.openin_mtopology using ‹y ∈ S› by auto
then have "g ` m'.mball y r ⊆ m.mball (g y) r"
using X d'_def hmg homeomorphic_imp_surjective_map by fastforce
with S fg have "m'.mball y r ⊆ S"
by (smt (verit, del_insts) image_iff m'.in_mball r subset_iff)
then show "∃r>0. m'.mball y r ⊆ S"
using ‹0 < r› by blast
qed
moreover have "openin X (g ` S)" if ope': "openin m'.mtopology S"
proof -
have "∃r>0. m.mball (g y) r ⊆ g ` S" if "y ∈ S" for y
proof -
have y: "y ∈ topspace Y"
using m'.openin_mtopology ope' that by blast
obtain r where "r > 0" and r: "m'.mball y r ⊆ S"
using ope' by (meson ‹y ∈ S› m'.openin_mtopology)
moreover have "⋀x. ⟦x ∈ M; d (g y) x < r⟧ ⟹ ∃u. u ∈ topspace Y ∧ d' y u < r ∧ x = g u"
using fg X d'_def hmf homeomorphic_imp_surjective_map by fastforce
ultimately have "m.mball (g y) r ⊆ g ` m'.mball y r"
using y by (force simp: m'.openin_mtopology)
then show ?thesis
using ‹0 < r› r by blast
qed
then show ?thesis
using X hmg homeomorphic_imp_surjective_map m.openin_mtopology ope' openin_subset by fastforce
qed
ultimately have "(S ⊆ topspace Y ∧ openin X (g ` S)) = openin m'.mtopology S"
using m'.topspace_mtopology openin_subset by blast
then show "openin Y S = openin m'.mtopology S"
by (simp add: m'.mopen_def homeomorphic_map_openness_eq [OF hmg])
qed
then show ?thesis
using m'.metrizable_space_mtopology by force
qed
lemma homeomorphic_metrizable_space:
assumes "X homeomorphic_space Y"
shows "metrizable_space X ⟷ metrizable_space Y"
using assms homeomorphic_metrizable_space_aux homeomorphic_space_sym by metis
lemma metrizable_space_retraction_map_image:
"retraction_map X Y r ∧ metrizable_space X
⟹ metrizable_space Y"
using hereditary_imp_retractive_property metrizable_space_subtopology homeomorphic_metrizable_space
by blast
lemma metrizable_imp_Hausdorff_space:
"metrizable_space X ⟹ Hausdorff_space X"
by (metis Metric_space.Hausdorff_space_mtopology metrizable_space_def)
lemma metrizable_imp_t1_space:
"metrizable_space X ⟹ t1_space X"
by (simp add: Hausdorff_imp_t1_space metrizable_imp_Hausdorff_space)
lemma closed_imp_gdelta_in:
assumes X: "metrizable_space X" and S: "closedin X S"
shows "gdelta_in X S"
proof -
obtain M d where "Metric_space M d" and Xeq: "X = Metric_space.mtopology M d"
using X metrizable_space_def by blast
then interpret M: Metric_space M d
by blast
have "S ⊆ M"
using M.closedin_metric ‹X = M.mtopology› S by blast
show ?thesis
proof (cases "S = {}")
case True
then show ?thesis
by simp
next
case False
have "∃y∈S. d x y < inverse (1 + real n)" if "x ∈ S" for x n
using ‹S ⊆ M› M.mdist_zero [of x] that by force
moreover
have "x ∈ S" if "x ∈ M" and §: "⋀n. ∃y∈S. d x y < inverse(Suc n)" for x
proof -
have *: "∃y∈S. d x y < ε" if "ε > 0" for ε
by (metis § that not0_implies_Suc order_less_le order_less_le_trans real_arch_inverse)
have "closedin M.mtopology S"
using S by (simp add: Xeq)
then show ?thesis
apply (simp add: M.closedin_metric)
by (metis * ‹x ∈ M› M.in_mball disjnt_insert1 insert_absorb subsetD)
qed
ultimately have Seq: "S = ⋂(range (λn. {x∈M. ∃y∈S. d x y < inverse(Suc n)}))"
using ‹S ⊆ M› by force
have "openin M.mtopology {xa ∈ M. ∃y∈S. d xa y < inverse (1 + real n)}" for n
proof (clarsimp simp: M.openin_mtopology)
fix x y
assume "x ∈ M" "y ∈ S" and dxy: "d x y < inverse (1 + real n)"
then have "⋀z. ⟦z ∈ M; d x z < inverse (1 + real n) - d x y⟧ ⟹ ∃y∈S. d z y < inverse (1 + real n)"
by (smt (verit) M.commute M.triangle ‹S ⊆ M› in_mono)
with dxy show "∃r>0. M.mball x r ⊆ {z ∈ M. ∃y∈S. d z y < inverse (1 + real n)}"
by (rule_tac x="inverse(Suc n) - d x y" in exI) auto
qed
then show ?thesis
apply (subst Seq)
apply (force simp: Xeq intro: gdelta_in_Inter open_imp_gdelta_in)
done
qed
qed
lemma open_imp_fsigma_in:
"⟦metrizable_space X; openin X S⟧ ⟹ fsigma_in X S"
by (meson closed_imp_gdelta_in fsigma_in_gdelta_in openin_closedin openin_subset)
lemma metrizable_space_euclidean:
"metrizable_space (euclidean :: 'a::metric_space topology)"
using Met_TC.metrizable_space_mtopology by auto
lemma (in Metric_space) regular_space_mtopology:
"regular_space mtopology"
unfolding regular_space_def
proof clarify
fix C a
assume C: "closedin mtopology C" and a: "a ∈ topspace mtopology" and "a ∉ C"
have "openin mtopology (topspace mtopology - C)"
by (simp add: C openin_diff)
then obtain r where "r>0" and r: "mball a r ⊆ topspace mtopology - C"
unfolding openin_mtopology using ‹a ∉ C› a by auto
show "∃U V. openin mtopology U ∧ openin mtopology V ∧ a ∈ U ∧ C ⊆ V ∧ disjnt U V"
proof (intro exI conjI)
show "a ∈ mball a (r/2)"
using ‹0 < r› a by force
show "C ⊆ topspace mtopology - mcball a (r/2)"
using C ‹0 < r› r by (fastforce simp: closedin_metric)
qed (auto simp: openin_mball closedin_mcball openin_diff disjnt_iff)
qed
lemma metrizable_imp_regular_space:
"metrizable_space X ⟹ regular_space X"
by (metis Metric_space.regular_space_mtopology metrizable_space_def)
lemma regular_space_euclidean:
"regular_space (euclidean :: 'a::metric_space topology)"
by (simp add: metrizable_imp_regular_space metrizable_space_euclidean)
subsection‹Limits at a point in a topological space›
lemma (in Metric_space) eventually_atin_metric:
"eventually P (atin mtopology a) ⟷
(a ∈ M ⟶ (∃δ>0. ∀x. x ∈ M ∧ 0 < d x a ∧ d x a < δ ⟶ P x))" (is "?lhs=?rhs")
proof (cases "a ∈ M")
case True
show ?thesis
proof
assume L: ?lhs
with True obtain U where "openin mtopology U" "a ∈ U" and U: "∀x∈U - {a}. P x"
by (auto simp: eventually_atin)
then obtain r where "r>0" and "mball a r ⊆ U"
by (meson openin_mtopology)
with U show ?rhs
by (smt (verit, ccfv_SIG) commute in_mball insert_Diff_single insert_iff subset_iff)
next
assume ?rhs
then obtain δ where "δ>0" and δ: "∀x. x ∈ M ∧ 0 < d x a ∧ d x a < δ ⟶ P x"
using True by blast
then have "∀x ∈ mball a δ - {a}. P x"
by (simp add: commute)
then show ?lhs
unfolding eventually_atin openin_mtopology
by (metis True ‹0 < δ› centre_in_mball_iff openin_mball openin_mtopology)
qed
qed auto
subsection ‹Normal spaces and metric spaces›
lemma (in Metric_space) normal_space_mtopology:
"normal_space mtopology"
unfolding normal_space_def
proof clarify
fix S T
assume "closedin mtopology S"
then have "⋀x. x ∈ M - S ⟹ (∃r>0. mball x r ⊆ M - S)"
by (simp add: closedin_def openin_mtopology)
then obtain δ where d0: "⋀x. x ∈ M - S ⟹ δ x > 0 ∧ mball x (δ x) ⊆ M - S"
by metis
assume "closedin mtopology T"
then have "⋀x. x ∈ M - T ⟹ (∃r>0. mball x r ⊆ M - T)"
by (simp add: closedin_def openin_mtopology)
then obtain ε where e: "⋀x. x ∈ M - T ⟹ ε x > 0 ∧ mball x (ε x) ⊆ M - T"
by metis
assume "disjnt S T"
have "S ⊆ M" "T ⊆ M"
using ‹closedin mtopology S› ‹closedin mtopology T› closedin_metric by blast+
have δ: "⋀x. x ∈ T ⟹ δ x > 0 ∧ mball x (δ x) ⊆ M - S"
by (meson DiffI ‹T ⊆ M› ‹disjnt S T› d0 disjnt_iff subsetD)
have ε: "⋀x. x ∈ S ⟹ ε x > 0 ∧ mball x (ε x) ⊆ M - T"
by (meson Diff_iff ‹S ⊆ M› ‹disjnt S T› disjnt_iff e subsetD)
show "∃U V. openin mtopology U ∧ openin mtopology V ∧ S ⊆ U ∧ T ⊆ V ∧ disjnt U V"
proof (intro exI conjI)
show "openin mtopology (⋃x∈S. mball x (ε x / 2))" "openin mtopology (⋃x∈T. mball x (δ x / 2))"
by force+
show "S ⊆ (⋃x∈S. mball x (ε x / 2))"
using ε ‹S ⊆ M› by force
show "T ⊆ (⋃x∈T. mball x (δ x / 2))"
using δ ‹T ⊆ M› by force
show "disjnt (⋃x∈S. mball x (ε x / 2)) (⋃x∈T. mball x (δ x / 2))"
using ε δ
apply (clarsimp simp: disjnt_iff subset_iff)
by (smt (verit, ccfv_SIG) field_sum_of_halves triangle')
qed
qed
lemma metrizable_imp_normal_space:
"metrizable_space X ⟹ normal_space X"
by (metis Metric_space.normal_space_mtopology metrizable_space_def)
subsection‹Topological limitin in metric spaces›
lemma (in Metric_space) limitin_mspace:
"limitin mtopology f l F ⟹ l ∈ M"
using limitin_topspace by fastforce
lemma (in Metric_space) limitin_metric_unique:
"⟦limitin mtopology f l1 F; limitin mtopology f l2 F; F ≠ bot⟧ ⟹ l1 = l2"
by (meson Hausdorff_space_mtopology limitin_Hausdorff_unique)
lemma (in Metric_space) limitin_metric:
"limitin mtopology f l F ⟷ l ∈ M ∧ (∀ε>0. eventually (λx. f x ∈ M ∧ d (f x) l < ε) F)"
(is "?lhs=?rhs")
proof
assume L: ?lhs
show ?rhs
unfolding limitin_def
proof (intro conjI strip)
show "l ∈ M"
using L limitin_mspace by blast
fix ε::real
assume "ε>0"
then have "∀⇩F x in F. f x ∈ mball l ε"
using L openin_mball by (fastforce simp: limitin_def)
then show "∀⇩F x in F. f x ∈ M ∧ d (f x) l < ε"
using commute eventually_mono by fastforce
qed
next
assume R: ?rhs
then show ?lhs
by (force simp: limitin_def commute openin_mtopology subset_eq elim: eventually_mono)
qed
lemma (in Metric_space) limit_metric_sequentially:
"limitin mtopology f l sequentially ⟷
l ∈ M ∧ (∀ε>0. ∃N. ∀n≥N. f n ∈ M ∧ d (f n) l < ε)"
by (auto simp: limitin_metric eventually_sequentially)
lemma (in Submetric) limitin_submetric_iff:
"limitin sub.mtopology f l F ⟷
l ∈ A ∧ eventually (λx. f x ∈ A) F ∧ limitin mtopology f l F" (is "?lhs=?rhs")
by (simp add: limitin_subtopology mtopology_submetric)
lemma (in Metric_space) metric_closedin_iff_sequentially_closed:
"closedin mtopology S ⟷
S ⊆ M ∧ (∀σ l. range σ ⊆ S ∧ limitin mtopology σ l sequentially ⟶ l ∈ S)" (is "?lhs=?rhs")
proof
assume ?lhs then show ?rhs
by (force simp: closedin_metric limitin_closedin range_subsetD)
next
assume R: ?rhs
show ?lhs
unfolding closedin_metric
proof (intro conjI strip)
show "S ⊆ M"
using R by blast
fix x
assume "x ∈ M - S"
have False if "∀r>0. ∃y. y ∈ M ∧ y ∈ S ∧ d x y < r"
proof -
have "∀n. ∃y. y ∈ M ∧ y ∈ S ∧ d x y < inverse(Suc n)"
using that by auto
then obtain σ where σ: "⋀n. σ n ∈ M ∧ σ n ∈ S ∧ d x (σ n) < inverse(Suc n)"
by metis
then have "range σ ⊆ M"
by blast
have "∃N. ∀n≥N. d x (σ n) < ε" if "ε>0" for ε
proof -
have "real (Suc (nat ⌈inverse ε⌉)) ≥ inverse ε"
by linarith
then have "∀n ≥ nat ⌈inverse ε⌉. d x (σ n) < ε"
by (metis σ inverse_inverse_eq inverse_le_imp_le nat_ceiling_le_eq nle_le not_less_eq_eq order.strict_trans2 that)
then show ?thesis ..
qed
with σ have "limitin mtopology σ x sequentially"
using ‹x ∈ M - S› commute limit_metric_sequentially by auto
then show ?thesis
by (metis R DiffD2 σ image_subset_iff ‹x ∈ M - S›)
qed
then show "∃r>0. disjnt S (mball x r)"
by (meson disjnt_iff in_mball)
qed
qed
lemma (in Metric_space) limit_atin_metric:
"limitin X f y (atin mtopology x) ⟷
y ∈ topspace X ∧
(x ∈ M
⟶ (∀V. openin X V ∧ y ∈ V
⟶ (∃δ>0. ∀x'. x' ∈ M ∧ 0 < d x' x ∧ d x' x < δ ⟶ f x' ∈ V)))"
by (force simp: limitin_def eventually_atin_metric)
lemma (in Metric_space) limitin_metric_dist_null:
"limitin mtopology f l F ⟷ l ∈ M ∧ eventually (λx. f x ∈ M) F ∧ ((λx. d (f x) l) ⤏ 0) F"
by (simp add: limitin_metric tendsto_iff eventually_conj_iff all_conj_distrib imp_conjR gt_ex)
subsection‹Cauchy sequences and complete metric spaces›
context Metric_space
begin
definition MCauchy :: "(nat ⇒ 'a) ⇒ bool"
where "MCauchy σ ≡ range σ ⊆ M ∧ (∀ε>0. ∃N. ∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d (σ n) (σ n') < ε)"
definition mcomplete
where "mcomplete ≡ (∀σ. MCauchy σ ⟶ (∃x. limitin mtopology σ x sequentially))"
lemma mcomplete_empty [iff]: "Metric_space.mcomplete {} d"
by (simp add: Metric_space.MCauchy_def Metric_space.mcomplete_def subspace)
lemma MCauchy_imp_MCauchy_suffix: "MCauchy σ ⟹ MCauchy (σ ∘ (+)n)"
unfolding MCauchy_def image_subset_iff comp_apply
by (metis UNIV_I add.commute trans_le_add1)
lemma mcomplete:
"mcomplete ⟷
(∀σ. (∀⇩F n in sequentially. σ n ∈ M) ∧
(∀ε>0. ∃N. ∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d (σ n) (σ n') < ε) ⟶
(∃x. limitin mtopology σ x sequentially))" (is "?lhs=?rhs")
proof
assume L: ?lhs
show ?rhs
proof clarify
fix σ
assume "∀⇩F n in sequentially. σ n ∈ M"
and σ: "∀ε>0. ∃N. ∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d (σ n) (σ n') < ε"
then obtain N where "⋀n. n≥N ⟹ σ n ∈ M"
by (auto simp: eventually_sequentially)
with σ have "MCauchy (σ ∘ (+)N)"
unfolding MCauchy_def image_subset_iff comp_apply by (meson le_add1 trans_le_add2)
then obtain x where "limitin mtopology (σ ∘ (+)N) x sequentially"
using L MCauchy_imp_MCauchy_suffix mcomplete_def by blast
then have "limitin mtopology σ x sequentially"
unfolding o_def by (auto simp: add.commute limitin_sequentially_offset_rev)
then show "∃x. limitin mtopology σ x sequentially" ..
qed
qed (simp add: mcomplete_def MCauchy_def image_subset_iff)
lemma mcomplete_empty_mspace: "M = {} ⟹ mcomplete"
using MCauchy_def mcomplete_def by blast
lemma MCauchy_const [simp]: "MCauchy (λn. a) ⟷ a ∈ M"
using MCauchy_def mdist_zero by auto
lemma convergent_imp_MCauchy:
assumes "range σ ⊆ M" and lim: "limitin mtopology σ l sequentially"
shows "MCauchy σ"
unfolding MCauchy_def image_subset_iff
proof (intro conjI strip)
fix ε::real
assume "ε > 0"
then have "∀⇩F n in sequentially. σ n ∈ M ∧ d (σ n) l < ε/2"
using half_gt_zero lim limitin_metric by blast
then obtain N where "⋀n. n≥N ⟹ σ n ∈ M ∧ d (σ n) l < ε/2"
by (force simp: eventually_sequentially)
then show "∃N. ∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d (σ n) (σ n') < ε"
by (smt (verit) limitin_mspace mdist_reverse_triangle field_sum_of_halves lim)
qed (use assms in blast)
lemma mcomplete_alt:
"mcomplete ⟷ (∀σ. MCauchy σ ⟷ range σ ⊆ M ∧ (∃x. limitin mtopology σ x sequentially))"
using MCauchy_def convergent_imp_MCauchy mcomplete_def by blast
lemma MCauchy_subsequence:
assumes "strict_mono r" "MCauchy σ"
shows "MCauchy (σ ∘ r)"
proof -
have "d (σ (r n)) (σ (r n')) < ε"
if "N ≤ n" "N ≤ n'" "strict_mono r" "∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d (σ n) (σ n') < ε"
for ε N n n'
using that by (meson le_trans strict_mono_imp_increasing)
moreover have "range (λx. σ (r x)) ⊆ M"
using MCauchy_def assms by blast
ultimately show ?thesis
using assms by (simp add: MCauchy_def) metis
qed
lemma MCauchy_offset:
assumes cau: "MCauchy (σ ∘ (+)k)" and σ: "⋀n. n < k ⟹ σ n ∈ M"
shows "MCauchy σ"
unfolding MCauchy_def image_subset_iff
proof (intro conjI strip)
fix n
show "σ n ∈ M"
using assms
unfolding MCauchy_def image_subset_iff
by (metis UNIV_I comp_apply le_iff_add linorder_not_le)
next
fix ε :: real
assume "ε > 0"
obtain N where "∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d ((σ ∘ (+)k) n) ((σ ∘ (+)k) n') < ε"
using cau ‹ε > 0› by (fastforce simp: MCauchy_def)
then show "∃N. ∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d (σ n) (σ n') < ε"
unfolding o_def
apply (rule_tac x="k+N" in exI)
by (smt (verit, del_insts) add.assoc le_add1 less_eqE)
qed
lemma MCauchy_convergent_subsequence:
assumes cau: "MCauchy σ" and "strict_mono r"
and lim: "limitin mtopology (σ ∘ r) a sequentially"
shows "limitin mtopology σ a sequentially"
unfolding limitin_metric
proof (intro conjI strip)
show "a ∈ M"
by (meson assms limitin_mspace)
fix ε :: real
assume "ε > 0"
then obtain N1 where N1: "⋀n n'. ⟦n≥N1; n'≥N1⟧ ⟹ d (σ n) (σ n') < ε/2"
using cau unfolding MCauchy_def by (meson half_gt_zero)
obtain N2 where N2: "⋀n. n ≥ N2 ⟹ (σ ∘ r) n ∈ M ∧ d ((σ ∘ r) n) a < ε/2"
by (metis (no_types, lifting) lim ‹ε > 0› half_gt_zero limit_metric_sequentially)
have "σ n ∈ M ∧ d (σ n) a < ε" if "n ≥ max N1 N2" for n
proof (intro conjI)
show "σ n ∈ M"
using MCauchy_def cau by blast
have "N1 ≤ r n"
by (meson ‹strict_mono r› le_trans max.cobounded1 strict_mono_imp_increasing that)
then show "d (σ n) a < ε"
using N1[of n "r n"] N2[of n] ‹σ n ∈ M› ‹a ∈ M› triangle that by fastforce
qed
then show "∀⇩F n in sequentially. σ n ∈ M ∧ d (σ n) a < ε"
using eventually_sequentially by blast
qed
lemma MCauchy_interleaving_gen:
"MCauchy (λn. if even n then x(n div 2) else y(n div 2)) ⟷
(MCauchy x ∧ MCauchy y ∧ (λn. d (x n) (y n)) ⇢ 0)" (is "?lhs=?rhs")
proof
assume L: ?lhs
have evens: "strict_mono (λn::nat. 2 * n)" and odds: "strict_mono (λn::nat. Suc (2 * n))"
by (auto simp: strict_mono_def)
show ?rhs
proof (intro conjI)
show "MCauchy x" "MCauchy y"
using MCauchy_subsequence [OF evens L] MCauchy_subsequence [OF odds L] by (auto simp: o_def)
show "(λn. d (x n) (y n)) ⇢ 0"
unfolding LIMSEQ_iff
proof (intro strip)
fix ε :: real
assume "ε > 0"
then obtain N where N:
"⋀n n'. ⟦n≥N; n'≥N⟧ ⟹ d (if even n then x (n div 2) else y (n div 2))
(if even n' then x (n' div 2) else y (n' div 2)) < ε"
using L MCauchy_def by fastforce
have "d (x n) (y n) < ε" if "n≥N" for n
using N [of "2*n" "Suc(2*n)"] that by auto
then show "∃N. ∀n≥N. norm (d (x n) (y n) - 0) < ε"
by auto
qed
qed
next
assume R: ?rhs
show ?lhs
unfolding MCauchy_def
proof (intro conjI strip)
show "range (λn. if even n then x (n div 2) else y (n div 2)) ⊆ M"
using R by (auto simp: MCauchy_def)
fix ε :: real
assume "ε > 0"
obtain Nx where Nx: "⋀n n'. ⟦n≥Nx; n'≥Nx⟧ ⟹ d (x n) (x n') < ε/2"
by (meson half_gt_zero MCauchy_def R ‹ε > 0›)
obtain Ny where Ny: "⋀n n'. ⟦n≥Ny; n'≥Ny⟧ ⟹ d (y n) (y n') < ε/2"
by (meson half_gt_zero MCauchy_def R ‹ε > 0›)
obtain Nxy where Nxy: "⋀n. n≥Nxy ⟹ d (x n) (y n) < ε/2"
using R ‹ε > 0› half_gt_zero unfolding LIMSEQ_iff
by (metis abs_mdist diff_zero real_norm_def)
define N where "N ≡ 2 * Max{Nx,Ny,Nxy}"
show "∃N. ∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d (if even n then x (n div 2) else y (n div 2)) (if even n' then x (n' div 2) else y (n' div 2)) < ε"
proof (intro exI strip)
fix n n'
assume "N ≤ n" and "N ≤ n'"
then have "n div 2 ≥ Nx" "n div 2 ≥ Ny" "n div 2 ≥ Nxy" "n' div 2 ≥ Nx" "n' div 2 ≥ Ny"
by (auto simp: N_def)
then have dxyn: "d (x (n div 2)) (y (n div 2)) < ε/2"
and dxnn': "d (x (n div 2)) (x (n' div 2)) < ε/2"
and dynn': "d (y (n div 2)) (y (n' div 2)) < ε/2"
using Nx Ny Nxy by blast+
have inM: "x (n div 2) ∈ M" "x (n' div 2) ∈ M""y (n div 2) ∈ M" "y (n' div 2) ∈ M"
using MCauchy_def R by blast+
show "d (if even n then x (n div 2) else y (n div 2)) (if even n' then x (n' div 2) else y (n' div 2)) < ε"
proof (cases "even n")
case nt: True
show ?thesis
proof (cases "even n'")
case True
with ‹ε > 0› nt dxnn' show ?thesis by auto
next
case False
with nt dxyn dynn' inM triangle show ?thesis
by fastforce
qed
next
case nf: False
show ?thesis
proof (cases "even n'")
case True
then show ?thesis
by (smt (verit) ‹ε > 0› dxyn dxnn' triangle commute inM field_sum_of_halves)
next
case False
with ‹ε > 0› nf dynn' show ?thesis by auto
qed
qed
qed
qed
qed
lemma MCauchy_interleaving:
"MCauchy (λn. if even n then σ(n div 2) else a) ⟷
range σ ⊆ M ∧ limitin mtopology σ a sequentially" (is "?lhs=?rhs")
proof -
have "?lhs ⟷ (MCauchy σ ∧ a ∈ M ∧ (λn. d (σ n) a) ⇢ 0)"
by (simp add: MCauchy_interleaving_gen [where y = "λn. a"])
also have "... = ?rhs"
by (metis MCauchy_def always_eventually convergent_imp_MCauchy limitin_metric_dist_null range_subsetD)
finally show ?thesis .
qed
lemma mcomplete_nest:
"mcomplete ⟷
(∀C::nat ⇒'a set. (∀n. closedin mtopology (C n)) ∧
(∀n. C n ≠ {}) ∧ decseq C ∧ (∀ε>0. ∃n a. C n ⊆ mcball a ε)
⟶ ⋂ (range C) ≠ {})" (is "?lhs=?rhs")
proof
assume L: ?lhs
show ?rhs
unfolding imp_conjL
proof (intro strip)
fix C :: "nat ⇒ 'a set"
assume clo: "∀n. closedin mtopology (C n)"
and ne: "∀n. C n ≠ ({}::'a set)"
and dec: "decseq C"
and cover [rule_format]: "∀ε>0. ∃n a. C n ⊆ mcball a ε"
obtain σ where σ: "⋀n. σ n ∈ C n"
by (meson ne empty_iff set_eq_iff)
have "MCauchy σ"
unfolding MCauchy_def
proof (intro conjI strip)
show "range σ ⊆ M"
using σ clo metric_closedin_iff_sequentially_closed by auto
fix ε :: real
assume "ε > 0"
then obtain N a where N: "C N ⊆ mcball a (ε/3)"
using cover by fastforce
have "d (σ m) (σ n) < ε" if "N ≤ m" "N ≤ n" for m n
proof -
have "d a (σ m) ≤ ε/3" "d a (σ n) ≤ ε/3"
using dec N σ that by (fastforce simp: decseq_def)+
then have "d (σ m) (σ n) ≤ ε/3 + ε/3"
using triangle σ commute dec decseq_def subsetD that N
by (smt (verit, ccfv_threshold) in_mcball)
also have "... < ε"
using ‹ε > 0› by auto
finally show ?thesis .
qed
then show "∃N. ∀m n. N ≤ m ⟶ N ≤ n ⟶ d (σ m) (σ n) < ε"
by blast
qed
then obtain x where x: "limitin mtopology σ x sequentially"
using L mcomplete_def by blast
have "x ∈ C n" for n
proof (rule limitin_closedin [OF x])
show "closedin mtopology (C n)"
by (simp add: clo)
show "∀⇩F x in sequentially. σ x ∈ C n"
by (metis σ dec decseq_def eventually_sequentiallyI subsetD)
qed auto
then show "⋂ (range C) ≠ {}"
by blast
qed
next
assume R: ?rhs
show ?lhs
unfolding mcomplete_def
proof (intro strip)
fix σ
assume "MCauchy σ"
then have "range σ ⊆ M"
using MCauchy_def by blast
define C where "C ≡ λn. mtopology closure_of (σ ` {n..})"
have "∀n. closedin mtopology (C n)"
by (auto simp: C_def)
moreover
have ne: "⋀n. C n ≠ {}"
using ‹MCauchy σ› by (auto simp: C_def MCauchy_def disjnt_iff closure_of_eq_empty_gen)
moreover
have dec: "decseq C"
unfolding monotone_on_def
proof (intro strip)
fix m n::nat
assume "m ≤ n"
then have "{n..} ⊆ {m..}"
by auto
then show "C n ⊆ C m"
unfolding C_def by (meson closure_of_mono image_mono)
qed
moreover
have C: "∃N u. C N ⊆ mcball u ε" if "ε>0" for ε
proof -
obtain N where "⋀m n. N ≤ m ∧ N ≤ n ⟹ d (σ m) (σ n) < ε"
by (meson MCauchy_def ‹0 < ε› ‹MCauchy σ›)
then have "σ ` {N..} ⊆ mcball (σ N) ε"
using MCauchy_def ‹MCauchy σ› by (force simp: less_eq_real_def)
then have "C N ⊆ mcball (σ N) ε"
by (simp add: C_def closure_of_minimal)
then show ?thesis
by blast
qed
ultimately obtain l where x: "l ∈ ⋂ (range C)"
by (metis R ex_in_conv)
then have *: "⋀ε N. 0 < ε ⟹ ∃n'. N ≤ n' ∧ l ∈ M ∧ σ n' ∈ M ∧ d l (σ n') < ε"
by (force simp: C_def metric_closure_of)
then have "l ∈ M"
using gt_ex by blast
show "∃l. limitin mtopology σ l sequentially"
unfolding limitin_metric
proof (intro conjI strip exI)
show "l ∈ M"
using ‹∀n. closedin mtopology (C n)› closedin_subset x by fastforce
fix ε::real
assume "ε > 0"
obtain N where N: "⋀m n. N ≤ m ∧ N ≤ n ⟹ d (σ m) (σ n) < ε/2"
by (meson MCauchy_def ‹0 < ε› ‹MCauchy σ› half_gt_zero)
with * [of "ε/2" N]
have "∀n≥N. σ n ∈ M ∧ d (σ n) l < ε"
by (smt (verit) ‹range σ ⊆ M› commute field_sum_of_halves range_subsetD triangle)
then show "∀⇩F n in sequentially. σ n ∈ M ∧ d (σ n) l < ε"
using eventually_sequentially by blast
qed
qed
qed
lemma mcomplete_nest_sing:
"mcomplete ⟷
(∀C. (∀n. closedin mtopology (C n)) ∧
(∀n. C n ≠ {}) ∧ decseq C ∧ (∀e>0. ∃n a. C n ⊆ mcball a e)
⟶ (∃l. l ∈ M ∧ ⋂ (range C) = {l}))"
proof -
have *: False
if clo: "∀n. closedin mtopology (C n)"
and cover: "∀ε>0. ∃n a. C n ⊆ mcball a ε"
and no_sing: "⋀y. y ∈ M ⟹ ⋂ (range C) ≠ {y}"
and l: "∀n. l ∈ C n"
for C :: "nat ⇒ 'a set" and l
proof -
have inM: "⋀x. x ∈ ⋂ (range C) ⟹ x ∈ M"
using closedin_metric clo by fastforce
then have "l ∈ M"
by (simp add: l)
have False if l': "l' ∈ ⋂ (range C)" and "l' ≠ l" for l'
proof -
have "l' ∈ M"
using inM l' by blast
obtain n a where na: "C n ⊆ mcball a (d l l' / 3)"
using inM ‹l ∈ M› l' ‹l' ≠ l› cover by force
then have "d a l ≤ (d l l' / 3)" "d a l' ≤ (d l l' / 3)" "a ∈ M"
using l l' na in_mcball by auto
then have "d l l' ≤ (d l l' / 3) + (d l l' / 3)"
using ‹l ∈ M› ‹l' ∈ M› mdist_reverse_triangle by fastforce
then show False
using nonneg [of l l'] ‹l' ≠ l› ‹l ∈ M› ‹l' ∈ M› zero by force
qed
then show False
by (metis l ‹l ∈ M› no_sing INT_I empty_iff insertI1 is_singletonE is_singletonI')
qed
show ?thesis
unfolding mcomplete_nest imp_conjL
apply (intro all_cong1 imp_cong refl)
using *
by (smt (verit) Inter_iff ex_in_conv range_constant range_eqI)
qed
lemma mcomplete_fip:
"mcomplete ⟷
(∀𝒞. (∀C ∈ 𝒞. closedin mtopology C) ∧
(∀e>0. ∃C a. C ∈ 𝒞 ∧ C ⊆ mcball a e) ∧ (∀ℱ. finite ℱ ∧ ℱ ⊆ 𝒞 ⟶ ⋂ ℱ ≠ {})
⟶ ⋂ 𝒞 ≠ {})"
(is "?lhs = ?rhs")
proof
assume L: ?lhs
show ?rhs
unfolding mcomplete_nest_sing imp_conjL
proof (intro strip)
fix 𝒞 :: "'a set set"
assume clo: "∀C∈𝒞. closedin mtopology C"
and cover: "∀e>0. ∃C a. C ∈ 𝒞 ∧ C ⊆ mcball a e"
and fip: "∀ℱ. finite ℱ ⟶ ℱ ⊆ 𝒞 ⟶ ⋂ ℱ ≠ {}"
then have "∀n. ∃C. C ∈ 𝒞 ∧ (∃a. C ⊆ mcball a (inverse (Suc n)))"
by simp
then obtain C where C: "⋀n. C n ∈ 𝒞"
and coverC: "⋀n. ∃a. C n ⊆ mcball a (inverse (Suc n))"
by metis
define D where "D ≡ λn. ⋂ (C ` {..n})"
have cloD: "closedin mtopology (D n)" for n
unfolding D_def using clo C by blast
have neD: "D n ≠ {}" for n
using fip C by (simp add: D_def image_subset_iff)
have decD: "decseq D"
by (force simp: D_def decseq_def)
have coverD: "∃n a. D n ⊆ mcball a ε" if " ε >0" for ε
proof -
obtain n where "inverse (Suc n) < ε"
using ‹0 < ε› reals_Archimedean by blast
then obtain a where "C n ⊆ mcball a ε"
by (meson coverC less_eq_real_def mcball_subset_concentric order_trans)
then show ?thesis
unfolding D_def by blast
qed
have *: "a ∈ ⋂𝒞" if a: "⋂ (range D) = {a}" and "a ∈ M" for a
proof -
have aC: "a ∈ C n" for n
using that by (auto simp: D_def)
have eqa: "⋀u. (∀n. u ∈ C n) ⟹ a = u"
using that by (auto simp: D_def)
have "a ∈ T" if "T ∈ 𝒞" for T
proof -
have cloT: "closedin mtopology (T ∩ D n)" for n
using clo cloD that by blast
have "⋂ (insert T (C ` {..n})) ≠ {}" for n
using that C by (intro fip [rule_format]) auto
then have neT: "T