src/HOL/Topological_Spaces.thy
changeset 61245 b77bf45efe21
parent 61234 a9e6052188fa
child 61306 9dd394c866fc
     1.1 --- a/src/HOL/Topological_Spaces.thy	Thu Sep 24 15:21:12 2015 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Sep 25 16:54:31 2015 +0200
     1.3 @@ -381,6 +381,17 @@
     1.4    "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
     1.5    by (simp only: at_within_open)
     1.6  
     1.7 +lemma at_within_nhd:
     1.8 +  assumes "x \<in> S" "open S" "T \<inter> S - {x} = U \<inter> S - {x}"
     1.9 +  shows "at x within T = at x within U"
    1.10 +  unfolding filter_eq_iff eventually_at_filter
    1.11 +proof (intro allI eventually_subst)
    1.12 +  have "eventually (\<lambda>x. x \<in> S) (nhds x)"
    1.13 +    using \<open>x \<in> S\<close> \<open>open S\<close> by (auto simp: eventually_nhds)
    1.14 +  then show "\<forall>\<^sub>F n in nhds x. (n \<noteq> x \<longrightarrow> n \<in> T \<longrightarrow> P n) = (n \<noteq> x \<longrightarrow> n \<in> U \<longrightarrow> P n)" for P  
    1.15 +    by eventually_elim (insert \<open>T \<inter> S - {x} = U \<inter> S - {x}\<close>, blast)
    1.16 +qed
    1.17 +
    1.18  lemma at_within_empty [simp]: "at a within {} = bot"
    1.19    unfolding at_within_def by simp
    1.20  
    1.21 @@ -1574,7 +1585,7 @@
    1.22    "continuous (at (x::'a::linorder_topology)) f = (continuous (at_left x) f \<and> continuous (at_right x) f)"
    1.23    by (simp add: continuous_within filterlim_at_split)
    1.24  
    1.25 -subsubsection\<open>Open-cover compactness\<close>
    1.26 +subsubsection \<open>Open-cover compactness\<close>
    1.27  
    1.28  context topological_space
    1.29  begin