Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Filter.thy
changeset 82603 5648293625a5
parent 82395 918c50e0447e 
--- a/src/HOL/Filter.thy	Sun May 04 21:03:04 2025 +0100
+++ b/src/HOL/Filter.thy	Mon May 05 17:04:07 2025 +0100
@@ -884,6 +884,12 @@
   unfolding at_bot_def
   by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
 
+lemma eventually_at_bot_linorderI:
+  fixes c::"'a::linorder"
+  assumes "\<And>x. x \<le> c \<Longrightarrow> P x"
+  shows "eventually P at_bot"
+  using assms by (auto simp: eventually_at_bot_linorder)     
+
 lemma eventually_filtercomap_at_bot_linorder: 
   "eventually P (filtercomap f at_bot) \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>x. f x \<le> N \<longrightarrow> P x)"
   by (auto simp: eventually_filtercomap eventually_at_bot_linorder)
isabelle