author immler Fri, 20 May 2016 22:01:39 +0200 changeset 63103 2394b0db133f parent 63102 71059cf60658 child 63104 9505a883403c
removed smt proof
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri May 20 07:54:54 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri May 20 22:01:39 2016 +0200
@@ -5976,17 +5976,15 @@
thus "isCont ((indicator A)::'a \<Rightarrow> real) x"
proof
assume int: "x \<in> interior A"
-    hence "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> A" unfolding interior_def by auto
-    then guess U .. note U = this
+    then obtain U where U: "open U" "x \<in> U" "U \<subseteq> A" unfolding interior_def by auto
hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto
hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff)
thus ?thesis using U continuous_on_eq_continuous_at by auto
next
assume ext: "x \<in> interior (-A)"
-    hence "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> -A" unfolding interior_def by auto
-    then guess U .. note U = this
-    hence "\<forall>y\<in>U. indicator A y = (0::real)" unfolding indicator_def by auto
-    hence "continuous_on U (indicator A)" by (smt U continuous_on_topological indicator_def)
+    then obtain U where U: "open U" "x \<in> U" "U \<subseteq> -A" unfolding interior_def by auto
+    then have "continuous_on U (indicator A)"
+      using continuous_on_topological by (auto simp: subset_iff)
thus ?thesis using U continuous_on_eq_continuous_at by auto
qed
qed