Function TENSOR-ORDER

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

Slots on this function:

Documentation:

Function that returns the order associated with a tensor.

Instance-Of: Function

Arity: 2

Domain: Tensor-quantity

Range: Non-negative-integer

Other Related Axioms:

(Inherited-Facet-Value Slot-Value-Type
                       Tensor-Quantity
                       Tensor-Order
                       Non-Negative-Integer)

(Inherited-Facet-Value Slot-Cardinality
                       Tensor-Quantity
                       Tensor-Order
                       1)

(<=> (And (Tensor-Quantity ?T) (= (Tensor-Order ?T) 0))
     (Scalar-Quantity ?T))

(=> (Tensor-Quantity ?T)
    (And (Value-Cardinality ?T Tensor-Order 1)
         (Value-Type ?T Tensor-Order Non-Negative-Integer)
         (Value-Cardinality ?T Tensor-Order 1)
         (Value-Cardinality ?T Spatial.Dimension 1)
         (Value-Type ?T Spatial.Dimension Non-Negative-Integer)
         (Value-Cardinality ?T Spatial.Dimension 1)))

(=> (Tensor-Order $X $Y) (Non-Negative-Integer $Y))

(=> (Tensor-Order $X $Y) (Tensor-Quantity $X))

(<= (Tensor-Order $X 1) (Vector-Quantity $X))

(<=> (Vector-Quantity ?V)
     (And (Constant-Quantity ?V)
          (Tensor-Quantity ?V)
          (= (Tensor-Order ?V) 1)
          (Forall (?B ?I)
                  (=> (And (Orthonormal-Basis ?B)
                           (= (Basis.Dimension ?B)
                              (Spatial.Dimension ?V))
                           (Positive-Integer ?I)
                           (=< ?I (Spatial.Dimension ?V)))
                      (And (Defined (Vector-Component ?V ?I ?B))
                           (= (Quantity.Dimension (Vector-Component ?V
                                                                    ?I
                                                                    ?B))
                              (Quantity.Dimension ?V)))))
          (Forall (?U)
                  (=> (And (Unit-Of-Measure ?U)
                           (= (Quantity.Dimension ?U)
                              (Quantity.Dimension ?V)))
                      (Numeric-Tensor (Magnitude ?V ?U))))))

(<= (Tensor-Order $X 2) (Dyad $X))

(<=> (Dyad ?D)
     (And (Constant-Quantity ?D)
          (Tensor-Quantity ?D)
          (= (Tensor-Order ?D) 2)
          (Forall (?B ?I ?J)
                  (=> (And (Orthonormal-Basis ?B)
                           (= (Basis.Dimension ?B)
                              (Spatial.Dimension ?D))
                           (Positive-Integer ?I)
                           (=< ?I (Spatial.Dimension ?D))
                           (Positive-Integer ?J)
                           (=< ?J (Spatial.Dimension ?D)))
                      (And (Defined (Dyad-Component ?D ?I ?J ?B))
                           (= (Quantity.Dimension (Dyad-Component ?D
                                                                  ?I
                                                                  ?J
                                                                  ?B))
                              (Quantity.Dimension ?D)))))
          (Forall (?U)
                  (=> (And (Unit-Of-Measure ?U)
                           (= (Quantity.Dimension ?U)
                              (Quantity.Dimension ?D)))
                      (Numeric-Tensor (Magnitude ?D ?U))))))

(=> (= (Tensor-To-Matrix ?T ?Basis) ?M)
    (=> (= (Tensor-Order ?T) 2)
        (Square-Matrix ?M)
        (= (Size ?M) (Spatial.Dimension ?T))
        (Forall (?I ?J)
                (= (Value ?M ?I ?J) (Dyad-Component ?T ?I ?J ?Basis)))))

(=> (= (Tensor-To-Matrix ?T ?Basis) ?M)
    (=> (= (Tensor-Order ?T) 1)
        (= (Row-Dimension ?M) 1)
        (= (Column-Dimension ?M) (Spatial.Dimension ?T))
        (Forall (?I)
                (= (Value ?M 1 ?I) (Vector-Component ?T ?I ?Basis)))))

(=> (= (Tensor-To-Matrix ?T ?Basis) ?M)
    (=> (Member ?Q (Tensor-Order ?T)) (Member ?Q (Setof 1 2))))