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"