Library Coq.Sets.Relations_1_facts
Require
Export
Relations_1
.
Definition
Complement
(
U
:
Type
) (
R
:
Relation
U
) :
Relation
U
:=
fun
x
y
:
U
=>
~
R
x
y
.
Theorem
Rsym_imp_notRsym
:
forall
(
U
:
Type
) (
R
:
Relation
U
),
Symmetric
U
R
->
Symmetric
U
(
Complement
U
R
).
Theorem
Equiv_from_preorder
:
forall
(
U
:
Type
) (
R
:
Relation
U
),
Preorder
U
R
->
Equivalence
U
(
fun
x
y
:
U
=>
R
x
y
/\
R
y
x
).
Hint Resolve
Equiv_from_preorder
.
Theorem
Equiv_from_order
:
forall
(
U
:
Type
) (
R
:
Relation
U
),
Order
U
R
->
Equivalence
U
(
fun
x
y
:
U
=>
R
x
y
/\
R
y
x
).
Hint Resolve
Equiv_from_order
.
Theorem
contains_is_preorder
:
forall
U
:
Type
,
Preorder
(
Relation
U
) (
contains
U
).
Hint Resolve
contains_is_preorder
.
Theorem
same_relation_is_equivalence
:
forall
U
:
Type
,
Equivalence
(
Relation
U
) (
same_relation
U
).
Hint Resolve
same_relation_is_equivalence
.
Theorem
cong_reflexive_same_relation
:
forall
(
U
:
Type
) (
R
R'
:
Relation
U
),
same_relation
U
R
R'
->
Reflexive
U
R
->
Reflexive
U
R'
.
Theorem
cong_symmetric_same_relation
:
forall
(
U
:
Type
) (
R
R'
:
Relation
U
),
same_relation
U
R
R'
->
Symmetric
U
R
->
Symmetric
U
R'
.
Theorem
cong_antisymmetric_same_relation
:
forall
(
U
:
Type
) (
R
R'
:
Relation
U
),
same_relation
U
R
R'
->
Antisymmetric
U
R
->
Antisymmetric
U
R'
.
Theorem
cong_transitive_same_relation
:
forall
(
U
:
Type
) (
R
R'
:
Relation
U
),
same_relation
U
R
R'
->
Transitive
U
R
->
Transitive
U
R'
.