src/HOL/Topological_Spaces.thy
changeset 60182 e1ea5a6379c9
parent 60172 423273355b55
child 60585 48fdff264eb2
     1.1 --- a/src/HOL/Topological_Spaces.thy	Wed May 06 15:04:38 2015 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Thu May 07 15:34:28 2015 +0200
     1.3 @@ -356,6 +356,10 @@
     1.4  lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
     1.5    unfolding trivial_limit_def eventually_nhds by simp
     1.6  
     1.7 +lemma (in t1_space) t1_space_nhds:
     1.8 +  "x \<noteq> y \<Longrightarrow> (\<forall>\<^sub>F x in nhds x. x \<noteq> y)"
     1.9 +  by (drule t1_space) (auto simp: eventually_nhds)
    1.10 +
    1.11  lemma at_within_eq: "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
    1.12    unfolding nhds_def at_within_def by (subst INF_inf_const2[symmetric]) (auto simp add: Diff_Int_distrib)
    1.13