equal
deleted
inserted
replaced
754 lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a" |
754 lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a" |
755 unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I) |
755 unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I) |
756 |
756 |
757 lemma at_within_empty [simp]: "at a within {} = bot" |
757 lemma at_within_empty [simp]: "at a within {} = bot" |
758 unfolding at_within_def by simp |
758 unfolding at_within_def by simp |
|
759 |
|
760 lemma at_within_union: "at x within (S \<union> T) = sup (at x within S) (at x within T)" |
|
761 unfolding filter_eq_iff eventually_sup eventually_at_filter |
|
762 by (auto elim!: eventually_rev_mp) |
759 |
763 |
760 lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}" |
764 lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}" |
761 unfolding trivial_limit_def eventually_at_topological |
765 unfolding trivial_limit_def eventually_at_topological |
762 by (safe, case_tac "S = {a}", simp, fast, fast) |
766 by (safe, case_tac "S = {a}", simp, fast, fast) |
763 |
767 |