# HG changeset patch
# User blanchet
# Date 1384794285 -3600
# Node ID 215d41768e515399e1d600e519822ddccb064c88
# Parent  f001ef2637d31c55eafba837eb8127c5be84b7a8
moved theorems out of LFP

diff -r f001ef2637d3 -r 215d41768e51 src/HOL/Cardinals/Fun_More.thy
--- a/src/HOL/Cardinals/Fun_More.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Fun_More.thy	Mon Nov 18 18:04:45 2013 +0100
@@ -132,6 +132,18 @@
 subsection {* Properties involving Hilbert choice *}
 
 
+(*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
+
+
 subsection {* Other facts *}
 
 (*3*)lemma atLeastLessThan_injective:
diff -r f001ef2637d3 -r 215d41768e51 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'"