# HG changeset patch
# User huffman
# Date 1243994390 25200
# Node ID f7c7bf82b12f6f38da4c1dd478ebdd1ff0a4eb34
# Parent  8cbcab09ce2acb6a1577839a049f4fcd2b85eab9
generalize lemma closed_cball

diff -r 8cbcab09ce2a -r f7c7bf82b12f src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Jun 02 18:46:32 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Jun 02 18:59:50 2009 -0700
@@ -1742,19 +1742,14 @@
 
 text{* More properties of closed balls. *}
 
-lemma closed_cball:
-  fixes x :: "'a::real_normed_vector" (* FIXME: generalize to metric_space *)
-  shows "closed (cball x e)"
-proof-
-  { fix xa::"nat\<Rightarrow>'a" and l assume as: "\<forall>n. dist x (xa n) \<le> e" "(xa ---> l) sequentially"
-    from as(2) have "((\<lambda>n. x - xa n) ---> x - l) sequentially" using Lim_sub[of "\<lambda>n. x" x sequentially xa l] Lim_const[of x sequentially] by auto
-    moreover from as(1) have "eventually (\<lambda>n. norm (x - xa n) \<le> e) sequentially" unfolding eventually_sequentially dist_norm by auto
-    ultimately have "dist x l \<le> e"
-      unfolding dist_norm
-      using Lim_norm_ubound[of sequentially _ "x - l" e] using trivial_limit_sequentially by auto
-  }
-  thus ?thesis unfolding closed_sequential_limits by auto
-qed
+lemma closed_cball: "closed (cball x e)"
+unfolding cball_def closed_def Compl_eq_Diff_UNIV [symmetric]
+unfolding Collect_neg_eq [symmetric] not_le
+apply (clarsimp simp add: open_def, rename_tac y)
+apply (rule_tac x="dist x y - e" in exI, clarsimp)
+apply (cut_tac x=x and y=x' and z=y in dist_triangle)
+apply simp
+done
 
 lemma open_contains_cball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0.  cball x e \<subseteq> S)"
 proof-