isabelle: src/ZF/AC.thy@2e3ca37dfa14 (annotated)

484 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	1	(* Title: ZF/AC.thy
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	2	ID: $Id$
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	4	Copyright 1994 University of Cambridge
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	5
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	6	The Axiom of Choice
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	7
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	8	This definition comes from Halmos (1960), page 59.
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	9	*)
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	10
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	11	AC = ZF + "func" +
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	12	rules
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	13	AC "[\| a: A; !!x. x:A ==> (EX y. y:B(x)) \|] ==> EX z. z : Pi(A,B)"
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	14	end

author	lcp
	Thu, 12 Jan 1995 03:02:34 +0100
changeset 854	2e3ca37dfa14
parent 484	70b789956bd3
child 1478	2b8c2a7547ab
permissions	-rw-r--r--