% @(#)$Id: PreVector.lsl,v 1.3 1997/06/05 03:10:51 leavens Exp $
PreVector(T): trait

  assumes RingWithUnit, Abelian(* for \circ),
           TotalOrder, CoerceToReal(T)

  includes PreVectorSpace(T), Real

  introduces
     __ \cdot __: Vec[T], Vec[T] -> T  % inner product
    length: Vec[T] -> T
  
  asserts
    \forall u,v,w: Vec[T], a, b: T
 
      % the inner product is bilinear
      (u + v) \cdot w == (u \cdot w) + (v \cdot w);
      u \cdot (v + w) == (u \cdot v) + (u \cdot w);
      (a * u) \cdot v == a * (u \cdot v);
      (a * u) \cdot v == u \cdot (a * v);

      % the inner product is symmetric (commutative)
      u \cdot v == v \cdot u;

      % the inner product is positive definite
      (u \cdot u) >= 0;
      (u \cdot u = 0) == (u = 0);

      approximates(length(u), sqrt(toReal(u \cdot u)));

  implies
    PreVectorSig(T)
    converts
       __ \cdot __: Vec[T], Vec[T] -> T

[Index]

HTML generated using lcpp2html.