blob: 86627c8b3a73424376f8495df010b0a9efc5b175 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
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.
Qed.
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
].
Qed.
|
