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/Analysis/Bochner_Integration.thy
changeset 80175 200107cdd3ac
parent 79599 2c18ac57e92e 
--- a/src/HOL/Analysis/Bochner_Integration.thy	Sun May 05 15:31:08 2024 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Mon May 06 14:39:33 2024 +0100
@@ -2795,7 +2795,7 @@
       have "eventually (\<lambda>n. x \<le> X n) sequentially"
         unfolding filterlim_at_top_ge[where c=x] by auto
       then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) \<longlonglongrightarrow> f x"
-        by (intro tendsto_eventually) (auto split: split_indicator elim!: eventually_mono)
+        by (intro tendsto_eventually) (auto simp: frequently_def split: split_indicator)
     qed
     fix n show "AE x in M. norm (indicator {..X n} x *\<^sub>R f x) \<le> norm (f x)"
       by (auto split: split_indicator)
isabelle