src/HOL/Topological_Spaces.thy
changeset 61234 a9e6052188fa
parent 61204 3e491e34a62e
child 61245 b77bf45efe21
     1.1 --- a/src/HOL/Topological_Spaces.thy	Tue Sep 22 16:53:59 2015 +0100
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Sep 22 16:55:07 2015 +0100
     1.3 @@ -377,6 +377,10 @@
     1.4  lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
     1.5    unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
     1.6  
     1.7 +lemma at_within_open_NO_MATCH:
     1.8 +  "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
     1.9 +  by (simp only: at_within_open)
    1.10 +
    1.11  lemma at_within_empty [simp]: "at a within {} = bot"
    1.12    unfolding at_within_def by simp
    1.13