summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Tue, 24 Sep 2013 15:03:49 -0700 | |

changeset 53859 | e6cb01686f7b |

parent 53858 | 60b89c05317f |

child 53860 | f2d683432580 |

replace lemma with more general simp rule

src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Topological_Spaces.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 24 23:51:32 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 24 15:03:49 2013 -0700 @@ -1485,9 +1485,6 @@ text{* The expected monotonicity property. *} -lemma Lim_within_empty: "(f ---> l) (at x within {})" - unfolding tendsto_def eventually_at_filter by simp - lemma Lim_Un: assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)" shows "(f ---> l) (at x within (S \<union> T))" @@ -1551,7 +1548,7 @@ shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))" proof (cases "{x<..} \<inter> I = {}") case True - then show ?thesis by (simp add: Lim_within_empty) + then show ?thesis by simp next case False show ?thesis

--- a/src/HOL/Topological_Spaces.thy Tue Sep 24 23:51:32 2013 +0200 +++ b/src/HOL/Topological_Spaces.thy Tue Sep 24 15:03:49 2013 -0700 @@ -490,7 +490,7 @@ unfolding le_filter_def eventually_Sup by simp } { show "Inf {} = (top::'a filter)" by (auto simp: top_filter_def Inf_filter_def Sup_filter_def) - (metis (full_types) Topological_Spaces.top_filter_def always_eventually eventually_top) } + (metis (full_types) top_filter_def always_eventually eventually_top) } { show "Sup {} = (bot::'a filter)" by (auto simp: bot_filter_def Sup_filter_def) } qed @@ -754,6 +754,9 @@ lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a" unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I) +lemma at_within_empty [simp]: "at a within {} = bot" + unfolding at_within_def by simp + lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}" unfolding trivial_limit_def eventually_at_topological by (safe, case_tac "S = {a}", simp, fast, fast)