join: pml_carr → pml_carr → pml_carr
}.
-interpretation "valued lattice meet" 'and a b =
- (cic:/matita/premetric_lattice/meet.con _ _ a b).
+interpretation "valued lattice meet" 'and a b = (meet _ _ a b).
-interpretation "valued lattice join" 'or a b =
- (cic:/matita/premetric_lattice/join.con _ _ a b).
+interpretation "valued lattice join" 'or a b = (join _ _ a b).
record premetric_lattice_props (R : todgroup) (ml : premetric_lattice_ R) : Prop ≝ {
prop1a: ∀a : ml.δ (a ∧ a) a ≈ 0;
apply (prop5 ? pml pml);]
qed.
-coercion cic:/matita/premetric_lattice/lattice_of_pmlattice.con.
\ No newline at end of file
+coercion cic:/matita/premetric_lattice/lattice_of_pmlattice.con.