Reference · Matrices

rainbow.math.linear.matrix.add-order

Matricessrc/rainbow/math/linear/matrix/add_order.clj0 definitions, 6 theorems

Pointwise order laws for native matrix addition and subtraction. Adding the same matrix preserves order; commutativity gives the mirrored law, and transitivity combines both varying arguments. Since subtraction is addition of pointwise negation, it is monotone in its left argument, antitone in its right argument, and mixed monotone/antitone jointly. Native and axiom-free on D63.

Depends onmath.linear.matrix.signed-scale-antitone

matrix/add-right-monotone :
  (left right offset : List (List ℚ)) (ordered : matrix/at-most left right)
  → matrix/at-most (matrix/add left offset) (matrix/add right offset)

matrix/add-left-monotone :
  (left right offset : List (List ℚ)) (ordered : matrix/at-most left right)
  → matrix/at-most (matrix/add offset left) (matrix/add offset right)

matrix/add-monotone :
  (left left* right right* : List (List ℚ)) (left-ordered : matrix/at-most left left*)
  (right-ordered : matrix/at-most right right*)
  → matrix/at-most (matrix/add left right) (matrix/add left* right*)

matrix/subtract-left-monotone :
  (left left* right : List (List ℚ)) (left-ordered : matrix/at-most left left*)
  → matrix/at-most (matrix/subtract left right) (matrix/subtract left* right)

matrix/subtract-right-antitone :
  (right right* left : List (List ℚ)) (right-ordered : matrix/at-most right right*)
  → matrix/at-most (matrix/subtract left right*) (matrix/subtract left right)

matrix/subtract-monotone-antitone :
  (left left* right right* : List (List ℚ)) (left-ordered : matrix/at-most left left*)
  (right-ordered : matrix/at-most right right*)
  → matrix/at-most (matrix/subtract left right*) (matrix/subtract left* right)