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}.
apply (lt0plus_orlt ????? LT0); apply mpositive;]
qed.
-coercion cic:/matita/metric_space/apart_of_metric_space.con.
+(* 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.