diff options
| -rw-r--r-- | theories/IntMap/Adist.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/theories/IntMap/Adist.v b/theories/IntMap/Adist.v index ec08fb35f1..f8bae6853c 100644 --- a/theories/IntMap/Adist.v +++ b/theories/IntMap/Adist.v @@ -258,10 +258,11 @@ Qed. (*s $d$ is an ultrametric distance, that is, not only $d(a,a')\leq d(a,a'')+d(a'',a')$, but in fact $d(a,a')\leq max(d(a,a''),d(a'',a'))$. This means that $min(pd(a,a''),pd(a'',a'))<=pd(a,a')$ (lemma [ad_pdist_ultra] below). - This follows from the fact that $a \Ra |a| = 1/2^\texttt{ad\_plength}(a))$ + This follows from the fact that $a \Ra |a| = 1/2^{\texttt{ad\_plength}}(a))$ is an ultrametric norm, i.e. that $|a-a'| \leq max (|a-a''|, |a''-a'|)$, or equivalently that $|a+b|<=max(|a|,|b|)$, i.e. that - min $(\texttt{ad\_plength}(a), \texttt{ad\_plength}(b)) \leq \texttt{ad\_plength} (a~\texttt{xor}~ b)$ + min $(\texttt{ad\_plength}(a), \texttt{ad\_plength}(b)) \leq + \texttt{ad\_plength} (a~\texttt{xor}~ b)$ (lemma [ad_plength_ultra]). *) |