src/HOL/Library/FuncSet.thy
changeset 33057 764547b68538
parent 32988 d1d4d7a08a66
child 33271 7be66dee1a5a
     1.1 --- a/src/HOL/Library/FuncSet.thy	Wed Oct 21 17:34:35 2009 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Thu Oct 22 09:27:48 2009 +0200
     1.3 @@ -190,20 +190,20 @@
     1.4        !!x. x\<in>A ==> f x = g x |] ==> f = g"
     1.5  by (force simp add: expand_fun_eq extensional_def)
     1.6  
     1.7 -lemma inv_onto_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_onto A f x) : B -> A"
     1.8 -by (unfold inv_onto_def) (fast intro: someI2)
     1.9 +lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
    1.10 +by (unfold inv_into_def) (fast intro: someI2)
    1.11  
    1.12 -lemma compose_inv_onto_id:
    1.13 -  "bij_betw f A B ==> compose A (\<lambda>y\<in>B. inv_onto A f y) f = (\<lambda>x\<in>A. x)"
    1.14 +lemma compose_inv_into_id:
    1.15 +  "bij_betw f A B ==> compose A (\<lambda>y\<in>B. inv_into A f y) f = (\<lambda>x\<in>A. x)"
    1.16  apply (simp add: bij_betw_def compose_def)
    1.17  apply (rule restrict_ext, auto)
    1.18  done
    1.19  
    1.20 -lemma compose_id_inv_onto:
    1.21 -  "f ` A = B ==> compose B f (\<lambda>y\<in>B. inv_onto A f y) = (\<lambda>x\<in>B. x)"
    1.22 +lemma compose_id_inv_into:
    1.23 +  "f ` A = B ==> compose B f (\<lambda>y\<in>B. inv_into A f y) = (\<lambda>x\<in>B. x)"
    1.24  apply (simp add: compose_def)
    1.25  apply (rule restrict_ext)
    1.26 -apply (simp add: f_inv_onto_f)
    1.27 +apply (simp add: f_inv_into_f)
    1.28  done
    1.29  
    1.30