src/ZF/AC.thy
changeset 13328 703de709a64b
parent 13269 3ba9be497c33
child 14171 0cab06e3bbd0
equal deleted inserted replaced
13327:be7105a066d3 13328:703de709a64b
     1 (*  Title:      ZF/AC.thy
     1 (*  Title:      ZF/AC.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     4     Copyright   1994  University of Cambridge
     5 
     5 
     6 The Axiom of Choice
     6 *)
     7 
     7 
     8 This definition comes from Halmos (1960), page 59.
     8 header{*The Axiom of Choice*}
     9 *)
       
    10 
     9 
    11 theory AC = Main:
    10 theory AC = Main:
    12 
    11 
       
    12 text{*This definition comes from Halmos (1960), page 59.*}
    13 axioms AC: "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
    13 axioms AC: "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
    14 
    14 
    15 (*The same as AC, but no premise a \<in> A*)
    15 (*The same as AC, but no premise a \<in> A*)
    16 lemma AC_Pi: "[| !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)"
    16 lemma AC_Pi: "[| !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)"
    17 apply (case_tac "A=0")
    17 apply (case_tac "A=0")