Reference · Vectors

rainbow.math.linear.vector.subtract-cancellation

Vectorssrc/rainbow/math/linear/vector/subtract_cancellation.clj0 definitions, 4 theorems

Shape-safe cancellation through native vector subtraction. A common subtrahend cancels from equivalence and order. A common minuend cancels from equivalence and reverses order, reflecting subtraction's antitone second argument. The proofs reduce subtraction to addition plus negation and compose checked shape, addition-cancellation, and negation- reflection laws.

Depends onmath.linear.vector.add-cancellation

vector/equivalent-subtract-right-cancel :
  (left right offset : List ℚ) (left-shape : vector/same-shape left offset)
  (right-shape : vector/same-shape right offset)
  (same : vector/equivalent (vector/subtract left offset) (vector/subtract right offset))
  → vector/equivalent left right

vector/at-most-subtract-right-cancel :
  (left right offset : List ℚ) (left-shape : vector/same-shape left offset)
  (right-shape : vector/same-shape right offset)
  (ordered : vector/at-most (vector/subtract left offset) (vector/subtract right offset))
  → vector/at-most left right

vector/equivalent-subtract-left-cancel :
  (left right offset : List ℚ) (left-shape : vector/same-shape left offset)
  (right-shape : vector/same-shape right offset)
  (same : vector/equivalent (vector/subtract offset left) (vector/subtract offset right))
  → vector/equivalent left right

vector/at-most-subtract-left-cancel :
  (left right offset : List ℚ) (left-shape : vector/same-shape left offset)
  (right-shape : vector/same-shape right offset)
  (ordered : vector/at-most (vector/subtract offset left) (vector/subtract offset right))
  → vector/at-most right left