Reference · Vectors

rainbow.math.linear.vector.subtract-laws

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

Congruence and mixed-variance order laws for native vector subtraction. Subtraction is addition of a negated vector. Its first argument is monotone, its second argument is antitone, and it respects componentwise signed equivalence in both arguments. These proofs compose existing checked vector laws and add no recursion, definitions, axioms, or trusted-base code.

Depends onmath.linear.vector.add-order

vector/subtract-respects-equivalence :
  (left left-prime right right-prime : List ℚ)
  (left-same : vector/equivalent left left-prime)
  (right-same : vector/equivalent right right-prime)
  → vector/equivalent (vector/subtract left right) (vector/subtract left-prime right-prime)

vector/subtract-left-monotone :
  (left left-prime right : List ℚ) (left-ordered : vector/at-most left left-prime)
  → vector/at-most (vector/subtract left right) (vector/subtract left-prime right)

vector/subtract-right-antitone :
  (right right-prime left : List ℚ) (right-ordered : vector/at-most right right-prime)
  → vector/at-most (vector/subtract left right-prime) (vector/subtract left right)

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