src/HOL/Cardinals/Fun_More_LFP.thy

 assumes "bij_betw f A A'" "a' \<in> A'"
 shows "f(inv_into A f a') = a'"
 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'"
 shows "bij_betw (inv_into A f) B' B"
 using assms unfolding bij_betw_def