summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | immler |

Fri, 20 May 2016 22:01:39 +0200 | |

changeset 63103 | 2394b0db133f |

parent 63102 | 71059cf60658 |

child 63104 | 9505a883403c |

removed smt proof

src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy | file | annotate | diff | comparison | revisions |

--- 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