X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fmetric_space.ma;h=2266fe9e9618a08a56e5a8a91e3033e9123818a8;hb=473f04c051fae559d1598e8e1a3f3bf5e43cbe64;hp=d529af83cd16c05d7c96495b01c12363c7e8c745;hpb=a42d4bd78f10ac8fc725c50c193503a3f29b848f;p=helm.git

diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma
index d529af83c..2266fe9e9 100644
--- a/helm/software/matita/dama/metric_space.ma
+++ b/helm/software/matita/dama/metric_space.ma
@@ -12,18 +12,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/metric_space/".
+include "ordered_divisible_group.ma".
 
-include "ordered_group.ma".
-
-record metric_space (R : ogroup) : Type ≝ {
+record metric_space (R: todgroup) : Type ≝ {
   ms_carr :> Type;
   metric: ms_carr → ms_carr → R;
   mpositive: ∀a,b:ms_carr. 0 ≤ metric a b; 
   mreflexive: ∀a. metric a a ≈ 0;
   msymmetric: ∀a,b. metric a b ≈ metric b a;
   mtineq: ∀a,b,c:ms_carr. metric a b ≤ metric a c + metric c b
-  (* manca qualcosa per essere una metrica e non una semimetrica *)
 }.
 
 notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}.
@@ -31,20 +28,19 @@ interpretation "metric" 'delta2 a b = (cic:/matita/metric_space/metric.con _ _ a
 notation "\delta" non associative with precedence 80 for @{ 'delta }.
 interpretation "metric" 'delta = (cic:/matita/metric_space/metric.con _ _).
 
-definition apart_metric:=
-  λR.λms:metric_space R.λa,b:ms.0 < δ a b.
-
-lemma apart_of_metric_space: ∀R:ogroup.metric_space R → apartness.
-intros (R ms); apply (mk_apartness ? (apart_metric ? ms)); unfold apart_metric; unfold;
-[1: intros 2 (x H); cases H (H1 H2); 
-    lapply (ap_rewr ???? (eq_sym ??? (mreflexive ??x)) H2);
+lemma apart_of_metric_space: ∀R.metric_space R → apartness.
+intros (R ms); apply (mk_apartness ? (λa,b:ms.0 < δ a b)); unfold;
+[1: intros 2 (x H); cases H (H1 H2); clear H; 
+    lapply (Ap≫ ? (eq_sym ??? (mreflexive ??x)) H2);
     apply (ap_coreflexive R 0); assumption;
 |2: intros (x y H); cases H; split;
-    [1: apply (le_rewr ???? (msymmetric ????)); assumption
-    |2: apply (ap_rewr ???? (msymmetric ????)); assumption]
-|3: simplify; intros (x y z H); cases H (LExy Axy);
-    lapply (mtineq ?? x y z) as H1; whd in Axy; cases Axy (H2 H2); [cases (LExy H2)]
+    [1: apply (Le≫ ? (msymmetric ????)); assumption
+    |2: apply (Ap≫ ? (msymmetric ????)); assumption]
+|3: simplify; intros (x y z H); elim H (LExy Axy);
+    lapply (mtineq ?? x y z) as H1; elim (ap2exc ??? Axy) (H2 H2); [cases (LExy H2)]
     clear LExy; lapply (lt_le_transitive ???? H H1) as LT0;
     apply (lt0plus_orlt ????? LT0); apply mpositive;]
 qed.
     
+lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.ap_apart (apart_of_metric_space ? m) x y → 0 < δ x y.
+intros 2 (R m); cases m 0; simplify; intros; assumption; qed.