--- a/src/HOL/Analysis/Measure_Space.thy Mon May 22 12:01:05 2023 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy Tue May 23 12:31:23 2023 +0100
@@ -2288,12 +2288,8 @@
subsection\<^marker>\<open>tag unimportant\<close> \<open>Counting space\<close>
lemma strict_monoI_Suc:
- assumes ord [simp]: "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
- unfolding strict_mono_def
-proof safe
- fix n m :: nat assume "n < m" then show "f n < f m"
- by (induct m) (auto simp: less_Suc_eq intro: less_trans ord)
-qed
+ assumes "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
+ by (simp add: assms strict_mono_Suc_iff)
lemma emeasure_count_space:
assumes "X \<subseteq> A" shows "emeasure (count_space A) X = (if finite X then of_nat (card X) else \<infinity>)"