Relation LINEAR-SPACE

• Defined in theory: Abstract-algebra
• Source code: abstract-algebra.lisp

Slots on this relation:

Documentation:

Abstract linear or vector space of arbitrary dimension. Defines operations on vectors over a scalar field.

Instance-Of: Relation

Arity: 7

Equivalence Axioms:

(<=> (Linear-Space ?Scalar-Domain
                   ?Vector-Domain
                   ?S-Zero
                   ?S-One
                   ?V-Zero
                   ?Mult
                   ?Add)
     (And (Class ?Scalar-Domain)
          (Class ?Vector-Domain)
          (Field ?Scalar-Domain ?Add ?S-Zero ?Mult ?S-One)
          (Abelian-Group ?Vector-Domain ?Add ?V-Zero)
          (Forall (?S ?V)
                  (=> (And (Instance-Of ?S ?Scalar-Domain)
                           (Instance-Of ?V ?Vector-Domain))
                      (Instance-Of (Value ?Mult ?S ?V)
                                   ?Vector-Domain)))
          (Forall (?S ?V1 ?V2)
                  (=> (And (Instance-Of ?S ?Scalar-Domain)
                           (Instance-Of ?V1 ?Vector-Domain)
                           (Instance-Of ?V2 ?Vector-Domain))
                      (= (Value ?Mult ?S (Value ?Add ?V1 ?V2))
                         (Value ?Add
                                (Value ?Mult ?S ?V1)
                                (Value ?Mult ?S ?V2)))))
          (Forall (?S1 ?S2 ?V)
                  (=> (And (Instance-Of ?S1 ?Scalar-Domain)
                           (Instance-Of ?S2 ?Scalar-Domain)
                           (Instance-Of ?V ?Vector-Domain))
                      (= (Value ?Mult (Value ?Add ?S1 ?S2) ?V)
                         (Value ?Add
                                (Value ?Mult ?S1 ?V)
                                (Value ?Mult ?S2 ?V)))))
          (Forall (?S1 ?S2 ?V)
                  (=> (And (Instance-Of ?S1 ?Scalar-Domain)
                           (Instance-Of ?S2 ?Scalar-Domain)
                           (Instance-Of ?V ?Vector-Domain))
                      (= (Value ?Mult (Value ?Mult ?S1 ?S2) ?V)
                         (Value ?Mult ?S1 (Value ?Mult ?S2 ?V)))))
          (Forall (?V)
                  (=> (Instance-Of ?V ?Vector-Domain)
                      (And (= (Value ?Mult ?S-One ?V) ?V)
                           (= (Value ?Mult ?S-Zero ?V) ?V-Zero))))))

Axioms:

(Nth-Domain Linear-Space 2 Class)

(Nth-Domain Linear-Space 1 Class)

Other Related Axioms:

(<=> (Linear-Space ?Scalar-Domain
                   ?Vector-Domain
                   ?S-Zero
                   ?S-One
                   ?V-Zero
                   ?Mult
                   ?Add)
     (And (Class ?Scalar-Domain)
          (Class ?Vector-Domain)
          (Field ?Scalar-Domain ?Add ?S-Zero ?Mult ?S-One)
          (Abelian-Group ?Vector-Domain ?Add ?V-Zero)
          (Forall (?S ?V)
                  (=> (And (Instance-Of ?S ?Scalar-Domain)
                           (Instance-Of ?V ?Vector-Domain))
                      (Instance-Of (Value ?Mult ?S ?V)
                                   ?Vector-Domain)))
          (Forall (?S ?V1 ?V2)
                  (=> (And (Instance-Of ?S ?Scalar-Domain)
                           (Instance-Of ?V1 ?Vector-Domain)
                           (Instance-Of ?V2 ?Vector-Domain))
                      (= (Value ?Mult ?S (Value ?Add ?V1 ?V2))
                         (Value ?Add
                                (Value ?Mult ?S ?V1)
                                (Value ?Mult ?S ?V2)))))
          (Forall (?S1 ?S2 ?V)
                  (=> (And (Instance-Of ?S1 ?Scalar-Domain)
                           (Instance-Of ?S2 ?Scalar-Domain)
                           (Instance-Of ?V ?Vector-Domain))
                      (= (Value ?Mult (Value ?Add ?S1 ?S2) ?V)
                         (Value ?Add
                                (Value ?Mult ?S1 ?V)
                                (Value ?Mult ?S2 ?V)))))
          (Forall (?S1 ?S2 ?V)
                  (=> (And (Instance-Of ?S1 ?Scalar-Domain)
                           (Instance-Of ?S2 ?Scalar-Domain)
                           (Instance-Of ?V ?Vector-Domain))
                      (= (Value ?Mult (Value ?Mult ?S1 ?S2) ?V)
                         (Value ?Mult ?S1 (Value ?Mult ?S2 ?V)))))
          (Forall (?V)
                  (=> (Instance-Of ?V ?Vector-Domain)
                      (And (= (Value ?Mult ?S-One ?V) ?V)
                           (= (Value ?Mult ?S-Zero ?V) ?V-Zero))))))