X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fnlibrary%2Fbasics%2Frelations.ma;fp=matitaB%2Fmatita%2Fnlibrary%2Fbasics%2Frelations.ma;h=9a01823bec70fb4652c64465281e090dfb20014c;hb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;hp=0000000000000000000000000000000000000000;hpb=f04a064bb34aabaf91dc0c48e3b08b37ecd7b0a2;p=helm.git

diff --git a/matitaB/matita/nlibrary/basics/relations.ma b/matitaB/matita/nlibrary/basics/relations.ma
new file mode 100644
index 000000000..9a01823be
--- /dev/null
+++ b/matitaB/matita/nlibrary/basics/relations.ma
@@ -0,0 +1,45 @@
+(**************************************************************************)
+(*       ___	                                                            *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Plogic/connectives.ma".
+
+ndefinition relation : Type \to Type
+≝ λA:Type.A→A→Prop. 
+
+nrecord relation (A:Type) : Type ≝
+{fun:2> A→A→Prop}.
+
+ndefinition reflexive: ∀A:Type.∀R :relation A.Prop
+≝ λA.λR.∀x:A.R x x.
+
+ndefinition symmetric: ∀A:Type.∀R: relation A.Prop
+≝ λA.λR.∀x,y:A.R x y → R y x.
+
+ndefinition transitive: ∀A:Type.∀R:relation A.Prop
+≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
+
+ndefinition irreflexive: ∀A:Type.∀R:relation A.Prop
+≝ λA.λR.∀x:A.¬(R x x).
+
+ndefinition cotransitive: ∀A:Type.∀R:relation A.Prop
+≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
+
+ndefinition tight_apart: ∀A:Type.∀eq,ap:relation A.Prop
+≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
+(eq x y → ¬(ap x y)).
+
+ndefinition antisymmetric: ∀A:Type.∀R:relation A.Prop
+≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
+
+