1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: Equiv.v,v 1.4 2004/04/23 10:01:02 lcf Exp $ *)
21 include "metrics/IR_CPMSpace.ma".
27 (*#* **Equivalent Pseudo Metric Spaces
31 We say that two pseudo metric spaces are equivalent, when there exists a
32 bijective, structure-preserving function between them.
35 inline procedural "cic:/CoRN/metrics/Equiv/equivalent_psmetric.con" as definition.
37 inline procedural "cic:/CoRN/metrics/Equiv/isopsmetry.con" as definition.
40 Implicit Arguments isopsmetry [X Y].
43 inline procedural "cic:/CoRN/metrics/Equiv/isopsmetry_imp_bij.con" as lemma.
45 inline procedural "cic:/CoRN/metrics/Equiv/isopsmetry_imp_lipschitz.con" as lemma.
47 inline procedural "cic:/CoRN/metrics/Equiv/id_is_isopsmetry.con" as lemma.
49 inline procedural "cic:/CoRN/metrics/Equiv/comp_resp_isopsmetry.con" as lemma.
51 inline procedural "cic:/CoRN/metrics/Equiv/inv_isopsmetry.con" as lemma.
53 inline procedural "cic:/CoRN/metrics/Equiv/MSequivalent.con" as definition.
56 Not all pseudo metric spaces are equivalent:
59 inline procedural "cic:/CoRN/metrics/Equiv/MSequivalent_discr.con" as lemma.