# HG changeset patch
# User desharna
# Date 1665664035 -7200
# Node ID 457f1cba78fbf4eb36321059452843a84bf89ff9
# Parent  cee0b9fccf6f075e3083f4cb4df30c1e128ce697
renamed lemma inj_on_strict_subset to image_strict_mono for symmetry with image_mono and to distinguish from inj_on_subset

diff -r cee0b9fccf6f -r 457f1cba78fb NEWS
--- a/NEWS	Thu Oct 13 10:44:27 2022 +0200
+++ b/NEWS	Thu Oct 13 14:27:15 2022 +0200
@@ -9,6 +9,10 @@
 
 *** HOL ***
 
+* Theory "HOL.Fun":
+  - Renamed lemma inj_on_strict_subset to image_strict_mono.
+    Minor INCOMPATIBILITY.
+
 * Theory "HOL.Relation":
   - Strengthened lemma total_on_singleton. Minor INCOMPATIBILITY.
   - Added lemmas.
diff -r cee0b9fccf6f -r 457f1cba78fb src/HOL/BNF_Wellorder_Constructions.thy
--- a/src/HOL/BNF_Wellorder_Constructions.thy	Thu Oct 13 10:44:27 2022 +0200
+++ b/src/HOL/BNF_Wellorder_Constructions.thy	Thu Oct 13 14:27:15 2022 +0200
@@ -708,7 +708,7 @@
   moreover have "inj_on f23 ?A2"
   using EMB23 0 by (simp add: wo_rel_def embed_inj_on)
   ultimately
-  have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: inj_on_strict_subset)
+  have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: image_strict_mono)
   moreover
   {have "embed r1 r3 (f23 \<circ> f12)"
    using 1 EMB23 0 by (auto simp add: comp_embed)
diff -r cee0b9fccf6f -r 457f1cba78fb src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Oct 13 10:44:27 2022 +0200
+++ b/src/HOL/Fun.thy	Thu Oct 13 14:27:15 2022 +0200
@@ -178,7 +178,7 @@
 lemma inj_on_cong: "(\<And>a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> inj_on f A \<longleftrightarrow> inj_on g A"
   by (auto simp: inj_on_def)
 
-lemma inj_on_strict_subset: "inj_on f B \<Longrightarrow> A \<subset> B \<Longrightarrow> f ` A \<subset> f ` B"
+lemma image_strict_mono: "inj_on f B \<Longrightarrow> A \<subset> B \<Longrightarrow> f ` A \<subset> f ` B"
   unfolding inj_on_def by blast
 
 lemma inj_compose: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
diff -r cee0b9fccf6f -r 457f1cba78fb src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Thu Oct 13 10:44:27 2022 +0200
+++ b/src/HOL/Library/FSet.thy	Thu Oct 13 14:27:15 2022 +0200
@@ -559,7 +559,7 @@
 lemma fimage_strict_mono:
   assumes "inj_on f (fset B)" and "A |\<subset>| B"
   shows "f |`| A |\<subset>| f |`| B"
-  \<comment> \<open>TODO: Configure transfer framework to lift @{thm Fun.inj_on_strict_subset}.\<close>
+  \<comment> \<open>TODO: Configure transfer framework to lift @{thm Fun.image_strict_mono}.\<close>
 proof (rule pfsubsetI)
   from \<open>A |\<subset>| B\<close> have "A |\<subseteq>| B"
     by (rule pfsubset_imp_fsubset)