diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-04 17:59:53 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-04 17:59:53 +0000 |
| commit | 03c392f24a204be29093166b9c42fa5c485e627c (patch) | |
| tree | ab7a5404f12e452ded8742b7a026d6cfad92b374 /theories/Logic/RelationalChoice.v | |
| parent | f288a7f38b1ad0b6e9ab6d01ea6cded80cc867c6 (diff) | |
Ajout exists! et restructuration/extension des fichiers sur la
description et le choix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8892 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/RelationalChoice.v')
| -rw-r--r-- | theories/Logic/RelationalChoice.v | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v index feb11b827..9ad6b7220 100644 --- a/theories/Logic/RelationalChoice.v +++ b/theories/Logic/RelationalChoice.v @@ -10,11 +10,8 @@ (** This file axiomatizes the relational form of the axiom of choice *) -Axiom - relational_choice : - forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B, R x y) -> - exists R' : A -> B -> Prop, - (forall x:A, - exists y : B, - R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). +Axiom relational_choice : + forall (A B : Type) (R : A->B->Prop), + (forall x : A, exists y : B, R x y) -> + exists R' : A->B->Prop, + subrelation R' R /\ forall x : A, exists! y : B, R' x y. |