diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-29 09:01:19 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-29 09:01:19 +0000 |
commit | af841b20c9aed32226a6e977d1ff87435783b574 (patch) | |
tree | a90af104fd0e295525b0e94059bae7d2869c50f3 /theories/Logic/RelationalChoice.v | |
parent | 0d80bdb68cdb5b753a3e56a8ed1029b50cd2cbd8 (diff) |
Choix sous sa forme relationnelle
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4741 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/RelationalChoice.v')
-rw-r--r-- | theories/Logic/RelationalChoice.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v new file mode 100644 index 000000000..5addb4d24 --- /dev/null +++ b/theories/Logic/RelationalChoice.v @@ -0,0 +1,17 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +(* This file axiomatizes the relational form of the axiom of choice *) + +Axiom relational_choice : + (A:Type;B:Type;R: A->B->Prop) + ((x:A)(EX y:B|(R x y))) + -> (EXT R':A->B->Prop | + ((x:A)(EX y:B|(R x y)/\(R' x y)/\ ((y':B) (R' x y') -> y=y')))). |