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/Vector_Spaces.thy
changeset 82802 547335b41005
parent 82684 a6cfe84d0ddd 
--- a/src/HOL/Vector_Spaces.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Vector_Spaces.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -1388,7 +1388,7 @@
   then have "vs1.span S = vs1.span B"
     using vs1.span_mono[of B S] vs1.span_mono[of S "vs1.span B"] vs1.span_span[of B] by auto
   moreover have "card (f ` B) = card B"
-    using assms card_image[of f B] subset_inj_on[of f "vs1.span S" B] B vs1.span_superset by auto
+    using assms card_image[of f B] inj_on_subset[of f "vs1.span S" B] B vs1.span_superset by auto
   moreover have "(f ` B) \<subseteq> (f ` S)"
     using B by auto
   ultimately show ?thesis
isabelle