src/ZF/OrderArith.thy
changeset 61980 6b780867d426
parent 61798 27f3c10b0b50
child 67443 3abf6a722518
     1.1 --- a/src/ZF/OrderArith.thy	Wed Dec 30 17:38:57 2015 +0100
     1.2 +++ b/src/ZF/OrderArith.thy	Wed Dec 30 17:45:18 2015 +0100
     1.3 @@ -557,7 +557,7 @@
     1.4  text\<open>As a special case, we have @{term "bij(Pow(A*B), A -> Pow(B))"}\<close>
     1.5  lemma Pow_Sigma_bij:
     1.6      "(\<lambda>r \<in> Pow(Sigma(A,B)). \<lambda>x \<in> A. r``{x})
     1.7 -     \<in> bij(Pow(Sigma(A,B)), \<Pi> x \<in> A. Pow(B(x)))"
     1.8 +     \<in> bij(Pow(Sigma(A,B)), \<Prod>x \<in> A. Pow(B(x)))"
     1.9  apply (rule_tac d = "%f. \<Union>x \<in> A. \<Union>y \<in> f`x. {<x,y>}" in lam_bijective)
    1.10  apply (blast intro: lam_type)
    1.11  apply (blast dest: apply_type, simp_all)