src/ZF/AC.thy
 changeset 13328 703de709a64b parent 13269 3ba9be497c33 child 14171 0cab06e3bbd0
equal 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")`