From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- theories/Logic/SetoidChoice.v | 62 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 theories/Logic/SetoidChoice.v (limited to 'theories/Logic/SetoidChoice.v') diff --git a/theories/Logic/SetoidChoice.v b/theories/Logic/SetoidChoice.v new file mode 100644 index 00000000..21bf7335 --- /dev/null +++ b/theories/Logic/SetoidChoice.v @@ -0,0 +1,62 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* A -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + (forall x x' y, R x x' -> T x y -> T x' y) -> + (forall x, exists y, T x y) -> + exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). +Proof. + apply setoid_functional_choice_first_characterization. split; [|split]. + - exact choice. + - exact extensional_function_representative. + - exact classic. +Qed. + +Theorem representative_choice : + forall A (R:A->A->Prop), (Equivalence R) -> + exists f : A->A, forall x : A, R x (f x) /\ forall x', R x x' -> f x = f x'. +Proof. + apply setoid_fun_choice_imp_repr_fun_choice. + exact setoid_choice. +Qed. -- cgit v1.2.3