src/HOL/Cardinals/Fun_More_LFP.thy

--- a/src/HOL/Cardinals/Fun_More_LFP.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Fun_More_LFP.thy	Mon Nov 18 18:04:45 2013 +0100
@@ -210,19 +210,6 @@
 using assms unfolding bij_betw_def using f_inv_into_f by force
 
 
-(*1*)lemma bij_betw_inv_into_LEFT:
-assumes BIJ: "bij_betw f A A'" and SUB: "B \<le> A"
-shows "(inv_into A f)`(f ` B) = B"
-using assms unfolding bij_betw_def using inv_into_image_cancel by force
-
-
-(*1*)lemma bij_betw_inv_into_LEFT_RIGHT:
-assumes BIJ: "bij_betw f A A'" and SUB: "B \<le> A" and
-        IM: "f ` B = B'"
-shows "(inv_into A f) ` B' = B"
-using assms bij_betw_inv_into_LEFT[of f A A' B] by fast
-
-
 (*1*)lemma bij_betw_inv_into_subset:
 assumes BIJ: "bij_betw f A A'" and
         SUB: "B \<le> A" and IM: "f ` B = B'"