src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 56742 678a52e676b6
parent 56544 b60d5d119489
child 57275 0ddb5b755cdc
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Apr 26 13:25:46 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Apr 26 14:53:22 2014 +0200
     1.3 @@ -3291,7 +3291,8 @@
     1.4  
     1.5  lemma filter_from_subbase_not_bot:
     1.6    "\<forall>X \<subseteq> B. finite X \<longrightarrow> Inf X \<noteq> bot \<Longrightarrow> filter_from_subbase B \<noteq> bot"
     1.7 -  unfolding trivial_limit_def eventually_filter_from_subbase by auto
     1.8 +  unfolding trivial_limit_def eventually_filter_from_subbase
     1.9 +    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
    1.10  
    1.11  lemma closure_iff_nhds_not_empty:
    1.12    "x \<in> closure X \<longleftrightarrow> (\<forall>A. \<forall>S\<subseteq>A. open S \<longrightarrow> x \<in> S \<longrightarrow> X \<inter> A \<noteq> {})"