bir georganization, most of the structures done

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

diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma
index 62a84090cbc446a6a55a0379b85075a4e9160318..c8a9c895fc4be18204bd2dc3e851b186085ada06 100644 (file)
--- a/helm/software/matita/dama/metric_lattice.ma
+++ b/helm/software/matita/dama/metric_lattice.ma
@@ -14,21 +14,21 @@
 
 set "baseuri" "cic:/matita/metric_lattice/".
 
-include "metric_set.ma".
+include "metric_space.ma".
 include "lattice.ma".
 
 record mlattice (R : ogroup) : Type ≝ {
-  ml_mset_: metric_set R;
+  ml_mspace_: metric_space R;
   ml_lattice:> lattice;
-  ml_with_: ms_carr ? ml_mset_ = ap_carr (l_carr ml_lattice)
+  ml_with_: ms_carr ? ml_mspace_ = ap_carr (l_carr ml_lattice)
 }.
 
-lemma ml_mset: ∀R.mlattice R → metric_set R.
-intros (R ml); apply (mk_metric_set R ml); unfold Type_OF_mlattice;
+lemma ml_mspace: ∀R.mlattice R → metric_space R.
+intros (R ml); apply (mk_metric_space R ml); unfold Type_OF_mlattice;
 cases (ml_with_ ? ml); simplify;
-[apply (metric ? (ml_mset_ ? ml));|apply (mpositive ? (ml_mset_ ? ml));
-|apply (mreflexive ? (ml_mset_ ? ml));|apply (msymmetric ? (ml_mset_ ? ml));
-|apply (mtineq ? (ml_mset_ ? ml))]
+[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))]
 qed.
 
-coercion cic:/matita/metric_lattice/ml_mset.con.
+coercion cic:/matita/metric_lattice/ml_mspace.con.