--- a/src/HOL/Fun.thy Mon Feb 12 09:30:22 2024 +0000
+++ b/src/HOL/Fun.thy Tue Feb 13 17:18:50 2024 +0000
@@ -395,6 +395,11 @@
lemma bij_betw_comp_iff: "bij_betw f A A' \<Longrightarrow> bij_betw f' A' A'' \<longleftrightarrow> bij_betw (f' \<circ> f) A A''"
by (auto simp add: bij_betw_def inj_on_def)
+lemma bij_betw_Collect:
+ assumes "bij_betw f A B" "\<And>x. x \<in> A \<Longrightarrow> Q (f x) \<longleftrightarrow> P x"
+ shows "bij_betw f {x\<in>A. P x} {y\<in>B. Q y}"
+ using assms by (auto simp add: bij_betw_def inj_on_def)
+
lemma bij_betw_comp_iff2:
assumes bij: "bij_betw f' A' A''"
and img: "f ` A \<le> A'"