src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 58184 db1381d811ab parent 57865 dcfb33c26f50 child 58729 e8ecc79aee43 child 58757 7f4924f23158
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 04 11:53:39 2014 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 04 14:02:37 2014 +0200
1.3 @@ -3734,64 +3734,39 @@
1.4    shows "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
1.5    by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
1.6
1.7 -subsubsection{* Total boundedness *}
1.8 +subsubsection{* Totally bounded *}
1.9
1.10  lemma cauchy_def: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
1.11    unfolding Cauchy_def by metis
1.12
1.13 -fun helper_1 :: "('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a"
1.14 -where
1.15 -  "helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))"
1.16 -declare helper_1.simps[simp del]
1.17 -
1.18  lemma seq_compact_imp_totally_bounded:
1.19    assumes "seq_compact s"
1.20 -  shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))"
1.21 -proof (rule, rule, rule ccontr)
1.22 -  fix e::real
1.23 -  assume "e > 0"
1.24 -  assume assm: "\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` k))"
1.25 -  def x \<equiv> "helper_1 s e"
1.26 -  {
1.27 -    fix n
1.28 -    have "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
1.29 -    proof (induct n rule: nat_less_induct)
1.30 -      fix n
1.31 -      def Q \<equiv> "(\<lambda>y. y \<in> s \<and> (\<forall>m<n. \<not> dist (x m) y < e))"
1.32 -      assume as: "\<forall>m<n. x m \<in> s \<and> (\<forall>ma<m. \<not> dist (x ma) (x m) < e)"
1.33 -      have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)"
1.34 -        using assm
1.35 -        apply simp
1.36 -        apply (erule_tac x="x ` {0 ..< n}" in allE)
1.37 -        using as
1.38 -        apply auto
1.39 -        done
1.40 +  shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)"
1.41 +proof -
1.42 +  { fix e::real assume "e > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> s \<Longrightarrow> \<not> s \<subseteq> (\<Union>x\<in>k. ball x e)"
1.43 +    let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"
1.44 +    have "\<exists>x. \<forall>n::nat. ?Q x n (x n)"
1.45 +    proof (rule dependent_wellorder_choice)
1.46 +      fix n x assume "\<And>y. y < n \<Longrightarrow> ?Q x y (x y)"
1.47 +      then have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)"
1.48 +        using *[of "x ` {0 ..< n}"] by (auto simp: subset_eq)
1.49        then obtain z where z:"z\<in>s" "z \<notin> (\<Union>x\<in>x ` {0..<n}. ball x e)"
1.50          unfolding subset_eq by auto
1.51 -      have "Q (x n)"
1.52 -        unfolding x_def and helper_1.simps[of s e n]
1.53 -        apply (rule someI2[where a=z])
1.54 -        unfolding x_def[symmetric] and Q_def
1.55 -        using z
1.56 -        apply auto
1.57 -        done
1.58 -      then show "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
1.59 -        unfolding Q_def by auto
1.60 -    qed
1.61 -  }
1.62 -  then have "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)"
1.63 -    by blast+
1.64 -  then obtain l r where "l\<in>s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially"
1.65 -    using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto
1.66 -  from this(3) have "Cauchy (x \<circ> r)"
1.67 -    using LIMSEQ_imp_Cauchy by auto
1.68 -  then obtain N::nat where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e"
1.69 -    unfolding cauchy_def using `e>0` by auto
1.70 -  show False
1.71 -    using N[THEN spec[where x=N], THEN spec[where x="N+1"]]
1.72 -    using r[unfolded subseq_def, THEN spec[where x=N], THEN spec[where x="N+1"]]
1.73 -    using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]]
1.74 -    by auto
1.75 +      show "\<exists>r. ?Q x n r"
1.76 +        using z by auto
1.77 +    qed simp
1.78 +    then obtain x where "\<forall>n::nat. x n \<in> s" and x:"\<And>n m. m < n \<Longrightarrow> \<not> (dist (x m) (x n) < e)"
1.79 +      by blast
1.80 +    then obtain l r where "l \<in> s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially"
1.81 +      using assms by (metis seq_compact_def)
1.82 +    from this(3) have "Cauchy (x \<circ> r)"
1.83 +      using LIMSEQ_imp_Cauchy by auto
1.84 +    then obtain N::nat where "\<And>m n. N \<le> m \<Longrightarrow> N \<le> n \<Longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e"
1.85 +      unfolding cauchy_def using `e > 0` by blast
1.86 +    then have False
1.87 +      using x[of "r N" "r (N+1)"] r by (auto simp: subseq_def) }
1.88 +  then show ?thesis
1.89 +    by metis
1.90  qed
1.91
1.92  subsubsection{* Heine-Borel theorem *}
1.93 @@ -3802,7 +3777,7 @@
1.94    shows "compact s"
1.95  proof -
1.96    from seq_compact_imp_totally_bounded[OF `seq_compact s`]
1.97 -  obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` f e)"
1.98 +  obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>f e. ball x e)"
1.99      unfolding choice_iff' ..
1.100    def K \<equiv> "(\<lambda>(x, r). ball x r) ` ((\<Union>e \<in> \<rat> \<inter> {0 <..}. f e) \<times> \<rat>)"
1.101    have "countably_compact s"
1.102 @@ -4137,7 +4112,7 @@
1.103  qed
1.104
1.105  lemma compact_eq_totally_bounded:
1.106 -  "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
1.107 +  "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
1.108      (is "_ \<longleftrightarrow> ?rhs")
1.109  proof
1.110    assume assms: "?rhs"
```