--- a/NEWS Tue Jul 01 20:51:26 2025 +0200
+++ b/NEWS Thu Jul 03 13:53:14 2025 +0200
@@ -175,6 +175,7 @@
strict_mono_on_less_eq
- Removed lemmas. Minor INCOMPATIBILITY.
mono_on_greaterD (use mono_invE instead)
+ subset_inj_on (use inj_on_subset)
* Theory "HOL.Relation":
- Changed definition of predicate refl_on to not constrain the domain
--- a/src/HOL/Algebra/Left_Coset.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Algebra/Left_Coset.thy Thu Jul 03 13:53:14 2025 +0200
@@ -95,7 +95,7 @@
lemma (in group) inj_on_f'':
"\<lbrakk>H \<subseteq> carrier G; a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. inv a \<otimes> y) (a <# H)"
- by (meson inj_on_cmult inv_closed l_coset_subset_G subset_inj_on)
+ by (meson inj_on_cmult inv_closed l_coset_subset_G inj_on_subset)
lemma (in group) inj_on_g':
"\<lbrakk>H \<subseteq> carrier G; a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. a \<otimes> y) H"
--- a/src/HOL/Analysis/Abstract_Topology.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy Thu Jul 03 13:53:14 2025 +0200
@@ -2997,7 +2997,7 @@
using S hom homeomorphic_map_interior_of
unfolding homeomorphic_map_def
by (metis (no_types, lifting) closure_of_subset_topspace inj_on_image_mem_iff
- interior_of_subset_closure_of subset_inj_on)
+ interior_of_subset_closure_of inj_on_subset)
qed
lemma homeomorphic_maps_subtopologies:
--- a/src/HOL/Analysis/Abstract_Topology_2.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy Thu Jul 03 13:53:14 2025 +0200
@@ -1384,7 +1384,7 @@
show "subtopology Y (f ` U) homeomorphic_space subtopology X U"
using assms unfolding homeomorphic_eq_everything_map
by (metis Int_absorb1 assms(1) homeomorphic_map_subtopologies homeomorphic_space
- homeomorphic_space_sym subset_image_inj subset_inj_on)
+ homeomorphic_space_sym subset_image_inj inj_on_subset)
qed
lemma homeomorphic_map_path_connectedness_eq:
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Jul 03 13:53:14 2025 +0200
@@ -746,7 +746,7 @@
and "inj f"
shows "rel_interior (f ` S) = f ` (rel_interior S)"
using assms rel_interior_injective_on_span_linear_image[of f S]
- subset_inj_on[of f "UNIV" "span S"]
+ inj_on_subset[of f "UNIV" "span S"]
by auto
--- a/src/HOL/Analysis/Determinants.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Determinants.thy Thu Jul 03 13:53:14 2025 +0200
@@ -56,7 +56,7 @@
by (metis sign_inverse fU p mem_Collect_eq permutation_permutes)
from permutes_inj[OF pU]
have pi: "inj_on p ?U"
- by (blast intro: subset_inj_on)
+ by (blast intro: inj_on_subset)
from permutes_image[OF pU]
have "prod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U =
prod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)"
--- a/src/HOL/Analysis/Embed_Measure.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Embed_Measure.thy Thu Jul 03 13:53:14 2025 +0200
@@ -132,7 +132,7 @@
lemma nn_integral_embed_measure:
"inj f \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
- by(erule nn_integral_embed_measure'[OF subset_inj_on]) simp
+ by(erule nn_integral_embed_measure'[OF inj_on_subset]) simp
lemma emeasure_embed_measure':
assumes "inj_on f (space M)" "A \<in> sets (embed_measure M f)"
@@ -196,7 +196,7 @@
lemma embed_measure_count_space:
"inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
- by(rule embed_measure_count_space')(erule subset_inj_on, simp)
+ by(rule embed_measure_count_space')(erule inj_on_subset, simp)
lemma sets_embed_measure_alt:
"inj f \<Longrightarrow> sets (embed_measure M f) = ((`) f) ` sets M"
--- a/src/HOL/Analysis/Further_Topology.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy Thu Jul 03 13:53:14 2025 +0200
@@ -2264,7 +2264,7 @@
have "DIM(real) \<le> DIM('a)"
by simp
then show ?thesis
- using invariance_of_domain_gen assms continuous_on_subset subset_inj_on by metis
+ using invariance_of_domain_gen assms continuous_on_subset inj_on_subset by metis
qed
lemma continuous_on_inverse_open:
@@ -2308,7 +2308,7 @@
proof -
have "open (f ` interior S)"
using assms
- by (intro invariance_of_domain_gen) (auto simp: subset_inj_on interior_subset continuous_on_subset)
+ by (intro invariance_of_domain_gen) (auto simp: inj_on_subset interior_subset continuous_on_subset)
then show ?thesis
by (simp add: image_mono interiorI interior_subset)
qed
--- a/src/HOL/Analysis/Infinite_Sum.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Infinite_Sum.thy Thu Jul 03 13:53:14 2025 +0200
@@ -1119,7 +1119,7 @@
also have \<open>\<dots> \<longleftrightarrow> (sum (g \<circ> h) \<longlongrightarrow> x) (finite_subsets_at_top A)\<close>
proof (intro tendsto_cong eventually_finite_subsets_at_top_weakI sum.reindex)
show "\<And>X. \<lbrakk>finite X; X \<subseteq> A\<rbrakk> \<Longrightarrow> inj_on h X"
- using assms subset_inj_on by blast
+ using assms inj_on_subset by blast
qed
also have \<open>\<dots> \<longleftrightarrow> ((g \<circ> h) has_sum x) A\<close>
by (simp add: has_sum_def)
--- a/src/HOL/Analysis/Measure_Space.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy Thu Jul 03 13:53:14 2025 +0200
@@ -2365,7 +2365,7 @@
moreover have "inj_on (the_inv_into A f) B"
using X f by (auto simp: bij_betw_def inj_on_the_inv_into)
with X have "inj_on (the_inv_into A f) X"
- by (auto intro: subset_inj_on)
+ by (auto intro: inj_on_subset)
ultimately show "emeasure (distr (count_space A) (count_space B) f) X = emeasure (count_space B) X"
using f unfolding emeasure_distr[OF f' X]
by (subst (1 2) emeasure_count_space) (auto simp: card_image dest: finite_imageD)
--- a/src/HOL/BNF_Wellorder_Constructions.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/BNF_Wellorder_Constructions.thy Thu Jul 03 13:53:14 2025 +0200
@@ -1017,7 +1017,7 @@
unfolding well_order_on_def
using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f]
dir_image_minus_Id[of f r]
- subset_inj_on[of f "Field r" "Field(r - Id)"]
+ inj_on_subset[of f "Field r" "Field(r - Id)"]
mono_Field[of "r - Id" r] by auto
lemma dir_image_bij_betw:
--- a/src/HOL/BNF_Wellorder_Embedding.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/BNF_Wellorder_Embedding.thy Thu Jul 03 13:53:14 2025 +0200
@@ -300,7 +300,7 @@
(* Main proof *)
show "bij_betw f (under r a) (under r' (f a))"
proof(unfold bij_betw_def, auto)
- show "inj_on f (under r a)" by (rule subset_inj_on[OF * under_Field])
+ show "inj_on f (under r a)" by (rule inj_on_subset[OF * under_Field])
next
fix b assume "b \<in> under r a"
thus "f b \<in> under r' (f a)"
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Thu Jul 03 13:53:14 2025 +0200
@@ -1302,7 +1302,7 @@
unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def under_def by auto
moreover from gh(2) *(1,3) have "(\<lambda>x. if x \<in> Field s then h (f x) else undefined) \<in> FinFunc r s"
unfolding FinFunc_def Func_def fin_support_def support_def t.ofilter_def under_def
- by (auto intro: subset_inj_on elim!: finite_imageD[OF finite_subset[rotated]])
+ by (auto intro: inj_on_subset elim!: finite_imageD[OF finite_subset[rotated]])
ultimately show "?thesis" by (rule image_eqI)
qed simp
qed
--- a/src/HOL/Combinatorics/Permutations.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Combinatorics/Permutations.thy Thu Jul 03 13:53:14 2025 +0200
@@ -797,7 +797,7 @@
from \<open>p permutes S\<close> have "inj p"
by (rule permutes_inj)
then have "inj_on p S"
- by (auto intro: subset_inj_on)
+ by (auto intro: inj_on_subset)
then have "F g (p ` S) = F (g \<circ> p) S"
by (rule reindex)
moreover from \<open>p permutes S\<close> have "p ` S = S"
--- a/src/HOL/Complex_Analysis/Riemann_Mapping.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Complex_Analysis/Riemann_Mapping.thy Thu Jul 03 13:53:14 2025 +0200
@@ -295,7 +295,7 @@
have 2: "\<And>z. z \<in> S \<Longrightarrow> (h \<circ> f) z \<noteq> 0"
by (metis \<open>h a = 0\<close> a comp_eq_dest_lhs nf1 kh mem_ball_0 that)
have 3: "inj_on (h \<circ> f) S"
- by (metis (no_types, lifting) F_def \<open>f \<in> F\<close> comp_inj_on inj_on_inverseI injf kh mem_Collect_eq subset_inj_on)
+ by (metis (no_types, lifting) F_def \<open>f \<in> F\<close> comp_inj_on inj_on_inverseI injf kh mem_Collect_eq inj_on_subset)
obtain \<psi> where hol\<psi>: "\<psi> holomorphic_on ((h \<circ> f) ` S)"
and \<psi>2: "\<And>z. z \<in> S \<Longrightarrow> \<psi>(h (f z)) ^ 2 = h(f z)"
proof (rule exE [OF prev [OF 1 2 3]], safe)
--- a/src/HOL/Equiv_Relations.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Equiv_Relations.thy Thu Jul 03 13:53:14 2025 +0200
@@ -408,6 +408,30 @@
qed (use assms in blast)
+subsection \<open>Kernel of a Function\<close>
+
+definition kernel :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a * 'a) set" where
+"kernel f = {(x,y). f x = f y}"
+
+lemma equiv_kernel: "equiv UNIV (kernel f)"
+unfolding kernel_def equiv_def refl_on_def sym_def trans_def by auto
+
+lemma respects_kernel: "f respects (kernel f)"
+by (simp add: congruent_def kernel_def)
+
+lemma inj_on_vimage_image: "inj_on (\<lambda>b. f -` {b}) (f ` A)"
+using inj_on_def by fastforce
+
+lemma kernel_Image: "kernel f `` A = f -` (f ` A)"
+unfolding kernel_def by (auto simp add: rev_image_eqI)
+
+lemma quotient_kernel_eq_image: "A // kernel f = (\<lambda>b. f -` {b}) ` f ` A"
+by(auto simp: quotient_def kernel_Image)
+
+lemma bij_betw_image_quotient_kernel: "bij_betw (\<lambda>b. f -` {b}) (f ` A) (A // kernel f)"
+by (simp add: bij_betw_def inj_on_vimage_image quotient_kernel_eq_image)
+
+
subsection \<open>Projection\<close>
definition proj :: "('b \<times> 'a) set \<Rightarrow> 'b \<Rightarrow> 'a set"
--- 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:
--- a/src/HOL/Fun.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Fun.thy Thu Jul 03 13:53:14 2025 +0200
@@ -229,18 +229,8 @@
unfolding inj_on_def by blast
lemma inj_on_subset:
- assumes "inj_on f A"
- and "B \<subseteq> A"
- shows "inj_on f B"
-proof (rule inj_onI)
- fix a b
- assume "a \<in> B" and "b \<in> B"
- with assms have "a \<in> A" and "b \<in> A"
- by auto
- moreover assume "f a = f b"
- ultimately show "a = b"
- using assms by (auto dest: inj_onD)
-qed
+ "\<lbrakk> inj_on f A; B \<subseteq> A \<rbrakk> \<Longrightarrow> inj_on f B"
+unfolding inj_on_def by blast
lemma comp_inj_on: "inj_on f A \<Longrightarrow> inj_on g (f ` A) \<Longrightarrow> inj_on (g \<circ> f) A"
by (simp add: comp_def inj_on_def)
@@ -261,9 +251,6 @@
lemma inj_on_empty[iff]: "inj_on f {}"
by (simp add: inj_on_def)
-lemma subset_inj_on: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> inj_on f A"
- unfolding inj_on_def by blast
-
lemma inj_on_Un: "inj_on f (A \<union> B) \<longleftrightarrow> inj_on f A \<and> inj_on f B \<and> f ` (A - B) \<inter> f ` (B - A) = {}"
unfolding inj_on_def by (blast intro: sym)
@@ -319,6 +306,9 @@
lemma inj_on_image_Pow: "inj_on f A \<Longrightarrow>inj_on (image f) (Pow A)"
unfolding Pow_def inj_on_def by blast
+lemma inj_on_vimage_image: "inj_on (\<lambda>b. f -` {b}) (f ` A)"
+using inj_on_def by fastforce
+
lemma bij_betw_image_Pow: "bij_betw f A B \<Longrightarrow> bij_betw (image f) (Pow A) (Pow B)"
by (auto simp add: bij_betw_def inj_on_image_Pow image_Pow_surj)
--- a/src/HOL/Homology/Invariance_of_Domain.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Homology/Invariance_of_Domain.thy Thu Jul 03 13:53:14 2025 +0200
@@ -1863,7 +1863,7 @@
shows "embedding_map(subtopology (Euclidean_space m) U) (Euclidean_space n) f"
proof (rule injective_open_imp_embedding_map [OF cmf])
show "open_map (subtopology (Euclidean_space m) U) (Euclidean_space n) f"
- by (meson U \<open>n \<le> m\<close> \<open>inj_on f U\<close> cmf continuous_map_from_subtopology_mono invariance_of_domain_Euclidean_space_gen open_map_def openin_open_subtopology subset_inj_on)
+ by (meson U \<open>n \<le> m\<close> \<open>inj_on f U\<close> cmf continuous_map_from_subtopology_mono invariance_of_domain_Euclidean_space_gen open_map_def openin_open_subtopology inj_on_subset)
show "inj_on f (topspace (subtopology (Euclidean_space m) U))"
using assms openin_subset topspace_subtopology_subset by fastforce
qed
@@ -2412,7 +2412,7 @@
assumes "open T" "continuous_on S f" "inj_on f S" "T \<subseteq> S"
shows "open (f ` T)"
apply (rule invariance_of_domain_gen [OF \<open>open T\<close>])
- using assms apply (auto simp: elim: continuous_on_subset subset_inj_on)
+ using assms apply (auto simp: elim: continuous_on_subset inj_on_subset)
done
lemma continuous_on_inverse_open:
@@ -2460,7 +2460,7 @@
by (simp add: image_mono interior_subset)
show "open (f ` interior S)"
using assms
- by (auto simp: subset_inj_on interior_subset continuous_on_subset invariance_of_domain_gen)
+ by (auto simp: inj_on_subset interior_subset continuous_on_subset invariance_of_domain_gen)
qed
lemma homeomorphic_interiors_same_dimension:
--- a/src/HOL/Inductive.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Inductive.thy Thu Jul 03 13:53:14 2025 +0200
@@ -467,7 +467,7 @@
show "inj_on ?h A"
proof -
from inj1 X_sub have on_X: "inj_on f X"
- by (rule subset_inj_on)
+ by (rule inj_on_subset)
have on_X_compl: "inj_on g' (A - X)"
unfolding g'_def X_compl
--- a/src/HOL/Library/Countable_Set.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Library/Countable_Set.thy Thu Jul 03 13:53:14 2025 +0200
@@ -47,7 +47,7 @@
by (blast intro: countableI_bij1 countableI_bij2)
lemma countable_subset: "A \<subseteq> B \<Longrightarrow> countable B \<Longrightarrow> countable A"
- by (auto simp: countable_def intro: subset_inj_on)
+ by (auto simp: countable_def intro: inj_on_subset)
lemma countableI_type[intro, simp]: "countable (A:: 'a :: countable set)"
using countableI[of to_nat A] by auto
@@ -211,7 +211,7 @@
moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A"
by (auto intro: inj_on_inv_into inv_into_into)
ultimately show ?thesis
- by (blast dest: comp_inj_on subset_inj_on intro: countableI)
+ by (blast dest: comp_inj_on inj_on_subset intro: countableI)
qed
lemma countable_image_inj_on: "countable (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> countable A"
--- a/src/HOL/Library/Groups_Big_Fun.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy Thu Jul 03 13:53:14 2025 +0200
@@ -74,7 +74,7 @@
proof -
from assms have unfold: "h = g \<circ> l" by simp
from \<open>bij l\<close> have "inj l" by (rule bij_is_inj)
- then have "inj_on l {a. h a \<noteq> \<^bold>1}" by (rule subset_inj_on) simp
+ then have "inj_on l {a. h a \<noteq> \<^bold>1}" by (rule inj_on_subset) simp
moreover from \<open>bij l\<close> have "{a. g a \<noteq> \<^bold>1} = l ` {a. h a \<noteq> \<^bold>1}"
by (auto simp add: image_Collect unfold elim: bij_pointE)
moreover have "\<And>x. x \<in> {a. h a \<noteq> \<^bold>1} \<Longrightarrow> g (l x) = h x"
--- a/src/HOL/Library/Ramsey.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Library/Ramsey.thy Thu Jul 03 13:53:14 2025 +0200
@@ -194,7 +194,7 @@
then show "A Int (f -` X) \<in> [A]\<^bsup>k\<^esup>"
using assms
unfolding nsets_def mem_Collect_eq
- by (metis card_image finite_image_iff inf_le1 subset_inj_on)
+ by (metis card_image finite_image_iff inf_le1 inj_on_subset)
qed
lemma nsets_image_funcset:
@@ -1016,7 +1016,7 @@
from pg show "?gy ` {n. ?gt n = s'} \<subseteq> YY"
by (auto simp add: Let_def split_beta)
from infeqs' show "infinite (?gy ` {n. ?gt n = s'})"
- by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
+ by (blast intro: inj_gy [THEN inj_on_subset] dest: finite_imageD)
show "s' < s" by (rule less')
show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} \<and> finite X \<and> card X = Suc r \<longrightarrow> f X = s'"
proof -
--- a/src/HOL/List.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/List.thy Thu Jul 03 13:53:14 2025 +0200
@@ -4701,7 +4701,7 @@
lemma map_removeAll_inj: "inj f \<Longrightarrow>
map f (removeAll x xs) = removeAll (f x) (map f xs)"
-by (rule map_removeAll_inj_on, erule subset_inj_on, rule subset_UNIV)
+by (rule map_removeAll_inj_on, erule inj_on_subset, rule subset_UNIV)
lemma length_removeAll_less_eq [simp]:
"length (removeAll x xs) \<le> length xs"
@@ -6653,7 +6653,7 @@
case True
with assms inj_on show ?thesis
using distinct_card[symmetric, OF distinct_sorted_key_list_of_set]
- by (auto simp: subset_inj_on intro!: card_image)
+ by (auto simp: inj_on_subset intro!: card_image)
qed auto
lemmas sorted_key_list_of_set =
@@ -6672,7 +6672,7 @@
lemma strict_sorted_key_list_of_set [simp]:
"A \<subseteq> S \<Longrightarrow> sorted_wrt (\<prec>) (map f (sorted_key_list_of_set f A))"
- by (cases "finite A") (auto simp: strict_sorted_iff subset_inj_on[OF inj_on])
+ by (cases "finite A") (auto simp: strict_sorted_iff inj_on_subset[OF inj_on])
lemma finite_set_strict_sorted:
assumes "A \<subseteq> S" and "finite A"
--- a/src/HOL/Modules.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Modules.thy Thu Jul 03 13:53:14 2025 +0200
@@ -872,7 +872,7 @@
lemma independent_inj_image:
"m1.independent S \<Longrightarrow> inj f \<Longrightarrow> m2.independent (f ` S)"
- using independent_inj_on_image[of S] by (auto simp: subset_inj_on)
+ using independent_inj_on_image[of S] by (auto simp: inj_on_subset)
end
--- a/src/HOL/Probability/Probability_Mass_Function.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Thu Jul 03 13:53:14 2025 +0200
@@ -688,7 +688,7 @@
lemma pmf_map_inj': "inj f \<Longrightarrow> pmf (map_pmf f M) (f x) = pmf M x"
apply(cases "x \<in> set_pmf M")
- apply(simp add: pmf_map_inj[OF subset_inj_on])
+ apply(simp add: pmf_map_inj[OF inj_on_subset])
apply(simp add: pmf_eq_0_set_pmf[symmetric])
apply(auto simp add: pmf_eq_0_set_pmf dest: injD)
done
--- a/src/HOL/Probability/Projective_Family.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Probability/Projective_Family.thy Thu Jul 03 13:53:14 2025 +0200
@@ -618,7 +618,7 @@
have inj_t: "inj_on t (\<Union>i. J i)"
using count by (auto simp: t_def)
then have inj_t_J: "inj_on t (J i)" for i
- by (rule subset_inj_on) auto
+ by (rule inj_on_subset) auto
interpret IT: Ionescu_Tulcea "\<lambda>i \<omega>. M (f i)" "\<lambda>i. M (f i)"
by standard auto
interpret Mf: product_prob_space "\<lambda>x. M (f x)" UNIV
--- a/src/HOL/Probability/Projective_Limit.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Probability/Projective_Limit.thy Thu Jul 03 13:53:14 2025 +0200
@@ -139,7 +139,7 @@
by unfold_locales (auto simp: Utn_def intro: from_nat_into_to_nat_on[OF countable_UN_J])
have inj_on_Utn: "inj_on Utn (\<Union>n. J n)"
unfolding Utn_def using countable_UN_J by (rule inj_on_to_nat_on)
- hence inj_on_Utn_J: "\<And>n. inj_on Utn (J n)" by (rule subset_inj_on) auto
+ hence inj_on_Utn_J: "\<And>n. inj_on Utn (J n)" by (rule inj_on_subset) auto
define P' where "P' n = mapmeasure n (P (J n)) (\<lambda>_. borel)" for n
interpret P': prob_space "P' n" for n
unfolding P'_def mapmeasure_def using J
--- a/src/HOL/Series.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Series.thy Thu Jul 03 13:53:14 2025 +0200
@@ -1164,7 +1164,7 @@
and suminf_reindex: "(\<And>x. x \<notin> range g \<Longrightarrow> f x = 0) \<Longrightarrow> suminf (f \<circ> g) = suminf f"
proof -
from \<open>inj g\<close> have [simp]: "\<And>A. inj_on g A"
- by (rule subset_inj_on) simp
+ by (rule inj_on_subset) simp
have smaller: "\<forall>n. (\<Sum>i<n. (f \<circ> g) i) \<le> suminf f"
proof
--- 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
--- a/src/HOL/ZF/Zet.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/ZF/Zet.thy Thu Jul 03 13:53:14 2025 +0200
@@ -54,7 +54,7 @@
have "inj_on (inv_into A g) (g ` A)" by (simp add: inj_on_inv_into)
then have injw: "inj_on ?w (g ` A)"
apply (rule comp_inj_on)
- apply (rule subset_inj_on[where B=A])
+ apply (rule inj_on_subset[where A=A])
apply (auto simp add: subset injf)
done
show ?thesis