Reference · Vectors

rainbow.math.linear.vector.equivalence-laws

Vectorssrc/rainbow/math/linear/vector/equivalence_laws.clj0 definitions, 5 theorems

Structural laws for length-sensitive componentwise signed-vector equivalence. Reflexivity and symmetry are proved for arbitrary finite vectors by native List induction. The map theorem is deliberately higher-order: any component function that respects signed equivalence respects vector equivalence when mapped over a list. Vector negation congruence is then a specialization of that general theorem, while involutivity maps the corresponding scalar law over one list.

vector/equivalent-reflexive :
  (values : List ℚ)
  → vector/equivalent values values

vector/equivalent-symmetric :
  (left right : List ℚ) (same : vector/equivalent left right)
  → vector/equivalent right left

vector/map-respects-equivalence :
  (mapping : ℚ → ℚ)
  (respects : ∀ (left-component : ℚ), ∀ (right-component : ℚ), ∀ (component-same : left-component = right-component), mapping left-component = mapping right-component)
  (left right : List ℚ) (same : vector/equivalent left right)
  → vector/equivalent (list/map ℚ ℚ mapping left) (list/map ℚ ℚ mapping right)

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

vector/negate-involutive :
  (values : List ℚ)
  → vector/equivalent (vector/negate (vector/negate values)) values