Reference · Vectors

rainbow.math.linear.vector.negate-reflection

Vectorssrc/rainbow/math/linear/vector/negate_reflection.clj0 definitions, 2 theorems

Involutive vector negation reflects order and equivalence. -left <= -right -> right <= left -left ~ -right -> left ~ right Reverse the negated order once more, then transport through vector negation involutivity. Equivalence reflection applies that result to both mutual bounds. Native and axiom-free on D63.

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

vector/negate-reflects-order :
  (left right : List ℚ)
  (ordered : vector/at-most (vector/negate left) (vector/negate right))
  → vector/at-most right left

vector/negate-reflects-equivalence :
  (left right : List ℚ)
  (same : vector/equivalent (vector/negate left) (vector/negate right))
  → vector/equivalent left right