src/HOL/Cardinals/Fun_More.thy

--- a/src/HOL/Cardinals/Fun_More.thy	Sat Jun 25 09:50:40 2022 +0000
+++ b/src/HOL/Cardinals/Fun_More.thy	Mon Jun 27 15:54:18 2022 +0200
@@ -38,12 +38,6 @@
 qed
 
 (* unused *)
-(*1*)lemma bij_betw_ball:
-assumes BIJ: "bij_betw f A B"
-shows "(\<forall>b \<in> B. phi b) = (\<forall>a \<in> A. phi(f a))"
-using assms unfolding bij_betw_def inj_on_def by blast
-
-(* unused *)
 (*1*)lemma bij_betw_diff_singl:
 assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A"
 shows "bij_betw f (A - {a}) (A' - {f a})"