diff options
Diffstat (limited to 'theories/Sets/Relations_1.v')
| -rwxr-xr-x | theories/Sets/Relations_1.v | 42 |
1 files changed, 21 insertions, 21 deletions
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index 74c031726..16a00740d 100755 --- a/theories/Sets/Relations_1.v +++ b/theories/Sets/Relations_1.v @@ -27,41 +27,41 @@ (*i $Id$ i*) Section Relations_1. - Variable U: Type. + Variable U : Type. - Definition Relation := U -> U -> Prop. - Variable R: Relation. + Definition Relation := U -> U -> Prop. + Variable R : Relation. - Definition Reflexive : Prop := (x: U) (R x x). + Definition Reflexive : Prop := forall x:U, R x x. - Definition Transitive : Prop := (x,y,z: U) (R x y) -> (R y z) -> (R x z). + Definition Transitive : Prop := forall x y z:U, R x y -> R y z -> R x z. - Definition Symmetric : Prop := (x,y: U) (R x y) -> (R y x). + Definition Symmetric : Prop := forall x y:U, R x y -> R y x. - Definition Antisymmetric : Prop := - (x: U) (y: U) (R x y) -> (R y x) -> x == y. + Definition Antisymmetric : Prop := forall x y:U, R x y -> R y x -> x = y. - Definition contains : Relation -> Relation -> Prop := - [R,R': Relation] (x: U) (y: U) (R' x y) -> (R x y). + Definition contains (R R':Relation) : Prop := + forall x y:U, R' x y -> R x y. - Definition same_relation : Relation -> Relation -> Prop := - [R,R': Relation] (contains R R') /\ (contains R' R). + Definition same_relation (R R':Relation) : Prop := + contains R R' /\ contains R' R. Inductive Preorder : Prop := - Definition_of_preorder: Reflexive -> Transitive -> Preorder. + Definition_of_preorder : Reflexive -> Transitive -> Preorder. Inductive Order : Prop := - Definition_of_order: Reflexive -> Transitive -> Antisymmetric -> Order. + Definition_of_order : + Reflexive -> Transitive -> Antisymmetric -> Order. Inductive Equivalence : Prop := - Definition_of_equivalence: - Reflexive -> Transitive -> Symmetric -> Equivalence. + Definition_of_equivalence : + Reflexive -> Transitive -> Symmetric -> Equivalence. Inductive PER : Prop := - Definition_of_PER: Symmetric -> Transitive -> PER. + Definition_of_PER : Symmetric -> Transitive -> PER. End Relations_1. -Hints Unfold Reflexive Transitive Antisymmetric Symmetric contains - same_relation : sets v62. -Hints Resolve Definition_of_preorder Definition_of_order - Definition_of_equivalence Definition_of_PER : sets v62. +Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains + same_relation: sets v62. +Hint Resolve Definition_of_preorder Definition_of_order + Definition_of_equivalence Definition_of_PER: sets v62.
\ No newline at end of file |