1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/metric_lattice/".
17 include "metric_set.ma".
20 record mlattice (R : ogroup) : Type ≝ {
21 ml_mset_: metric_set R;
23 ml_with_: ms_carr ? ml_mset_ = ap_carr (l_carr ml_lattice)
26 lemma ml_mset: ∀R.mlattice R → metric_set R.
27 intros (R ml); apply (mk_metric_set R ml); unfold Type_OF_mlattice;
28 cases (ml_with_ ? ml); simplify;
29 [apply (metric ? (ml_mset_ ? ml));|apply (mpositive ? (ml_mset_ ? ml));
30 |apply (mreflexive ? (ml_mset_ ? ml));|apply (msymmetric ? (ml_mset_ ? ml));
31 |apply (mtineq ? (ml_mset_ ? ml))]
34 coercion cic:/matita/metric_lattice/ml_mset.con.