From 639af2938c15202b12f709eb84790d0b5c627a9f Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 21 Jun 2000 01:12:20 +0000
Subject: theories/Relations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@510 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Relations/Relations.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100755 theories/Relations/Relations.v

(limited to 'theories/Relations/Relations.v')

diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
new file mode 100755
index 0000000000..f11537a6e8
--- /dev/null
+++ b/theories/Relations/Relations.v
@@ -0,0 +1,21 @@
+
+(* $Id$ *)
+
+Require Export Relation_Definitions.
+Require Export Relation_Operators.
+Require Export Operators_Properties.
+
+Lemma inverse_image_of_equivalence : (A,B:Set)(f:A->B)
+  (r:(relation B))(equivalence B r)->(equivalence A [x,y:A](r (f x) (f y))).
+Intros; Split; Elim H; Red; Auto.
+Intros; Apply equiv_trans with (f y); Assumption.
+Save.
+
+Lemma inverse_image_of_eq : (A,B:Set)(f:A->B)
+  (equivalence A [x,y:A](f x)=(f y)).
+Split; Red;
+[ (* reflexivity *)  Reflexivity
+| (* transitivity *) Intros; Transitivity (f y); Assumption
+| (* symmetry *) Intros; Symmetry; Assumption
+].
+Save.
-- 
cgit v1.2.3