Function THE-ZERO-VECTOR-OF-TYPE

• Defined in theory: Tensor-quantities
• Source code: tensor-quantities.lisp

Slots on this function:

Documentation:

The ?spatdim dimensional zero vector of physical dimension ?physdim.

Instance-Of: Function

Arity: 3

Axioms:

(Nth-Domain The-Zero-Vector-Of-Type 2 Physical-Dimension)

(Nth-Domain The-Zero-Vector-Of-Type 1 Positive-Integer)

(Nth-Domain The-Zero-Vector-Of-Type 3 Vector-Quantity)

Other Related Axioms:

(Forall (?Physdim ?Spatdim)
        (Abelian-Group (Vector-Quantities-Of-Dimensions ?Physdim
                                                        ?Spatdim)
                       +
                       (The-Zero-Vector-Of-Type ?Spatdim ?Physdim)))

(=> (And (Vector-Quantity ?X) (- ?X ?Y))
    (And (Vector-Quantity ?Y)
         (= (+ ?X ?Y)
            (The-Zero-Vector-Of-Type (Quantity.Dimension ?X)
                                     (Spatial.Dimension ?X)))))

(=> (= (The-Zero-Vector-Of-Type ?Spatdim ?Physdim) ?V0)
    (Forall (?V)
            (=> (Vector-Quantity ?V)
                (= (Dot ?V ?V0)
                   (The-Zero-Scalar-For-Dimension ?Physdim)))))