equal
deleted
inserted
replaced
488 unfolding le_filter_def eventually_Sup by simp } |
488 unfolding le_filter_def eventually_Sup by simp } |
489 { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'" |
489 { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'" |
490 unfolding le_filter_def eventually_Sup by simp } |
490 unfolding le_filter_def eventually_Sup by simp } |
491 { show "Inf {} = (top::'a filter)" |
491 { show "Inf {} = (top::'a filter)" |
492 by (auto simp: top_filter_def Inf_filter_def Sup_filter_def) |
492 by (auto simp: top_filter_def Inf_filter_def Sup_filter_def) |
493 (metis (full_types) Topological_Spaces.top_filter_def always_eventually eventually_top) } |
493 (metis (full_types) top_filter_def always_eventually eventually_top) } |
494 { show "Sup {} = (bot::'a filter)" |
494 { show "Sup {} = (bot::'a filter)" |
495 by (auto simp: bot_filter_def Sup_filter_def) } |
495 by (auto simp: bot_filter_def Sup_filter_def) } |
496 qed |
496 qed |
497 |
497 |
498 end |
498 end |
751 "eventually P (at a within s) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x))" |
751 "eventually P (at a within s) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x))" |
752 unfolding eventually_nhds eventually_at_filter by simp |
752 unfolding eventually_nhds eventually_at_filter by simp |
753 |
753 |
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 |
|
757 lemma at_within_empty [simp]: "at a within {} = bot" |
|
758 unfolding at_within_def by simp |
756 |
759 |
757 lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}" |
760 lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}" |
758 unfolding trivial_limit_def eventually_at_topological |
761 unfolding trivial_limit_def eventually_at_topological |
759 by (safe, case_tac "S = {a}", simp, fast, fast) |
762 by (safe, case_tac "S = {a}", simp, fast, fast) |
760 |
763 |