src/HOL/Real_Vector_Spaces.thy
changeset 62101 26c0a70f78a3
parent 62087 44841d07ef1d
child 62102 877463945ce9
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Fri Jan 08 16:37:56 2016 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Fri Jan 08 17:40:59 2016 +0100
     1.3 @@ -191,7 +191,7 @@
     1.4    fixes x :: "'a::real_vector"
     1.5    shows "scaleR (-1) x = - x"
     1.6    using scaleR_minus_left [of 1 x] by simp
     1.7 -  
     1.8 +
     1.9  class real_algebra = real_vector + ring +
    1.10    assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)"
    1.11    and mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)"
    1.12 @@ -662,10 +662,19 @@
    1.13  class dist_norm = dist + norm + minus +
    1.14    assumes dist_norm: "dist x y = norm (x - y)"
    1.15  
    1.16 -class open_dist = "open" + dist +
    1.17 -  assumes open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.18 +class uniformity_dist = dist + uniformity +
    1.19 +  assumes uniformity_dist: "uniformity = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    1.20 +begin
    1.21  
    1.22 -class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist +
    1.23 +lemma eventually_uniformity_metric:
    1.24 +  "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x y. dist x y < e \<longrightarrow> P (x, y))"
    1.25 +  unfolding uniformity_dist
    1.26 +  by (subst eventually_INF_base)
    1.27 +     (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
    1.28 +
    1.29 +end
    1.30 +
    1.31 +class real_normed_vector = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
    1.32    assumes norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
    1.33    and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
    1.34    and norm_scaleR [simp]: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
    1.35 @@ -686,8 +695,8 @@
    1.36  
    1.37  class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra +
    1.38    assumes norm_one [simp]: "norm 1 = 1"
    1.39 -  
    1.40 -lemma (in real_normed_algebra_1) scaleR_power [simp]: 
    1.41 +
    1.42 +lemma (in real_normed_algebra_1) scaleR_power [simp]:
    1.43    "(scaleR x y) ^ n = scaleR (x^n) (y^n)"
    1.44    by (induction n) (simp_all add: scaleR_one scaleR_scaleR mult_ac)
    1.45  
    1.46 @@ -1010,7 +1019,7 @@
    1.47  
    1.48  subsection \<open>Metric spaces\<close>
    1.49  
    1.50 -class metric_space = open_dist +
    1.51 +class metric_space = uniformity_dist + open_uniformity +
    1.52    assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
    1.53    assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
    1.54  begin
    1.55 @@ -1074,26 +1083,23 @@
    1.56    shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
    1.57  by (rule dist_triangle_half_l, simp_all add: dist_commute)
    1.58  
    1.59 -subclass topological_space
    1.60 +subclass uniform_space
    1.61  proof
    1.62 -  have "\<exists>e::real. 0 < e"
    1.63 -    by (blast intro: zero_less_one)
    1.64 -  then show "open UNIV"
    1.65 -    unfolding open_dist by simp
    1.66 -next
    1.67 -  fix S T assume "open S" "open T"
    1.68 -  then show "open (S \<inter> T)"
    1.69 -    unfolding open_dist
    1.70 -    apply clarify
    1.71 -    apply (drule (1) bspec)+
    1.72 -    apply (clarify, rename_tac r s)
    1.73 -    apply (rule_tac x="min r s" in exI, simp)
    1.74 -    done
    1.75 -next
    1.76 -  fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
    1.77 -    unfolding open_dist by (meson UnionE UnionI) 
    1.78 +  fix E x assume "eventually E uniformity"
    1.79 +  then obtain e where E: "0 < e" "\<And>x y. dist x y < e \<Longrightarrow> E (x, y)"
    1.80 +    unfolding eventually_uniformity_metric by auto
    1.81 +  then show "E (x, x)" "\<forall>\<^sub>F (x, y) in uniformity. E (y, x)"
    1.82 +    unfolding eventually_uniformity_metric by (auto simp: dist_commute)
    1.83 +
    1.84 +  show "\<exists>D. eventually D uniformity \<and> (\<forall>x y z. D (x, y) \<longrightarrow> D (y, z) \<longrightarrow> E (x, z))"
    1.85 +    using E dist_triangle_half_l[where e=e] unfolding eventually_uniformity_metric
    1.86 +    by (intro exI[of _ "\<lambda>(x, y). dist x y < e / 2"] exI[of _ "e/2"] conjI)
    1.87 +       (auto simp: dist_commute)
    1.88  qed
    1.89  
    1.90 +lemma open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.91 +  unfolding open_uniformity eventually_uniformity_metric by (simp add: dist_commute)
    1.92 +
    1.93  lemma open_ball: "open {y. dist x y < d}"
    1.94  proof (unfold open_dist, intro ballI)
    1.95    fix y assume *: "y \<in> {y. dist x y < d}"
    1.96 @@ -1156,8 +1162,11 @@
    1.97  definition dist_real_def:
    1.98    "dist x y = \<bar>x - y\<bar>"
    1.99  
   1.100 +definition uniformity_real_def [code del]:
   1.101 +  "(uniformity :: (real \<times> real) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
   1.102 +
   1.103  definition open_real_def [code del]:
   1.104 -  "open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   1.105 +  "open (U :: real set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
   1.106  
   1.107  definition real_norm_def [simp]:
   1.108    "norm r = \<bar>r\<bar>"
   1.109 @@ -1165,8 +1174,9 @@
   1.110  instance
   1.111  apply (intro_classes, unfold real_norm_def real_scaleR_def)
   1.112  apply (rule dist_real_def)
   1.113 +apply (simp add: sgn_real_def)
   1.114 +apply (rule uniformity_real_def)
   1.115  apply (rule open_real_def)
   1.116 -apply (simp add: sgn_real_def)
   1.117  apply (rule abs_eq_0)
   1.118  apply (rule abs_triangle_ineq)
   1.119  apply (rule abs_mult)
   1.120 @@ -1188,7 +1198,7 @@
   1.121    proof (rule ext, safe)
   1.122      fix S :: "real set" assume "open S"
   1.123      then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
   1.124 -      unfolding open_real_def bchoice_iff ..
   1.125 +      unfolding open_dist bchoice_iff ..
   1.126      then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
   1.127        by (fastforce simp: dist_real_def)
   1.128      show "generate_topology (range lessThan \<union> range greaterThan) S"
   1.129 @@ -1199,14 +1209,14 @@
   1.130    next
   1.131      fix S :: "real set" assume "generate_topology (range lessThan \<union> range greaterThan) S"
   1.132      moreover have "\<And>a::real. open {..<a}"
   1.133 -      unfolding open_real_def dist_real_def
   1.134 +      unfolding open_dist dist_real_def
   1.135      proof clarify
   1.136        fix x a :: real assume "x < a"
   1.137        hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
   1.138        thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
   1.139      qed
   1.140      moreover have "\<And>a::real. open {a <..}"
   1.141 -      unfolding open_real_def dist_real_def
   1.142 +      unfolding open_dist dist_real_def
   1.143      proof clarify
   1.144        fix x a :: real assume "a < x"
   1.145        hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
   1.146 @@ -1233,6 +1243,11 @@
   1.147  setup \<open>Sign.add_const_constraint
   1.148    (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
   1.149  
   1.150 +text \<open>Only allow @{term "uniformity"} in class \<open>uniform_space\<close>.\<close>
   1.151 +
   1.152 +setup \<open>Sign.add_const_constraint
   1.153 +  (@{const_name "uniformity"}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
   1.154 +
   1.155  text \<open>Only allow @{term dist} in class \<open>metric_space\<close>.\<close>
   1.156  
   1.157  setup \<open>Sign.add_const_constraint
   1.158 @@ -1786,10 +1801,22 @@
   1.159  
   1.160  subsection \<open>Cauchy sequences\<close>
   1.161  
   1.162 -definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
   1.163 -  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
   1.164 +lemma (in metric_space) Cauchy_def: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e)"
   1.165 +proof -
   1.166 +  have *: "eventually P (INF M. principal {(X m, X n) | n m. m \<ge> M \<and> n \<ge> M}) =
   1.167 +    (\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. P (X m, X n))" for P
   1.168 +  proof (subst eventually_INF_base, goal_cases)
   1.169 +    case (2 a b) then show ?case
   1.170 +      by (intro bexI[of _ "max a b"]) (auto simp: eventually_principal subset_eq)
   1.171 +  qed (auto simp: eventually_principal, blast)
   1.172 +  have "Cauchy X \<longleftrightarrow> (INF M. principal {(X m, X n) | n m. m \<ge> M \<and> n \<ge> M}) \<le> uniformity"
   1.173 +    unfolding Cauchy_uniform_iff le_filter_def * ..
   1.174 +  also have "\<dots> = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e)"
   1.175 +    unfolding uniformity_dist le_INF_iff by (auto simp: * le_principal)
   1.176 +  finally show ?thesis .
   1.177 +qed
   1.178  
   1.179 -lemma Cauchy_altdef:
   1.180 +lemma (in metric_space) Cauchy_altdef:
   1.181    "Cauchy f = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e)"
   1.182  proof
   1.183    assume A: "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e"
   1.184 @@ -1812,18 +1839,18 @@
   1.185    qed
   1.186  qed
   1.187  
   1.188 -lemma metric_CauchyI:
   1.189 +lemma (in metric_space) metric_CauchyI:
   1.190    "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
   1.191    by (simp add: Cauchy_def)
   1.192  
   1.193 -lemma CauchyI': "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
   1.194 +lemma (in metric_space) CauchyI': "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
   1.195    unfolding Cauchy_altdef by blast
   1.196  
   1.197 -lemma metric_CauchyD:
   1.198 +lemma (in metric_space) metric_CauchyD:
   1.199    "Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
   1.200    by (simp add: Cauchy_def)
   1.201  
   1.202 -lemma metric_Cauchy_iff2:
   1.203 +lemma (in metric_space) metric_Cauchy_iff2:
   1.204    "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < inverse(real (Suc j))))"
   1.205  apply (simp add: Cauchy_def, auto)
   1.206  apply (drule reals_Archimedean, safe)
   1.207 @@ -1837,40 +1864,118 @@
   1.208    "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
   1.209    unfolding metric_Cauchy_iff2 dist_real_def ..
   1.210  
   1.211 -lemma Cauchy_subseq_Cauchy:
   1.212 -  "\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)"
   1.213 -apply (auto simp add: Cauchy_def)
   1.214 -apply (drule_tac x=e in spec, clarify)
   1.215 -apply (rule_tac x=M in exI, clarify)
   1.216 -apply (blast intro: le_trans [OF _ seq_suble] dest!: spec)
   1.217 -done
   1.218 -
   1.219 -theorem LIMSEQ_imp_Cauchy:
   1.220 -  assumes X: "X \<longlonglongrightarrow> a" shows "Cauchy X"
   1.221 -proof (rule metric_CauchyI)
   1.222 -  fix e::real assume "0 < e"
   1.223 -  hence "0 < e/2" by simp
   1.224 -  with X have "\<exists>N. \<forall>n\<ge>N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D)
   1.225 -  then obtain N where N: "\<forall>n\<ge>N. dist (X n) a < e/2" ..
   1.226 -  show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e"
   1.227 -  proof (intro exI allI impI)
   1.228 -    fix m assume "N \<le> m"
   1.229 -    hence m: "dist (X m) a < e/2" using N by blast
   1.230 -    fix n assume "N \<le> n"
   1.231 -    hence n: "dist (X n) a < e/2" using N by blast
   1.232 -    have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a"
   1.233 -      by (rule dist_triangle2)
   1.234 -    also from m n have "\<dots> < e" by simp
   1.235 -    finally show "dist (X m) (X n) < e" .
   1.236 -  qed
   1.237 +lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
   1.238 +proof (subst lim_sequentially, intro allI impI exI)
   1.239 +  fix e :: real assume e: "e > 0"
   1.240 +  fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
   1.241 +  have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
   1.242 +  also note n
   1.243 +  finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
   1.244 +    by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
   1.245  qed
   1.246  
   1.247 -lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
   1.248 -unfolding convergent_def
   1.249 -by (erule exE, erule LIMSEQ_imp_Cauchy)
   1.250 +lemma (in metric_space) complete_def:
   1.251 +  shows "complete S = (\<forall>f. (\<forall>n. f n \<in> S) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>S. f \<longlonglongrightarrow> l))"
   1.252 +  unfolding complete_uniform
   1.253 +proof safe
   1.254 +  fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> S" "Cauchy f"
   1.255 +    and *: "\<forall>F\<le>principal S. F \<noteq> bot \<longrightarrow> cauchy_filter F \<longrightarrow> (\<exists>x\<in>S. F \<le> nhds x)"
   1.256 +  then show "\<exists>l\<in>S. f \<longlonglongrightarrow> l"
   1.257 +    unfolding filterlim_def using f
   1.258 +    by (intro *[rule_format])
   1.259 +       (auto simp: filtermap_sequentually_ne_bot le_principal eventually_filtermap Cauchy_uniform)
   1.260 +next
   1.261 +  fix F :: "'a filter" assume "F \<le> principal S" "F \<noteq> bot" "cauchy_filter F"
   1.262 +  assume seq: "\<forall>f. (\<forall>n. f n \<in> S) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>S. f \<longlonglongrightarrow> l)"
   1.263 +
   1.264 +  from \<open>F \<le> principal S\<close> \<open>cauchy_filter F\<close> have FF_le: "F \<times>\<^sub>F F \<le> uniformity_on S"
   1.265 +    by (simp add: cauchy_filter_def principal_prod_principal[symmetric] prod_filter_mono)
   1.266 +
   1.267 +  let ?P = "\<lambda>P e. eventually P F \<and> (\<forall>x. P x \<longrightarrow> x \<in> S) \<and> (\<forall>x y. P x \<longrightarrow> P y \<longrightarrow> dist x y < e)"
   1.268 +
   1.269 +  { fix \<epsilon> :: real assume "0 < \<epsilon>"
   1.270 +    then have "eventually (\<lambda>(x, y). x \<in> S \<and> y \<in> S \<and> dist x y < \<epsilon>) (uniformity_on S)"
   1.271 +      unfolding eventually_inf_principal eventually_uniformity_metric by auto
   1.272 +    from filter_leD[OF FF_le this] have "\<exists>P. ?P P \<epsilon>"
   1.273 +      unfolding eventually_prod_same by auto }
   1.274 +  note P = this
   1.275 +
   1.276 +  have "\<exists>P. \<forall>n. ?P (P n) (1 / Suc n) \<and> P (Suc n) \<le> P n"
   1.277 +  proof (rule dependent_nat_choice)
   1.278 +    show "\<exists>P. ?P P (1 / Suc 0)"
   1.279 +      using P[of 1] by auto
   1.280 +  next
   1.281 +    fix P n assume "?P P (1/Suc n)"
   1.282 +    moreover obtain Q where "?P Q (1 / Suc (Suc n))"
   1.283 +      using P[of "1/Suc (Suc n)"] by auto
   1.284 +    ultimately show "\<exists>Q. ?P Q (1 / Suc (Suc n)) \<and> Q \<le> P"
   1.285 +      by (intro exI[of _ "\<lambda>x. P x \<and> Q x"]) (auto simp: eventually_conj_iff)
   1.286 +  qed
   1.287 +  then obtain P where P: "\<And>n. eventually (P n) F" "\<And>n x. P n x \<Longrightarrow> x \<in> S"
   1.288 +    "\<And>n x y. P n x \<Longrightarrow> P n y \<Longrightarrow> dist x y < 1 / Suc n" "\<And>n. P (Suc n) \<le> P n"
   1.289 +    by metis
   1.290 +  have "antimono P"
   1.291 +    using P(4) unfolding decseq_Suc_iff le_fun_def by blast
   1.292 +
   1.293 +  obtain X where X: "\<And>n. P n (X n)"
   1.294 +    using P(1)[THEN eventually_happens'[OF \<open>F \<noteq> bot\<close>]] by metis
   1.295 +  have "Cauchy X"
   1.296 +    unfolding metric_Cauchy_iff2 inverse_eq_divide
   1.297 +  proof (intro exI allI impI)
   1.298 +    fix j m n :: nat assume "j \<le> m" "j \<le> n"
   1.299 +    with \<open>antimono P\<close> X have "P j (X m)" "P j (X n)"
   1.300 +      by (auto simp: antimono_def)
   1.301 +    then show "dist (X m) (X n) < 1 / Suc j"
   1.302 +      by (rule P)
   1.303 +  qed
   1.304 +  moreover have "\<forall>n. X n \<in> S"
   1.305 +    using P(2) X by auto
   1.306 +  ultimately obtain x where "X \<longlonglongrightarrow> x" "x \<in> S"
   1.307 +    using seq by blast
   1.308 +
   1.309 +  show "\<exists>x\<in>S. F \<le> nhds x"
   1.310 +  proof (rule bexI)
   1.311 +    { fix e :: real assume "0 < e"
   1.312 +      then have "(\<lambda>n. 1 / Suc n :: real) \<longlonglongrightarrow> 0 \<and> 0 < e / 2"
   1.313 +        by (subst LIMSEQ_Suc_iff) (auto intro!: lim_1_over_n)
   1.314 +      then have "\<forall>\<^sub>F n in sequentially. dist (X n) x < e / 2 \<and> 1 / Suc n < e / 2"
   1.315 +        using \<open>X \<longlonglongrightarrow> x\<close> unfolding tendsto_iff order_tendsto_iff[where 'a=real] eventually_conj_iff by blast
   1.316 +      then obtain n where "dist x (X n) < e / 2" "1 / Suc n < e / 2"
   1.317 +        by (auto simp: eventually_sequentially dist_commute)
   1.318 +      have "eventually (\<lambda>y. dist y x < e) F"
   1.319 +        using \<open>eventually (P n) F\<close>
   1.320 +      proof eventually_elim
   1.321 +        fix y assume "P n y"
   1.322 +        then have "dist y (X n) < 1 / Suc n"
   1.323 +          by (intro X P)
   1.324 +        also have "\<dots> < e / 2" by fact
   1.325 +        finally show "dist y x < e"
   1.326 +          by (rule dist_triangle_half_l) fact
   1.327 +      qed }
   1.328 +    then show "F \<le> nhds x"
   1.329 +      unfolding nhds_metric le_INF_iff le_principal by auto
   1.330 +  qed fact
   1.331 +qed
   1.332 +
   1.333 +lemma (in metric_space) totally_bounded_metric:
   1.334 +  "totally_bounded S \<longleftrightarrow> (\<forall>e>0. \<exists>k. finite k \<and> S \<subseteq> (\<Union>x\<in>k. {y. dist x y < e}))"
   1.335 +  unfolding totally_bounded_def eventually_uniformity_metric imp_ex
   1.336 +  apply (subst all_comm)
   1.337 +  apply (intro arg_cong[where f=All] ext)
   1.338 +  apply safe
   1.339 +  subgoal for e
   1.340 +    apply (erule allE[of _ "\<lambda>(x, y). dist x y < e"])
   1.341 +    apply auto
   1.342 +    done
   1.343 +  subgoal for e P k
   1.344 +    apply (intro exI[of _ k])
   1.345 +    apply (force simp: subset_eq)
   1.346 +    done
   1.347 +  done
   1.348  
   1.349  subsubsection \<open>Cauchy Sequences are Convergent\<close>
   1.350  
   1.351 +(* TODO: update to uniform_space *)
   1.352  class complete_space = metric_space +
   1.353    assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
   1.354