Function COLUMN

• Defined in theory: Basic-matrix-algebra
• Source code: basic-matrix.lisp

Slots on this function:

Documentation:

Function that returns the i-th column of a given matrix

Instance-Of: Function

Arity: 3

Equivalence Axioms:

(<=> (Column ?M ?I)
     (And (Matrix ?M)
          (Positive-Integer ?I)
          (=< ?I (Column-Dimension ?M))
          (Column-Matrix ?L)
          (= (Row-Dimension ?M) (Row-Dimension ?L))
          (Forall (?J) (= (Value ?M ?J ?I) (Value ?L ?J 1)))))

Axioms:

(Nth-Domain Column 3 Column-Matrix)

(Nth-Domain Column 2 Positive-Integer)

(Nth-Domain Column 1 Matrix)

Other Related Axioms:

(=> (= (Matrix-Of-Columns @Elements) ?M)
    (= (Column ?I ?M) (Nth (Listof @Elements) ?I)))

(=> (= (Column ?M ?I) ?L)
    (Forall (?J) (= (Value ?M ?J ?I) (Value ?L ?J 1))))

(=> (= (Column ?M ?I) ?L) (= (Row-Dimension ?M) (Row-Dimension ?L)))

(=> (= (Column ?M ?I) ?L) (Column-Matrix ?L))

(=> (= (Column ?M ?I) ?L) (=< ?I (Column-Dimension ?M)))

(=> (= (Column ?M ?I) ?L) (Positive-Integer ?I))

(=> (= (Column ?M ?I) ?L) (Matrix ?M))

(=> (= (Matrix-Less-Row-And-Column ?A ?I ?J) ?B)
    (Defined (Column ?A ?J)))

(=> (= (Matrix-Less-Column ?A ?I) ?B) (Defined (Column ?A ?I)))