Reference · Vectors

rainbow.math.linear.vector.equivalence-transitivity

Vectorssrc/rainbow/math/linear/vector/equivalence_transitivity.clj0 definitions, 1 theorems

Transitivity of length-sensitive componentwise vector equivalence. Each vector equivalence yields pointwise bounds in both directions. Compose the forward bounds and the backward bounds with vector/at-most-transitive, then recover vector equivalence by vector/at-most-antisymmetric. This avoids duplicating the underlying two-list induction.

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

vector/equivalent-transitive :
  (left middle right : List ℚ) (left-middle : vector/equivalent left middle)
  (middle-right : vector/equivalent middle right)
  → vector/equivalent left right