--- a/src/HOL/Library/Infinite_Set.thy Wed Jun 22 14:52:27 2022 +0200
+++ b/src/HOL/Library/Infinite_Set.thy Thu Jun 23 19:29:22 2022 +0200
@@ -467,7 +467,7 @@
lemma finite_enumerate:
assumes fS: "finite S"
- shows "\<exists>r::nat\<Rightarrow>nat. strict_mono_on r {..<card S} \<and> (\<forall>n<card S. r n \<in> S)"
+ shows "\<exists>r::nat\<Rightarrow>nat. strict_mono_on {..<card S} r \<and> (\<forall>n<card S. r n \<in> S)"
unfolding strict_mono_def
using finite_enumerate_in_set[OF fS] finite_enumerate_mono[of _ _ S] fS
by (metis lessThan_iff strict_mono_on_def)
@@ -603,11 +603,11 @@
lemma ex_bij_betw_strict_mono_card:
fixes M :: "'a::wellorder set"
assumes "finite M"
- obtains h where "bij_betw h {..<card M} M" and "strict_mono_on h {..<card M}"
+ obtains h where "bij_betw h {..<card M} M" and "strict_mono_on {..<card M} h"
proof
show "bij_betw (enumerate M) {..<card M} M"
by (simp add: assms finite_bij_enumerate)
- show "strict_mono_on (enumerate M) {..<card M}"
+ show "strict_mono_on {..<card M} (enumerate M)"
by (simp add: assms finite_enumerate_mono strict_mono_on_def)
qed