Library Coq.Relations.Relations
Require
Export
Relation_Definitions
.
Require
Export
Relation_Operators
.
Require
Export
Operators_Properties
.
Lemma
inverse_image_of_equivalence
:
forall
(
A
B
:Type) (
f
:A ->
B
) (
r
:relation
B
),
equivalence
B
r
->
equivalence
A
(
fun
x
y
:A =>
r
(
f
x
) (
f
y
)).
Lemma
inverse_image_of_eq
:
forall
(
A
B
:Type) (
f
:A ->
B
),
equivalence
A
(
fun
x
y
:A =>
f
x
=
f
y
).