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 include "ordered_divisible_group.ma".
17 record metric_space (R: todgroup) : Type ≝ {
19 metric: ms_carr → ms_carr → R;
20 mpositive: ∀a,b:ms_carr. 0 ≤ metric a b;
21 mreflexive: ∀a. metric a a ≈ 0;
22 msymmetric: ∀a,b. metric a b ≈ metric b a;
23 mtineq: ∀a,b,c:ms_carr. metric a b ≤ metric a c + metric c b
26 notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}.
27 interpretation "metric" 'delta2 a b = (metric ? ? a b).
28 notation "\delta" non associative with precedence 80 for @{ 'delta }.
29 interpretation "metric" 'delta = (metric ? ?).
31 lemma apart_of_metric_space: ∀R.metric_space R → apartness.
32 intros (R ms); apply (mk_apartness ? (λa,b:ms.0 < δ a b)); unfold;
33 [1: intros 2 (x H); cases H (H1 H2); clear H;
34 lapply (Ap≫ ? (eq_sym ??? (mreflexive ??x)) H2);
35 apply (ap_coreflexive R 0); assumption;
36 |2: intros (x y H); cases H; split;
37 [1: apply (Le≫ ? (msymmetric ????)); assumption
38 |2: apply (Ap≫ ? (msymmetric ????)); assumption]
39 |3: simplify; intros (x y z H); elim H (LExy Axy);
40 lapply (mtineq ?? x y z) as H1; elim (ap2exc ??? Axy) (H2 H2); [cases (LExy H2)]
41 clear LExy; lapply (lt_le_transitive ???? H H1) as LT0;
42 apply (lt0plus_orlt ????? LT0); apply mpositive;]
45 lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.ap_apart (apart_of_metric_space ? m) x y → 0 < δ x y.
46 intros 2 (R m); cases m 0; simplify; intros; assumption; qed.