src/ZF/func.thy
changeset 58860 fee7cfa69c50
parent 46953 2b6e55924af3
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/func.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/ZF/func.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -249,7 +249,7 @@
     1.4  
     1.5  lemma Repfun_function_if:
     1.6       "function(f)
     1.7 -      ==> {f`x. x \<in> C} = (if C \<subseteq> domain(f) then f``C else cons(0,f``C))";
     1.8 +      ==> {f`x. x \<in> C} = (if C \<subseteq> domain(f) then f``C else cons(0,f``C))"
     1.9  apply simp
    1.10  apply (intro conjI impI)
    1.11   apply (blast dest: function_apply_equality intro: function_apply_Pair)
    1.12 @@ -261,7 +261,7 @@
    1.13  (*For this lemma and the next, the right-hand side could equivalently
    1.14    be written \<Union>x\<in>C. {f`x} *)
    1.15  lemma image_function:
    1.16 -     "[| function(f);  C \<subseteq> domain(f) |] ==> f``C = {f`x. x \<in> C}";
    1.17 +     "[| function(f);  C \<subseteq> domain(f) |] ==> f``C = {f`x. x \<in> C}"
    1.18  by (simp add: Repfun_function_if)
    1.19  
    1.20  lemma image_fun: "[| f \<in> Pi(A,B);  C \<subseteq> A |] ==> f``C = {f`x. x \<in> C}"