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/Finite_Set.thy
changeset 82802 547335b41005
parent 82664 e9f3b94eb6a0 
--- a/src/HOL/Finite_Set.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -2380,7 +2380,7 @@
 
 lemma card_vimage_inj: "inj f \<Longrightarrow> A \<subseteq> range f \<Longrightarrow> card (f -` A) = card A"
   by (auto 4 3 simp: subset_image_iff inj_vimage_image_eq
-      intro: card_image[symmetric, OF subset_inj_on])
+      intro: card_image[symmetric, OF inj_on_subset])
 
 lemma card_inverse[simp]: "card (R\<inverse>) = card R"
 proof -
@@ -3053,7 +3053,7 @@
 lemma inj_on_image_Fpow:
   assumes "inj_on f A"
   shows "inj_on (image f) (Fpow A)"
-  using assms Fpow_subset_Pow[of A] subset_inj_on[of "image f" "Pow A"]
+  using assms Fpow_subset_Pow[of A] inj_on_subset[of "image f" "Pow A"]
     inj_on_image_Pow by blast
 
 lemma image_Fpow_mono:
isabelle