Quelle  metric_vect.pvs  Sprache: unbekannt

metric_vect[n,m:posnat] : THEORY
BEGIN

  IMPORTING vectors@vectors
  IMPORTING cont_vect[n,m]

  
    f(v: Vector[n])(x: real): Vector[n]

    ex(v: Vector[1]): real = v(0)

    CONVERSION ex

    d(x,y:real): real = abs(x-y)

    dn(x,y: Vector[n]): real = norm[n](x-y)


END metric_vect