Reference · Vectors

rainbow.math.linear.vector.shape-add

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

Shape preservation for truncating vector addition and subtraction. Equal-shaped inputs make vector/add's truncating zip consume both lists at the same position. A native two-list induction proves that the result has both input shapes. Subtraction follows by composing negation shape preservation with the addition theorem. Native and axiom-free on D63.

Depends onmath.linear.vector.shape-map

vector/add-preserves-shape :
  (left right : List ℚ) (same : vector/same-shape left right)
  → proposition/conjunction (shape₁) (shape)
  where shape := vector/same-shape (vector/add left right) right
  where shape₁ := vector/same-shape (vector/add left right) left

vector/add-preserves-left-shape :
  (left right : List ℚ) (same : vector/same-shape left right)
  → vector/same-shape (vector/add left right) left

vector/add-preserves-right-shape :
  (left right : List ℚ) (same : vector/same-shape left right)
  → vector/same-shape (vector/add left right) right

vector/subtract-preserves-shape :
  (left right : List ℚ) (same : vector/same-shape left right)
  → proposition/conjunction (shape₁) (shape)
  where shape := vector/same-shape (vector/subtract left right) right
  where shape₁ := vector/same-shape (vector/subtract left right) left