Reference · Vectors

rainbow.math.linear.vector.add-order

Vectorssrc/rainbow/math/linear/vector/add_order.clj0 definitions, 6 theorems

Translation monotonicity for native signed vectors. left <= right -> left + offset <= right + offset All relations are `vector/at-most`, so the hypothesis carries equal dimension for left and right. The fixed offset may have any length: vector/add truncates both results at the same point, preserving equal result dimensions and the componentwise order. Impossible mismatched-input branches are eliminated from the order evidence. Native and axiom-free on D63.

Depends onmath.finite.vectormath.linear.vector.pointwise-order-laws

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

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

vector/add-monotone :
  (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/add left right) (vector/add left-prime right-prime)

vector/add-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/add left right) (vector/add left-prime right-prime)

vector/add-commutative :
  (left right : List ℚ)
  → vector/equivalent (vector/add left right) (vector/add right left)

vector/add-associative :
  (left middle right : List ℚ)
  → vector/equivalent (add) (add₁)
  where add := vector/add (vector/add left middle) right
  where add₁ := vector/add left (vector/add middle right)