3.27 ok

[helm.git] / helm / software / matita / dama / metric_space.ma

diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma
index 35e0e0066334862681f1aa7e471434199172899d..2ea43c03ae11017df5c262218a41b570ff11c15a 100644 (file)
--- a/helm/software/matita/dama/metric_space.ma
+++ b/helm/software/matita/dama/metric_space.ma
@@ -12,18 +12,17 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/metric_space/".
 
-include "ordered_groups.ma".
 
-record metric_space (R : ogroup) : Type ≝ {
+include "ordered_divisible_group.ma".
+
+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}.
@@ -34,7 +33,7 @@ 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.
+lemma apart_of_metric_space: ∀R:todgroup.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);
@@ -48,3 +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. *)
+
+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.