Reference · Matrices

rainbow.math.linear.matrix.pointwise-order-laws

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

Partial-order and quotient-transport laws for native finite matrices. Matrix pointwise order is transitive, reversed by pointwise negation, and antisymmetric up to length-sensitive matrix equivalence. Matrix equivalence yields both order directions, and order endpoints may therefore be replaced by equivalent representatives. Dimension mismatches eliminate through the falsity branches of the reducible relation. Native and axiom-free on D63.

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

matrix/negate-reverses-order :
  (left right : List (List ℚ)) (ordered : matrix/at-most left right)
  → matrix/at-most (matrix/negate right) (matrix/negate left)

matrix/at-most-transitive :
  (left middle right : List (List ℚ)) (left-middle : matrix/at-most left middle)
  (middle-right : matrix/at-most middle right)
  → matrix/at-most left right

matrix/at-most-antisymmetric :
  (left right : List (List ℚ)) (left-right : matrix/at-most left right)
  (right-left : matrix/at-most right left)
  → matrix/equivalent left right

matrix/equivalent-to-mutual-at-most :
  (left right : List (List ℚ)) (same : matrix/equivalent left right)
  → proposition/conjunction (matrix/at-most left right) (matrix/at-most right left)

matrix/equivalent-to-at-most :
  (left right : List (List ℚ)) (same : matrix/equivalent left right)
  → matrix/at-most left right

matrix/at-most-respects-equivalence :
  (left left* right right* : List (List ℚ)) (left-same : matrix/equivalent left left*)
  (right-same : matrix/equivalent right right*) (ordered : matrix/at-most left right)
  → matrix/at-most left* right*