X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fmetric_space.ma;h=2ea43c03ae11017df5c262218a41b570ff11c15a;hb=5806e0aa438ae85f09c93c93ba9f53d9663d7420;hp=d36e90a68d2b9eaff7aa1e24371722e5821efe48;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma
index d36e90a68..2ea43c03a 100644
--- a/helm/software/matita/dama/metric_space.ma
+++ b/helm/software/matita/dama/metric_space.ma
@@ -23,7 +23,6 @@ record metric_space (R : todgroup) : Type ≝ {
   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}.
@@ -48,4 +47,7 @@ intros (R ms); apply (mk_apartness ? (apart_metric ? ms)); unfold apart_metric;
     apply (lt0plus_orlt ????? LT0); apply mpositive;]
 qed.
     
-coercion cic:/matita/metric_space/apart_of_metric_space.con.
+(* coercion cic:/matita/metric_space/apart_of_metric_space.con. *)
+
+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.