X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fmetric_lattice.ma;fp=helm%2Fsoftware%2Fmatita%2Fdama%2Fmetric_lattice.ma;h=a2d25734217ead71fd14871f92b2264dd0987d01;hb=b3dd479a0a36aeea948dcea09336fe8dfec1462d;hp=40f3d41eb8f32fa057cf46faf463fe2f045f5381;hpb=c5cee90d95a54db8897a688f0bade4c503d82e15;p=helm.git

diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma
index 40f3d41eb..a2d257342 100644
--- a/helm/software/matita/dama/metric_lattice.ma
+++ b/helm/software/matita/dama/metric_lattice.ma
@@ -12,18 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-
-
 include "metric_space.ma".
 include "lattice.ma".
 
 record mlattice_ (R : todgroup) : Type ≝ {
   ml_mspace_: metric_space R;
-  ml_lattice_: lattice;
-  ml_with_: ms_carr ? ml_mspace_ = l_carr ml_lattice_;
-  ml_with2_: l_carr ml_lattice_ = apart_of_metric_space ? ml_mspace_ 
+  ml_lattice:> lattice;
+  ml_with_: ms_carr ? ml_mspace_ = apart_of_excess (pl_carr ml_lattice) 
 }.
 
+(*
 lemma ml_lattice: ∀R.mlattice_ R → lattice.
 intros (R ml); apply (mk_lattice (apart_of_metric_space ? (ml_mspace_ ? ml))); try unfold eq;
 cases (ml_with2_ ? ml);
@@ -36,13 +34,15 @@ cases (ml_with2_ ? ml);
 qed.
 
 coercion cic:/matita/metric_lattice/ml_lattice.con.
+*)
 
 lemma ml_mspace: ∀R.mlattice_ R → metric_space R.
-intros (R ml); apply (mk_metric_space R ml);
+intros (R ml); apply (mk_metric_space R (apart_of_excess ml)); 
+unfold apartness_OF_mlattice_; 
+[rewrite < (ml_with_ ? ml); apply (metric ? (ml_mspace_ ? ml))]
 cases (ml_with_ ? ml); simplify;
-[apply (metric ? (ml_mspace_ ? ml));|apply (mpositive ? (ml_mspace_ ? ml));
-|apply (mreflexive ? (ml_mspace_ ? ml));|apply (msymmetric ? (ml_mspace_ ? ml));
-|apply (mtineq ? (ml_mspace_ ? ml))]
+[apply (mpositive ? (ml_mspace_ ? ml));|apply (mreflexive ? (ml_mspace_ ? ml));
+|apply (msymmetric ? (ml_mspace_ ? ml));|apply (mtineq ? (ml_mspace_ ? ml))]
 qed.
 
 coercion cic:/matita/metric_lattice/ml_mspace.con.