Reference · Vectors

rainbow.math.linear.vector.equivalence

Vectors src/rainbow/math/linear/vector/equivalence.clj1 definitions, 5 theorems

Componentwise equivalence of signed-rational vectors: two vectors are equivalent when every pair of components is signed-equivalent. This is a conjunction folded over the two component lists (a Prop-valued nested data/List.rec, the shape of vector/add but eliminating into Prop): equivalent [a..] [b..] = (a_1 ~ b_1) AND ... AND (a_n ~ b_n) AND True It is the vector analogue of signed/equivalent, and it is what lets worked vector results that come out as non-canonical Grothendieck pairs (e.g. a subtraction [4,4]-[1,1] whose components are the pair (4,1), not the reduced 3) be proven equal to their reduced vectors -- unblocking direct-search and non-origin optimizer worked examples. Requires the finite-vector capability (data/List over signed) in the environment.

vector/equivalent

DefinitionSource, line 87

vector/equivalent :
  (x₁ x₂ : List ℚ)
  → Prop

List = data/Listℚ = signed/SignedRational

vector/nil-equivalent

TheoremWorked exampleNo axiomsSource, line 134

vector/nil-equivalent :
  → vector/equivalent [] []

vector/reflexive-example

TheoremWorked exampleNo axiomsSource, line 141

vector/reflexive-example :
  → vector/equivalent [signed/from-nnrat 1, signed/from-nnrat 2] [signed/from-nnrat 1, signed/from-nnrat 2]

vector/subtract-equivalent-example

TheoremWorked exampleNo axiomsSource, line 154

vector/subtract-equivalent-example :
  → vector/equivalent [signed/from-nnrat 4 - signed/from-nnrat 1, signed/from-nnrat 4 - signed/from-nnrat 1] [signed/from-nnrat 3, signed/from-nnrat 3]

- = signed/subtract

vector/nil-cons-not-equivalent

TheoremWorked exampleNo axiomsSource, line 168

vector/nil-cons-not-equivalent :
  → proposition/negation (vector/equivalent [] [signed/from-nnrat 1])

vector/cons-nil-not-equivalent

TheoremWorked exampleNo axiomsSource, line 174

vector/cons-nil-not-equivalent :
  → proposition/negation (vector/equivalent [signed/from-nnrat 1] [])