Class ORTHONORMAL-BASIS

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

Slots on this class:

Documentation:

A set of n vector-quantities in an n-dimensional vector space which form an ortho-normal basis, the n vector-quantities are linearly independent and the scalar product of any two is the identity-scalar.

---

Slots on instances of this class:

Basis.Dimension:

Slot-Cardinality: 1

Axioms:

(=> (Orthonormal-Basis ?B)
    (And (Forall (?N)
                 (=> (And (Positive-Integer ?N)
                          (=< ?N (Basis.Dimension ?B)))
                     (Defined (Basis.Vec ?B ?N))))
         (Forall (?N1 ?N2)
                 (=> (And (Positive-Integer ?N1)
                          (Positive-Integer ?N2)
                          (=< ?N1 (Basis.Dimension ?B))
                          (=< ?N2 (Basis.Dimension ?B)))
                     (=> (= ?N1 ?N2)
                         (= (Dot (Basis.Vec ?B ?N1)
                                 (Basis.Vec ?B ?N2))
                            1))
                     (=> (/= ?N1 ?N2)
                         (= (Dot (Basis.Vec ?B ?N1)
                                 (Basis.Vec ?B ?N2))
                            0))))))